Jannis Limperg

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 foci are AI-assisted software verification and (the Lean part of) LLM-based agents that write formal proofs.

I was previously an 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, MATH-AI 2026, 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 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
• LinkedIn: Jannis Limperg