LeanDojo
First page
Paper summary
An open-source Lean playground consisting of toolkits, data, models, and benchmarks for theorem proving.
Ask this paper
01
Theorem-proving infrastructure: Full stack for LLM-based theorem proving in Lean, including the first large-scale extraction of proof data from the Mathlib library.
02
ReProver model: Releases a retrieval-augmented LLM-based prover that selects relevant premises from a vast math library rather than memorizing everything.
03
Academic accessibility: Makes theorem-proving research accessible to smaller groups that lack the resources to build Lean tooling from scratch.
04
Formal math acceleration: A foundational piece that enabled 2024 breakthroughs like DeepMind's AlphaProof and the broader surge in LLM-driven formal math research.