BFS-Prover
A plain best-first search over Lean tactics, with a model retrained each round on the proofs and compiler errors the search produced.
The loop
- Proposes
Lean 4 tactics for the current proof state, from a language model
- Judged by
The Lean 4 compiler through LeanDojo, which runs each tactic and reports success or an error
- Steers
Best-first search ranks states by log probability; expert iteration retrains on proofs (SFT) and error pairs (DPO)
Headline result
Reaches 72.95% on the miniF2F test set as an accumulative score; the single-run figure is 70.83% +/- 0.89 at a budget of 2048 x 2 x 600 (Lean 4.7.0). The authors say this shows plain best-first search can compete when scaled.
What this does not prove
The 72.95% is a cumulative (union across runs and settings) score, not one fixed-budget run. Its claims date from early 2025 and are compared with provers that used different budgets.
How it generalizes the harness
- A domain authority judges
- Feedback retrains the generator
- Search over a population
- The output outlives the model
Compiler verdicts retrain the generator between rounds while a search tree is explored; the proofs it outputs are machine-checkable without it.
Classification
| What it proposes | Proof tactic |
|---|---|
| Generative model | 7B policy language model (open-sourced as BFS-Prover-V1-7B) |
| Algorithmic authority | Lean 4 compiler via LeanDojo |
| Feedback | Verifier errors |
| What gets updated | Model weights, search tree and training data |
| When it runs | During training |
| Validity | Formal (machine-checked) |
| Evidence | Experiments reported |
| Lineage | Original system |