Primary evidence
- LeanDojo: Theorem Proving with Retrieval-Augmented Language ModelsS1 · Primary research · Paper · 2023-06-27
- LeanDojo repositoryS1 · Primary research · Repository
LeanDojo opens a reproducible environment for LLM theorem proving in Lean
The project extracts proof states, tactics and premise information from Lean repositories and exposes a programmatic proof environment. ReProver retrieves relevant premises before generating tactics, directly addressing the library-scale premise-selection problem.
What happened?
LeanDojo released an open toolkit and benchmark for interacting with Lean and training theorem provers, together with ReProver, a retrieval-augmented language-model prover evaluated on nearly one hundred thousand mathlib theorems.
Why it matters
LeanDojo helped turn Lean theorem proving into an accessible machine-learning research platform and supplied infrastructure that later formal-math agents could reuse rather than rebuilding environment integration from scratch.
Significance rationale: LeanDojo lowered the reproducibility barrier for learning-based theorem proving by combining programmatic Lean interaction, extracted proof data, a large benchmark and an open retrieval-augmented prover.
Historical context
Earlier developments
Later developments
Related milestones
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- Autonomous primary role
- Formal assurance
- Artifact available
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Symbolic
- AI contribution
- ReProver used retrieval and language-model generation to choose premises and propose Lean tactics, with the proof assistant determining whether generated proof steps were valid.
- Human contribution
- Researchers engineered the Lean extraction and interaction tooling, built the benchmark, trained the retriever and generator, and designed reproducible evaluation splits.
- Verification
- Paper released · E3 · Inspectable artifact · Artifact available
- Last reviewed
- 2026-09-15
Technical details
- Systems
- leandojo, reprover, lean
- Organizations
- caltech, nvidia
- Problems
- lean-theorem-proving
- Methods
- retrieval-augmented-generation, premise-selection, formal-theorem-proving, language-modeling
Sources & artifacts
- LeanDojo: Theorem Proving with Retrieval-Augmented Language ModelsS1 · Primary research · Paper · accessed 2026-09-10
- LeanDojo repositoryS1 · Primary research · Repository · accessed 2026-09-10
- LeanDojo theorem-proving toolkitArtifact · Code
Verification history
- 2023-06-27 · Paper released · E2 · Research record
The paper described LeanDojo, ReProver and the benchmark methodology.
- 2023-06-27 · Paper released · E3 · Inspectable artifact
Open-source tooling, benchmark resources and prover code were released for reproduction and extension.
Corrections
No corrections recorded.