DeepSeek-Prover-V2

What it is

DeepSeek-Prover-V2 is an open-source model for formal theorem proving in Lean 4, a programming language and proof assistant in which a mathematical statement and its proof are written in a form a machine can check step by step ^[1]. That separates it from a system that explains mathematics in ordinary prose: the output is a proof script that the Lean kernel either accepts or rejects, and an argument that merely sounds plausible earns nothing. The paper describing the model was posted to arXiv on 30 April 2025, and Wikipedia lists the release as 1 May 2025 ^[1][3]. DeepSeek released it in two sizes, 7B and 671B parameters, and the repository states that use of the models is subject to DeepSeek's Model License ^[2].

How it was trained

The cold-start training data was not written by hand. It came from a recursive proving pipeline driven by DeepSeek-V3, which breaks a problem into subgoals, works on each subgoal, and turns the results into training material ^[1]. Proofs of the subgoals that were resolved were then combined with DeepSeek-V3's step-by-step reasoning to form chain-of-thought data, so that informal reasoning and formal proof live in one model ^[1]. In effect the model practises two skills at once: talking through a strategy in ordinary mathematical language, and rendering each step in Lean so that it checks. The paper's title frames the method as reinforcement learning for subgoal decomposition ^[1].

Results

On MiniF2F-test, a widely used benchmark for formalized problems, the model reached a pass ratio of 88.9% ^[1]. On PutnamBench, which contains 658 problems, it solved 49 ^[1]. The two numbers describe different kinds of difficulty: a high pass ratio on a curated benchmark, and a smaller absolute count on a much larger and harder collection.

ProverBench

The paper introduced a benchmark of its own, ProverBench, with 325 formalized problems, 15 of them taken from the AIME 2024–2025 competitions ^[1]. Those 15 problems allow a direct comparison between formal and informal solving. DeepSeek-Prover-V2 solved 6 of them, while DeepSeek-V3, answering in natural language and taking a majority vote across attempts, solved 8 ^[1]. The authors read this as a narrowing gap between formal and informal mathematics: the formally trained model was still behind, but the two settings had come close enough to measure against each other on the same questions ^[1].

Release details

The 7B model has an extended context length of up to 32K tokens; the repository gives no context length for the 671B model ^[2]. Both sizes are published as open weights under DeepSeek's Model License ^[2].

Place in the line

DeepSeek-Prover-V2 belongs to DeepSeek's line of mathematics models, and its successor in that line is DeepSeekMath-V2, dated 27 November 2025 ^[3]. What makes the formal branch interesting is that its successes are checkable: a proof either compiles or it does not, so progress on benchmarks such as MiniF2F-test and PutnamBench can be verified rather than judged. The comparison on AIME problems in the paper points at the larger question the model was built to probe — how much of ordinary mathematical reasoning can be carried over into a form that a machine can certify.