Hi! I'm Jannis Limperg, a PhD student of computer science in the LMU Theoretical Computer Science group on the Lean Forward project under the supervision of Jasmin Blanchette.

I'm interested in interactive theorem proving, particularly tooling and proof automation for theorem provers based on dependent type theory. I currently use Lean 4 and have previously used Coq and Agda.

My main project is currently Aesop, a pragmatic, customisable proof search tactic for Lean 4.

Drafts

Publications

Theses

Software

Talks

Academic Service

Teaching

Students

Blog

Contact