ReProver
LeanDojo
A retrieval-augmented language model proposes the next Lean tactic, and best-first search runs each tactic in Lean to get new proof states.
The loop
- Proposes
Lean tactics, from a language model that first retrieves relevant premises from the math library
- Judged by
The Lean environment, driven through LeanDojo, which runs each tactic and reports the new state or an error
- Steers
Best-first search expands the most promising proof states and feeds each new state back to the tactic generator
Headline result
On the LeanDojo Benchmark test set, pass@1 is 51.2% (random split) and 26.3% (novel_premises split) with retrieval, versus 47.6% and 23.2% without retrieval and 29.0% and 7.4% for zero-shot GPT-4. Also 26.5% on miniF2F and 13.8% on ProofNet (pass@1, 10 minute wall-time limit per theorem).
What this does not prove
Main experiments use Lean 3 (Lean 4 results are in an appendix not covered here). The tactic generator is trained once, offline, on extracted proofs; search results do not update its weights. The paper's claim is about open, cheap training (one GPU week), not top accuracy.
How it generalizes the harness
A search algorithm drives the proof and calls the model for candidate tactics; Lean decides validity and the output proof needs no model to check.
Classification
| What it proposes | Proof tactic |
|---|---|
| Generative model | Retrieval-augmented transformer tactic generator, trained on LeanDojo data |
| Algorithmic authority | Lean proof assistant via LeanDojo |
| Feedback | Proof state |
| What gets updated | Search tree |
| When it runs | At inference time |
| Validity | Formal (machine-checked) |
| Evidence | Experiments reported |
| Lineage | Original system |