Hi! I'm Jannis Limperg, a researcher at Axiom Math 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 part of) LLM-based agents that write formal proofs.
I was previously and Applied Scientist at AWS and 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.
Articles
-
AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilities
Jimmy Xin, Alexander Mark Schneidman, Chris Cummins, Karun Ram, Srihari Ganesh and Jannis Limperg. AI4Math@ICML 2026. Best Paper Award
PDF ∎ OpenReview -
Verus-SpecGym: An Agentic Environment for Evaluating Specification Autoformalization
Anmol Agarwal, Natalie Neamtu, Pranjal Aggarwal, Seungone Kim, Jannis Limperg, Cedric Flamant, Kanna Shimizu, Bryan Parno and Sean Welleck. 2026
arXiv -
Incremental Forward Reasoning for White-Box Proof Search
Xavier Généreux and Jannis Limperg. TACAS 2026
Published PDF ∎ Publisher's website ∎ Supplement -
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
Books and Lecture Notes
-
The Hitchhiker's Guide to Logical Verification
Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Xavier Généreux, Johannes Hölzl and Jannis Limperg. 2026.
PDF ∎ GitHub -
Metaprogramming in Lean 4
Arthur Paulino, Damiano Testa, Edward Ayers, Evgenia Karunus, Henrik Böving, Jannis Limperg, Siddhartha Gadgil and Siddharth Bhat. 2025
PDF ∎ Website ∎ GitHub
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
-
Symbolic Proof Optimisation for Lean
Leaning In. March 2026
Slides -
Writing in the Age of AI
Guest lecture for a technical writing course at LMU Munich. January 2026
Slides -
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
- Artifact Evaluation Co-Chair: ICFP 2022, ICFP 2023
- PC Member: FM 2024 Tutorials Track, MATH-AI 2025, CPP 2027
- Artifact Evaluator: ICFP 2021
- Subreviewer: CAV 2021, AITP 2021, CICM 2024, CPP 2024
- Member of the IPA PhD Council 2022—2023
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 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
- LinkedIn: Jannis Limperg