Jannis Limperg

Hi! I'm Jannis Limperg, an Applied Scientist at Amazon Web Service working on neurosymbolic AI.

I'm interested in interactive theorem proving, particularly tooling and proof automation for Lean 4. Currently, my main focus is (the Lean 4 part of) LLM-based agents that write formal proofs.

I was previously a PhD student at the Chair for Theoretical Computer Science and Theorem Proving, LMU Munich, under the supervision of Jasmin Blanchette.

I'm the main author of Aesop, a pragmatic, customisable proof search tactic for Lean 4.

Drafts

• Incremental Forward Reasoning for White-Box Proof Search
  Xavier Généreux and Jannis Limperg. To be published at TACAS 2026
  Preprint ∎ Supplement

Publications

• Tool-Assisted Multi-Turn Theorem Proving with LLMs
  Kanan Gupta, Jannis Limperg and Udaya Ghai. MATH-AI 2025
  Published PDF ∎ Publisher's website
• Tactic Script Optimisation for Aesop
  Jannis Limperg. CPP 2025
  Published PDF ∎ Publisher's website ∎ Supplement ∎ Talk ∎ Slides
• 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

• Efficient Forward Reasoning for Aesop
  With Xavier Généreux. Lean Together. January 2025
  Video ∎ Slides
• Aesop: White-Box Automation for Lean 4
  Amazon Web Services (online). December 2024
  Slides
• Aesop: White-Box Automation for Lean 4
  University of Heidelberg. December 2024
  Slides
• 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

• PC Member, MATH-AI 2025
• 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

• Samuel Leßmann. Intensional Martin-Löf Type Theory as a Domain-Specific Language in Lean. BSc thesis. 2025
• Hoang Vu Nhat. Feasibility Study for Eager Normalization in Aesop. BSc thesis. 2025
• Florian Würmseer. Generalised Rewriting for Lean. MSc thesis. 2025
• Johannes Reichle. A Formalization of a Predicative Intensional Dependent Type Theory with One Universe in Lean. MSc thesis. 2025
• Moatez Ouertatani. Semi-Automatic Structuring of Lean Proofs. BSc thesis. 2025
• Kerem Ergür. Expression Matching Up to Weak Head Normal Form in the Lean Proof Assistant. BSc thesis. 2025
• Melissa Rapp. Negative Caching for Lean's Simplifier. BSc thesis. 2024
• 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

• Email: <my first name>@<my last name>.de
• PGP key: 19A1F1FCF8652F1EDF460E5D4723F9AD5B3835B9
• GitHub: JLimperg