DeepSeek releases DeepSeek-Prover-V2 for Lean 4 theorem proving

What happened

DeepSeek released DeepSeek-Prover-V2, an open-source model for formal theorem proving in Lean 4. Its paper was posted to arXiv on 30 April 2025, and Wikipedia lists the release as 1 May 2025. ^[1][3]

Theorem proving is the task of showing that a mathematical statement follows from accepted axioms and earlier results. In Lean 4 the proof is written in the language itself, so a correct proof can be verified mechanically. Benchmarks in this area are collections of competition-style problems, which makes results comparable across models tested on the same set.

Key details

The cold-start training data came from a recursive proving pipeline driven by DeepSeek-V3, which breaks problems into subgoals. ^[1]

Resolved subgoal proofs were combined with DeepSeek-V3's step-by-step reasoning into chain-of-thought data, integrating informal and formal reasoning in one model. ^[1]

The model reached an 88.9% pass ratio on the MiniF2F-test benchmark and solved 49 of the 658 problems in PutnamBench. ^[1]

The paper introduced ProverBench, 325 formalized problems including 15 from the AIME 2024 and 2025 competitions. ^[1]

Impact

A proof checked by a computer does not rely on trust in the author, which is why formal theorem proving is watched as a route to checkable mathematical results. The paper's comparison with natural-language solving on the same AIME problems is the most direct evidence it gives on that question.