Jannis Limperg

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

• Tactic Script Optimisation for Aesop
  Jannis Limperg. To be published at CPP 2025.
  Preprint ∎ Supplement

Publications

• ABEL: Sample Efficient Online Reinforcement Learning for Neural Theorem Proving
  Fabian Gloeckle, Jannis Limperg, Gabriel Synnaeve and Amaury Hayat. MATH-AI 2024
  PDF ∎ OpenReview
• Aesop: White-Box Best-First Proof Search for Lean
  Jannis Limperg and Asta Halkjær From. CPP 2023. Distinguished Paper Award
  Published PDF ∎ Publisher's website ∎ Supplement ∎ Slides
• A Novice-Friendly Induction Tactic for Lean
  Jannis Limperg. CPP 2021
  Published PDF ∎ Publisher's website ∎ Supplement ∎ Short talk + slides ∎ Long talk + slides

Theses

• A Reflexive Graph Model of Sized Types
  Chalmers University of Technology. 2019. Supervised by Andreas Abel
  PDF ∎ Code ∎ Rendered code
• A Cofixpoint Combinator for Mixed Recursive-Corecursive Functions
  University of Freiburg. 2017. Supervised by Peter Thiemann
  PDF ∎ Code

Software

• Aesop: white-box proof automation for the Lean 4 theorem prover

Talks

• Aesop: White-Box Automation for Lean 4
  BICMR and Istituto Grothendieck (online). April 2024
  Slides
• A Taste of Lean 4
  Lecture series at the International Summer School on Interactions of Proof Assistants and Mathematics in Regensburg. September 2023
  Materials
• Aesop: White-Box Best-First Proof Search for Lean
  TU Delft Programming Languages Seminar. February 2023
  Slides
• Towards Complete Tree-Based Proof Search with Metavariables
  With Asta Halkjær From. VU Theoretical Computer Science Seminar. May 2022
  Slides
• Towards General-Purpose Automation for Lean
  Lean Together 2021
  Video ∎ Slides

Academic Service

• Subreviewer, CPP 2024
• PC Member, FM 2024 Tutorials Track
• Subreviewer, CICM 2024
• Artifact Evaluation Co-Chair, ICFP 2022 and 2023
• Member of the IPA PhD Council, 2022—2023
• Artifact Evaluator, ICFP 2021
• Subreviewer, CAV 2021 and AITP 2021

Teaching

• Seminar: Software Foundations 2024
• Formale Sprachen und Komplexität 2024 (assistant)
• Seminar: Dependent Type Theory 2024
• Seminar: Basics of Theorem Proving Using Coq 2023
• Formale Sprachen und Komplexität 2023 (assistant)
• Logical Verification 2020—2022 (TA and some lectures)
• Logic and Modelling 2022 (TA and some lectures)

Students

• Alistair Geesing. Premise Selection for Lean 4. MSc thesis. 2023
• Jasper Abbes. Verified Binomial Heaps in Lean 4. BSc thesis. 2023
• Michalis Stylianou. Compiling the Lambda Calculus to C++. BSc thesis. 2023
• Reinier van der Gronden. A Tool for Structuring Interactive Proofs. MSc thesis. 2023
• Dominique Danco. Porting the induction' Tactic to Lean 4. MSc project. 2023
• Othman Alhorani. Implementing and Verifying Merge Sort in Lean 3. BSc thesis. 2021
• Péter Kementzey. A Graph Library for Lean 4. BSc thesis. 2021
• Sofia Konovalova. Verifying AVL Trees in Lean. BSc thesis. 2021

Blog

• A Guide to GHC's Extensions

• A Basic Lean 4 Project Template 31 May 2021
• Some Lean Metaprogramming Gotchas 19 August 2020
• On the Master Programme "Algorithms, Languages and Logic" at Chalmers University Gothenburg 27 December 2019
• Yoneda's Lemma in Excruciating Detail 27 July 2018

Contact

• E-Mail: <my first name>@<my last name>.de or <my first name>.<my last name>@lmu.de
• Office: Oettingenstraße 67, room L 103
• PGP key: 19A1F1FCF8652F1EDF460E5D4723F9AD5B3835B9
• GitHub: JLimperg
• Reddit: /u/jlimperg