Lean and AI
Use Lean 4 as a training and evaluation ground for machine-learning-guided theorem proving, and study what makes a Lean proof state learnable.
- Suitable for
- Master's thesis
PhD thesis - Supervision
- Zafeirakis Zafeirakopoulos
Interactive theorem provers like Lean produce, as a side effect of ordinary use, a huge amount of structured data: proof states, the tactics that transform them, and the premises (lemmas from Mathlib) used along the way. This has made Lean one of the main testbeds for machine-learning-guided theorem proving: models that suggest the next tactic, retrieve a relevant lemma, or search a proof tree, with every candidate step checked by Lean’s own kernel.
Unlike most machine learning settings, a wrong answer here is not merely graded low — it fails to compile. This gives the field an unusually clean notion of correctness, and makes Lean a natural place to study what “the model is right” actually means.
Why it matters
- Grounded evaluation. LeanDojo’s benchmark of ~100,000 theorem/proof pairs extracted from Mathlib, together with its retrieval-augmented prover (ReProver), gave the field a reproducible way to compare tactic-prediction and premise-selection models against each other.
- A shared yardstick. miniF2F translates competition mathematics (AIME, AMC, IMO) into a common benchmark spanning Lean, Isabelle, HOL Light, and Metamath, so that progress in neural theorem proving can be compared across proof assistants, not just within one.
- Directly relevant to this lab’s other Lean topics. Whatever benchmark or tooling this topic produces can double as evaluation infrastructure for the Lean and Computer Algebra and Lean and Polyhedral Geometry topics: e.g. can a retrieval-augmented prover close routine lemmas in a new polyhedral-geometry file automatically?
Targets
Premise retrieval. Reproduce a small-scale version of LeanDojo’s retrieval-augmented setup: given a proof state, retrieve the Mathlib lemmas most likely to be useful next.
Benchmark extension. Extract a small, well-scoped benchmark of proof states from one of this lab’s own Lean topics (e.g. the Euclidean-domain or Gröbner-basis formalizations), in the style of miniF2F, and evaluate an existing tactic-prediction model on it.
Failure analysis. Characterize where current models fail on this lab’s benchmark: is it premise selection, tactic choice, or search depth?
Goal
Build a small, reproducible evaluation pipeline (data extraction from Lean proofs, an existing or lightly adapted model, and a scoring script) for one machine-learning-for-theorem-proving task, and report where it succeeds and fails.
Milestones
| ID | Title |
|---|---|
| M1 | Environment setup; extract proof states from a Lean project |
| M2 | Baseline model running end-to-end on extracted data |
| M3 | Evaluation + failure analysis |
| M4 | Final report |
Tasks
| ID | Title | Status |
|---|---|---|
| T1 | Set up LeanDojo (or equivalent) data extraction | todo |
| T2 | Run a baseline retrieval/tactic model | todo |
| T3 | Build the evaluation benchmark + run failure analysis | todo |
| T4 | Write-up | todo |
Deliverables
- Reproducible pipeline: Lean proof-state extraction, model, and scoring script
- A small benchmark of proof states drawn from this lab’s own Lean formalizations
- Final report analyzing where the model succeeds and fails
Resources
References
-
K. Yang, A. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. Prenger, and A. Anandkumar. LeanDojo: Theorem Proving with Retrieval-Augmented Language Models. NeurIPS 2023, Datasets and Benchmarks Track. proceedings.neurips.cc
-
K. Zheng, J. M. Han, and S. Polu. miniF2F: a cross-system benchmark for formal Olympiad-level mathematics. ICLR 2022, OpenReview.net. openreview.net/forum?id=9ZPegFuFTFv