Overview
DeepSeek-Prover-V2 is DeepSeek's open-weight model line for formal mathematical theorem proving in the Lean 4 proof assistant, released on 30 April 2025. It ships in two sizes: DeepSeek-Prover-V2-7B, a dense model built on DeepSeek-Prover-V1.5-Base with a 32K context, and DeepSeek-Prover-V2-671B, a Mixture-of-Experts model built on DeepSeek-V3-Base that activates roughly 37B of its parameters per token and inherits DeepSeek-V3's 163,840-token (164K) context window. Both produce machine-checkable Lean 4 proofs rather than free-text math.
The defining idea is reinforcement learning for subgoal decomposition. DeepSeek-V3 is prompted to break a hard theorem into a chain of subgoals and formalize each as a Lean 4 statement; once the smaller subgoals are proved, their proofs are recombined with the informal reasoning into a single chain-of-thought example. This 'cold-start' synthetic data trains the prover, and a follow-up RL stage with a binary correct/incorrect reward teaches it to connect natural-language reasoning to formal proof steps. The approach is described in the paper 'DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition' (Ren et al., arXiv 2504.21801).
DeepSeek-Prover-V2-671B reaches state-of-the-art results among neural theorem provers, with an 88.9% pass ratio on the miniF2F-test benchmark and 49 of 658 problems solved on PutnamBench. DeepSeek also released ProverBench, a 325-problem evaluation set that includes 15 formalized AIME 2024-2025 competition problems. The weights are openly downloadable on Hugging Face (BF16 and FP8) under the DeepSeek Model License, and the 671B model is also served through hosted APIs such as Novita.
| Released | 2025-04-30 |
|---|---|
| License | DeepSeek Model License (code MIT) |
| Weights | Open weights |
| Parameters | 671B total / ~37B active per token (671B MoE); 7B (dense) |
| Context | 164K (671B); 32K (7B) |
| Max output | Not separately specified |
| Architecture | Two open-weight models for formal theorem proving in Lean 4. The 671B variant is built on DeepSeek-V3-Base and inherits its Mixture-of-Experts design (256 experts, 8 active per token, ~37B active parameters) with Multi-head Latent Attention and a 163,840-token context. The 7B variant is a dense model built on DeepSeek-Prover-V1.5-Base with a 32K context. Training uses a recursive proof pipeline: DeepSeek-V3 decomposes a theorem into subgoals and formalizes them in Lean 4, the resolved subgoal proofs are stitched into a chain-of-thought cold-start dataset, and a reinforcement-learning stage then sharpens the model's ability to bridge informal reasoning and formal proof construction. |
| Knowledge cutoff | Not disclosed |
| Modalities | Text |
| Status | Available (open weights) |
Benchmarks
- miniF2F-test (pass ratio, 671B)88.9%
- PutnamBench (problems solved, 671B)49problems
- ProverBench AIME 24-25 (formalized, 671B)6problems
Scores on a 0–100 scale (25-point gridlines); higher is better. Each benchmark links to its published source.
Pricing
| Input | $0.70 / 1M tokens per 1M tokens |
|---|---|
| Output | $2.50 / 1M tokens per 1M tokens |
Hosted-API pricing for DeepSeek-Prover-V2-671B on Novita AI (160K context). The model weights are also free to download and self-host from Hugging Face. DeepSeek does not list this model on its own first-party API.
Strengths
- State-of-the-art neural theorem proving: 88.9% pass ratio on miniF2F-test (671B)
- Produces fully machine-checkable Lean 4 proofs, not just informal math text
- Recursive subgoal decomposition lets it tackle hard problems by proving smaller pieces and recombining them
- Open weights (7B and 671B) on Hugging Face under the DeepSeek Model License — free to self-host
- 671B inherits DeepSeek-V3's efficient MoE backbone (~37B active params) and 164K context for long proofs
- Small 7B variant runs on far more modest hardware while still being a capable Lean 4 prover
Best for
- Automated formal theorem proving and proof search in Lean 4
- Formalizing competition mathematics (e.g. AIME-style problems) into verifiable proofs
- Research on neural theorem proving, subgoal decomposition, and autoformalization
- Assisting mathematicians and Lean users with machine-checkable proof drafts
- Self-hosted formal-math tooling where open weights are required
How to access
| Provider | Model ID |
|---|---|
| Novita AI ↗ | deepseek/deepseek-prover-v2-671b |
| OpenRouter ↗ | deepseek/deepseek-prover-v2 |
DeepSeek Prover — every version
The full lineage of the DeepSeek Prover line, newest first. Every version has its own page — click any to compare specs, benchmarks and pricing.
| Version | Released | Context | License |
|---|---|---|---|
| DeepSeek-Prover-V2current | 2025-04-30 | — | Open weights |
| DeepSeek-Prover-V1.5 | 2024-08 | — | Open weights |
FAQ
What is DeepSeek-Prover-V2?
It is DeepSeek's open-weight model line for formal theorem proving in the Lean 4 proof assistant, released on 30 April 2025. It generates machine-checkable Lean 4 proofs and comes in two sizes: a 7B dense model built on DeepSeek-Prover-V1.5-Base and a 671B Mixture-of-Experts model built on DeepSeek-V3-Base.
How is it trained?
DeepSeek-V3 decomposes each hard theorem into subgoals and formalizes them in Lean 4; the proofs of the resolved subgoals are recombined with the informal reasoning into a chain-of-thought 'cold-start' dataset. The prover is fine-tuned on that data and then refined with a reinforcement-learning stage that rewards correct formal proofs, teaching it to bridge informal reasoning and formal proof construction.
How well does it perform?
The 671B model reaches state-of-the-art neural-theorem-proving results: an 88.9% pass ratio on the miniF2F-test benchmark and 49 of 658 problems solved on PutnamBench. DeepSeek also released ProverBench, a 325-problem set that includes 15 formalized AIME 2024-2025 problems.
Is it open source, and how can I use it?
Both the 7B and 671B weights are openly downloadable from Hugging Face under the DeepSeek Model License (the code is MIT), so you can self-host them. The 671B model is also offered through hosted APIs such as Novita AI and OpenRouter for those who prefer not to run it themselves.