DeepSeek-Prover (V1)
Lean 4 theorem prover trained on 8M synthetic formal statements with proofs, reaching 52% cumulative on miniF2F versus GPT-4's 23%.
Auto-formalizes competition problems into Lean 4, filters low-quality statements, then generates proofs at scale to fine-tune a 7B model. The synthetic data fixes the shortage of formal proofs.
- Date
- Thursday, 23 May 2024
- Lab
- DeepSeek
- Kind
- paper
- Access
- open weights (restricted license)
Figures
| Measure | Value | Measured by |
|---|---|---|
| miniF2F-test (Lean 4) | 46.3% (64 samples), 52% cumulative GPT-4 baseline 23% | company |
Sources
This record was checked against its sources on 6 October 2026. How we check