DeepSeek-Prover-V2 (7B, 671B)
Lean 4 prover built on V3: 88.9% on miniF2F-test and 49 of 658 PutnamBench problems, using V3-driven subgoal decomposition for cold-start data.
DeepSeek-V3 decomposes theorems into subgoals and formalizes them in Lean 4 to create cold-start data; RL with binary Lean-verifier reward then links informal reasoning to formal proof. Adds ProverBench (325 problems).
- Date
- Wednesday, 30 April 2025
- Lab
- DeepSeek
- Kind
- open-weights
- Access
- open weights (restricted license)
Figures
| Measure | Value | Measured by |
|---|---|---|
| miniF2F-test pass ratio | 88.9% 49 of 658 PutnamBench problems solved (671B) | company |
License tag not re-read; earlier Prover releases used DeepSeek's Model License.
Sources
This record was checked against its sources on 6 October 2026. How we check