DeepSeek-Prover-V2: RL + Monte Carlo Tree Search Solves 49% of Competition Math Problems

DeepSeek released Prover-V2 in April 2025, extending its formal mathematics line into a different regime: not just solving math problems as text, but generating machine-verifiable proofs that Lean 4 can check. The result, 49.3% on MiniF2F, means the model correctly proves nearly half of competition-level mathematics problems with formal, step-by-step proofs where every logical step is verified by an automated theorem prover.

This is a qualitatively different capability from benchmark scores on AIME or MATH-500, where a model outputs a numerical answer. Lean 4 proofs are programs — they either compile (the proof is correct) or they don't. There's no partial credit, no human judgment, and no ambiguity.

The Subgoal Decomposition Approach

The core innovation in Prover-V2 is applying RL with Monte Carlo Tree Search (MCTS) to proof generation, using a subgoal decomposition strategy:

Proof as tree search: A mathematical proof isn't a single generation — it's a sequence of logical steps, each building on previous ones. If any step fails (can't be proven from the previous steps), the entire proof fails. This is the fundamental difficulty: you can't just generate the full proof and check at the end; you need to explore the proof space.

Subgoal decomposition: Rather than generating the complete proof in one pass, Prover-V2 breaks the problem into subgoals — intermediate claims that, if proven, imply the final result. Each subgoal is attacked independently. The MCTS framework explores different subgoal decompositions, tracking which paths lead to provable lemmas and which are dead ends.

Lean 4 verification at each step: Every candidate subgoal is verified by Lean 4 before the search continues. Invalid proof steps are pruned immediately rather than propagating through the tree. This is what makes MCTS work here — the verifier provides clean binary feedback at each node.

RL from proof outcomes: The model is trained with RL using proof success/failure as the reward signal. Successful complete proofs reinforce the subgoal decompositions and proof strategies that led to them. This is analogous to how DeepSeek R1 uses correctness of mathematical answers as RL signal, but with formal proof verification as the oracle.

Architecture

Prover-V2 uses the DeepSeek-V3 671B MoE architecture as its base, with specialized post-training for formal proof generation. The 671B total / 37B active specification means the same compute envelope as V3 — the mathematical specialization comes from training, not architectural changes.

The training pipeline:

1. Warmup on formal proofs: SFT on a large corpus of Lean 4 proofs, establishing familiarity with the proof language
2. Subgoal synthesis: Training specifically on generating valid subgoal decompositions
3. MCTS-guided RL: The core training phase — RL with tree search, Lean 4 as the verifier, proof success as reward
4. Cold start handling: Techniques for proving problems where no direct training examples exist, involving proof sketch generation and guided search

Benchmarks

MiniF2F competition benchmark results (April 2025):

The jump from Prover-V1.5 (37.0%) to V2 (49.3%) represents +12.3 percentage points — a substantial improvement from the MCTS approach. For context, 49.3% of MiniF2F problems are competition-level (AMC/AIME/IMO difficulty) formalized in Lean 4.

The informal comparison to GPT-4 (22%) is significant: formal proof generation is dramatically harder than informal answer generation, and yet dedicated formal proof models have surpassed informal-only models by a wide margin at this task.

What Formal Proof Means for AI Math

The distinction between informal math solving (R1, o1, GPT-4) and formal proof generation (Prover-V2) matters:

Informal: Model outputs text that looks like a mathematical argument. May be correct. May contain subtle errors. Correctness is judged by humans or by checking the final numerical answer.

Formal: Model outputs Lean 4 code. Either the theorem prover accepts it (provably correct) or rejects it (definitely wrong). No ambiguity. No "plausible but wrong" category.

For AI safety research, for verifying mathematical software, for educational tools where correctness matters absolutely — formal proof is a different capability class.

Open Source

Prover-V2 is released under MIT license:

• huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B — full model
• huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B — distilled 7B variant

The 7B distilled variant achieves 33.5% on MiniF2F — significantly more deployable for researchers working with formal math, and competitive with previous full-scale models.

What It Means for Developers

Lean 4 proof automation: For teams working with Lean 4 — whether for software verification, mathematical research tools, or educational proof assistants — Prover-V2 provides the most capable automated proof search available as open weights.

Mathematical software verification: Formal verification of algorithmic correctness is an application area where Prover-V2's Lean 4 capability is directly applicable. If you can express a correctness claim as a Lean 4 theorem, Prover-V2 can attempt to prove it.

Research base: The MCTS + RL methodology for formal proof search is described in detail in the technical report. Teams working on automated theorem proving, formal verification, or RL for structured generation have a well-documented system to build on and compare against.

7B for practical use: The 7B distilled model brings formal proof generation within reach of smaller deployments. For interactive proof assistants or educational tools, 7B latency and cost is workable in a way that 671B is not.

Bottom Line

DeepSeek-Prover-V2 established that combining MCTS with Lean 4 verification and RL training could achieve near-50% formal proof rates on competition-level mathematics. The jump from V1.5 to V2 (+12 points) suggests the MCTS component is load-bearing, not just incremental.

For the formal verification and automated theorem proving communities, Prover-V2 represents a significant capability jump available as open weights. For the broader AI community, it's a data point on what becomes possible when you give a model a formal verifier as an RL reward signal.

Resources

• Technical Report (arXiv 2504.21801) — MCTS approach, subgoal decomposition, training details
• HuggingFace — DeepSeek-Prover-V2-671B — full model
• HuggingFace — DeepSeek-Prover-V2-7B — distilled 7B
• GitHub — DeepSeek-Prover-V2 — code and examples

DeepSeek-Prover-V2 weights are available at HuggingFace under MIT license. Full 671B and distilled 7B variants available.