Goedel-Prover
A Lean 4 prover trained in rounds: each prover writes proofs, Lean checks them, and verified proofs train the next one.
The loop
- Proposes
Lean 4 proofs for 1.64 million formalized statements
- Judged by
The Lean compiler, which checks each candidate proof
- Steers
Verified proofs join the training set and the next, stronger prover is trained on them (expert iteration)
Headline result
Goedel-Prover-SFT reaches 57.6% Pass@32 on miniF2F, 7.6 points above DeepSeek-Prover-V1.5-RL; the paper's abstract reports over 60% Pass@32 after RL including DPO, 7 PutnamBench problems at Pass@512, and proofs for 29.7K Lean Workbook problems versus 15.7K for prior provers.
What this does not prove
Its best-result claims are dated April 2025 and use Pass@32 or Pass@512, so budgets differ from some rivals. The paper text says 8 iterations while a table lists Iter-9. The abstract does not describe the compiler signal beyond verification.
How it generalizes the harness
Lean-verified proofs become the training data for the next generator, so feedback changes the model, and the proofs are checkable without it.
Classification
| What it proposes | Proof |
|---|---|
| Generative model | DeepSeek-Prover-V1.5-Base fine-tuned over successive rounds |
| Algorithmic authority | Lean compiler |
| Feedback | New labeled data |
| What gets updated | Model weights and training data |
| When it runs | During training |
| Validity | Formal (machine-checked) |
| Evidence | Experiments reported |
| Lineage | Original system |