Seed-Prover
A Lean prover that writes whole proofs from lemmas and revises them using Lean feedback, proven lemmas and summaries of earlier tries.
The loop
- Proposes
Lean proofs built from lemmas, from a language model
- Judged by
The Lean proof assistant
- Steers
Lean feedback, proved lemmas and self-summaries of earlier attempts go into the next try, with three test-time strategies
Headline result
The abstract reports 78.1% of formalized past IMO problems proved, MiniF2F saturated, above 50% on PutnamBench, and 5 of 6 IMO 2025 problems fully proved; a separate Seed-Geometry engine handles geometry.
What this does not prove
This card rests on the abstract only. Budgets, training details and who formalized the IMO 2025 statements are not stated there.
How it generalizes the harness
Lean decides validity and the finished proof is checkable without the model; the abstract does not support weight updates from the loop.
Classification
| What it proposes | Proof |
|---|---|
| Generative model | Lemma-style whole-proof language model |
| Algorithmic authority | Lean proof assistant |
| Feedback | Verifier errors |
| What gets updated | Prompt context |
| When it runs | At inference time |
| Validity | Formal (machine-checked) |
| Evidence | Experiments reported |
| Lineage | Original system |