Primary evidence
- DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic DataS1 · Primary research · Paper · 2024-05-23
DeepSeek-Prover scales Lean theorem proving with millions of synthetic formal statements
Natural-language competition problems are translated into Lean statements, filtered, proved and recycled as synthetic training data.
What happened?
DeepSeek-Prover trained on a synthetic corpus containing about eight million formal statements with proofs and reported 52% cumulative accuracy on Lean 4 miniF2F plus five FIMO proofs.
Why it matters
The work established synthetic formal-data generation as a scalable route to stronger neural theorem provers.
Significance rationale: DeepSeek-Prover demonstrated that large-scale synthetic Lean data could materially raise whole-proof generation performance.
Historical context
Earlier developments
Later developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E2 · Research record
- AI role
- AI primary, human verified
- Formal assurance
- Machine-checked
Contribution & verification
- Mathematical novelty
- Benchmark result
- Interface
- Formal, Symbolic
- AI contribution
- Models generate formal statements and whole proofs that Lean checks mechanically.
- Human contribution
- Researchers designed the translation, filtering, proof-generation and training pipeline.
- Verification
- Paper released · E2 · Research record · Machine-checked
- Last reviewed
- 2026-09-11
Technical details
- Systems
- deepseek-prover, lean
- Organizations
- deepseek
- Problems
- minif2f, fimo
- Methods
- synthetic-data, whole-proof-generation, lean
Sources & artifacts
- DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic DataS1 · Primary research · Paper · accessed 2026-09-10
Verification history
- 2024-05-23 · Paper released · E2 · Research record
The Chronicle records this event from the cited primary or official source; the status does not imply independent Chronicle verification.
Corrections
No corrections recorded.