DeepSeek-Prover-V2 is a new open-source language model for formal theorem proving in Lean 4. Developed by DeepSeek AI and released in late April 2025, it builds on earlier “Prover” models but introduces a novel training pipeline and much larger scale. In the company’s words, it’s “designed for formal theorem proving within the Lean 4 environment,” and represents a leap in neural proof technology​.

DeepSeek-Prover-V2 comes in two sizes: a 7-billion-parameter model and a massive 671-billion-parameter model​. The larger variant (671B) uses a mixture-of-experts (MoE) architecture – 61 transformer layers with hidden size 7168 – along with FP8 quantization and support for ultra-long contexts (on the order of 163,800 tokens)​, see: ainvest.com.

In practice, DeepSeek-Prover-V2 “achieves state-of-the-art performance” on automated theorem tasks​. For example, the 671B model scores 88.9% pass ratio on the Lean 4 MiniF2F benchmark and solves 49 out of 658 problems on the PutnamBench challenge​ – vastly ahead of previous models.

The release also introduces ProverBench, a new formal benchmark of 325 math problems (including 15 from recent AIME contests)​, allowing evaluation of formal reasoning across high-school and undergrad levels.

DeepSeek emphasizes that Prover-V2 was generated via a recursive proof-search pipeline. It first prompts an even larger DeepSeek-V3 language model to break down hard theorems into subgoals and sketch informal proofs, then uses a smaller 7B prover to solve each subgoal in Lean 4. The full proofs of the subgoals (now formalized in Lean) are paired with the original chain-of-thought sketches, yielding synthetic “cold-start” data for reinforcement learning​.

In short, the model learns both high-level mathematical reasoning and detailed formal steps in one process – a key innovation of this release​.

Download and Platform Support

The DeepSeek-Prover-V2 models are freely available for download. DeepSeek’s GitHub repository (Github.com/deepseek-ai/DeepSeek-Prover-V2) and Hugging Face model hub host the code and weights. According to the official README, the two released models can be obtained via Hugging Face:

• DeepSeek-Prover-V2-7B – Hugging Face model ID deepseek-ai/DeepSeek-Prover-V2-7B​
• DeepSeek-Prover-V2-671B – Hugging Face model ID deepseek-ai/DeepSeek-Prover-V2-671B

In practice, you can simply call AutoModelForCausalLM.from_pretrained("DeepSeek-Prover-V2-7B") or -671B to load the model. The GitHub page provides direct download links and also a ZIP of example proofs for the MiniF2F dataset​.

These models are distributed in safetensors format (as noted by AI press) and support mixed-precision inference (e.g. bfloat16 or 8-bit)​, see: ainvest.com. The 671B model is very large (~650 GB when unpacked; DeepSeek quantized it to 8-bit to roughly half its size). Running it requires a high-end GPU setup, but because it’s on Hugging Face you can also run inference via the Transformers library on any machine with enough RAM/VRAM.

DeepSeek explicitly notes the models support local deployment and even commercial use​, thanks to their permissive license (the model is released under an MIT-style open-source license​). In short, if you have Python and PyTorch installed, you can download and run Prover-V2 anywhere.

In terms of environment, DeepSeek-Prover-V2 targets Lean 4. It expects inputs in the Lean 4 theorem-proving language (as shown in usage examples below). However, because it is delivered as a standard HuggingFace Transformers model, it can be used on Linux, Windows, or macOS just like any Python library. The main dependencies are transformers and torch (plus any Lean 4 environment if you want to verify proofs).

DeepSeek’s quickstart guide specifically assumes you use the HuggingFace chat-generation API, but you could also use raw token generation or the pipeline API. All model details (architectural features, supported context length, etc.) are documented on Hugging Face under the DeepSeek-V3 model card and the Prover-V2 repo.

Basic Usage

Getting started with DeepSeek-Prover-V2 is straightforward if you’re familiar with HuggingFace Transformers. First, install the necessary Python packages:

• pip install torch transformers
• (If not already, install Lean 4 on your system so you can verify proofs.)

Then load the model and tokenizer from Hugging Face. For example, in Python you might write:

pythonCopyEditfrom transformers import AutoModelForCausalLM, AutoTokenizer
import torch
torch.manual_seed(30)

model_id = "DeepSeek-Prover-V2-7B"  # or use "DeepSeek-Prover-V2-671B"
tokenizer = AutoTokenizer.from_pretrained(model_id)
model = AutoModelForCausalLM.from_pretrained(
    model_id, 
    device_map="auto", 
    torch_dtype=torch.bfloat16,
    trust_remote_code=True
)

This snippet (adapted from the official README) loads the 7B model into GPU memory, see: ​github.com. The trust_remote_code=True is required because DeepSeek uses a custom generation template. Once loaded, you can feed the model a Lean 4 theorem (as plain text) and ask it to “Complete” the proof. DeepSeek’s recommended approach is to prompt for a proof plan first, then the formal proof. For example:

pythonCopyEditformal_statement = """
import Mathlib
import Aesop

set_option maxHeartbeats 0

open BigOperators Real Nat Topology Rat

/-- What is the positive difference between 120% of 30 and 130% of 20?
    Show that it is 10. -/
theorem mathd_algebra_10 : abs ((120 : ℝ) / 100 * 30 - 130 / 100 * 20) = 10 :=
by
  sorry
""".strip()

prompt = f"Complete the following Lean 4 code:\n```lean4\n{formal_statement}\n```\n"
prompt += "Before producing the Lean 4 code, provide a detailed proof plan outlining the main steps and ideas."

inputs = tokenizer(prompt, return_tensors="pt").to(model.device)
outputs = model.generate(**inputs, max_new_tokens=1024)
print(tokenizer.decode(outputs[0]))

This toy example (inspired by DeepSeek’s docs) shows how to ask the model for a proof plan and then a proof. The model will output Lean code for the solution (replacing sorry). In practice, you may need to tune generation settings (max_new_tokens, temperature, etc.) and use the provided chat template API (tokenizer.apply_chat_template) as shown in the docs​.

Quick start summary:

• Installation: Python 3.8+, PyTorch (GPU-enabled), HuggingFace transformers.
• Model loading: Use AutoTokenizer/AutoModelForCausalLM.from_pretrained("DeepSeek-Prover-V2-<size>") with trust_remote_code=True​
• Context length: The 7B model supports up to 32K tokens (extended context)​. The 671B model (same DeepSeek-V3 base) can handle even longer contexts (hundreds of thousands of tokens) due to its architecture.
• Generation: Input is a Lean 4 proof goal. You may prompt for a “proof plan” then the actual proof. Use the Transformers generation API to get the completed Lean code.

The official GitHub README and paper contain more examples (including fine-tuning scripts if needed). For most users, following the HuggingFace example above is enough to start experimenting with Prover-V2.

Benchmark Results

DeepSeek-Prover-V2 shatters previous benchmarks in automated theorem proving. On the MiniF2F Lean benchmark (244 held-out theorems of Olympiad/AIME level), the 671B model hits an 88.9% pass rate​, up from ~63.5% for the earlier DeepSeek-Prover V1.5​arxiv.org and only ~50% for the best prior open model (the LEGO-Prover). On the new PutnamBench (658 formal Putnam problems), DeepSeek-V2 solves 49 problems​ – again a huge jump over the 23 solved by the 7B variant, and trivially larger than older baselines. By contrast, even GPT-4 (a proprietary model) only managed ~22.9% on MiniF2F in comparable tests​. In short, DeepSeek-Prover-V2 dramatically outperforms both open and closed LLMs on formal math tasks.

The embedded figure above (from DeepSeek’s repo) illustrates these results. The left panel (MiniF2F) shows DeepSeek-V2 (88.9%) well above prior models: GPT-4 (~22.9%) and others like Hypertree (41.0%) and LEGO-Prover (50.0%). The center panel (PutnamBench) shows 49 problems solved by V2-671B versus just 23 by the V2-7B model, and single-digit solves by older provers.

The right panel shows the new ProverBench-AIME subset (15 problems): DeepSeek-V2 solves 6 of 15, DeepSeek-V3 solves 8 (informally), while others solve few.

Key benchmarks (summarized): MiniF2F-test pass rate and Putnam solved count for various models: DeepSeek-V2 (671B) – 88.9% / 49 solved​; DeepSeek-V2 (7B) – 82.0% / 23 solved; DeepSeek-Prover V1.5 (7B) – 63.5%​; LEGO-Prover – 50.0%​; GPT-4 – ~22.9%​arxiv.org. No other open-source model is reported anywhere near DeepSeek’s level.

Feature Comparison

How does DeepSeek-Prover-V2 stack up feature-by-feature against other theorem-proving models and LLMs? In general, no other open model is specialized for Lean 4 proofs at this scale. Below we compare some salient features:

• Architecture: Prover-V2-671B uses a Mixture-of-Experts transformer (same as DeepSeek-V3) with 61 layers and hidden dimension 7168​. This allows a huge capacity (671B parameters) with efficiency tricks like token-routing MoE. By contrast, Prover-V1.5 was a dense 7B model​. Other open LLMs (LLaMA, MPT, etc.) are not tailored for math proofs, and closed models (GPT-4) have unknown internals. Importantly, Prover-V2 supports very long contexts: the 7B model runs at up to 32K tokens, while the 671B MoE can handle even more (hundreds of thousands) as documented​.
  
• Training & Data: DeepSeek-Prover-V2 uses large-scale synthetic data generated via an automated pipeline. A powerful DeepSeek-V3 model produces informal proof outlines and Lean subgoal statements, a 7B prover solves them, and the combined reasoning+proof pairs train the model​. Then DeepSeek applies reinforcement learning on top of this data using proof-assistant feedback​.
  
  This is very different from other systems: LEGO-Prover (ICLR’24) uses a “growing library” of lemmas with tree search over GPT-3.5 or similar​openreview.net. Traditional math LLMs just fine-tune on whatever formal corpora exist or use autoformalization. In short, V2’s pipeline combines informal chain-of-thought and formal proof steps in one model​ (syncedreview.com) – no other open model does that.
  
• Performance: As noted, Prover-V2’s raw benchmark scores dwarf the rest. Other top open experiments include the Hypertree Proof Search model (41.0% on miniF2F) and early DeepSeek variants (63.5%). None matched V2’s 88.9%. Even GPT-4 (a closed model) only hits ~25% in comparable tests​, see: arxiv.org. In practical terms, Prover-V2 can solve high-school Olympiad problems almost like a student, whereas generic LLMs struggle on such formal tasks.
  
• Flexibility: DeepSeek-Prover-V2 is explicitly specialized for Lean 4 proofs. It outputs Lean code and is trained to reason in Lean’s logic. Other LLMs (e.g. GPT-3/4, Llama) are general-purpose and can be prompted to emit Lean proofs, but they were not trained on Lean semantics. Conversely, specialized theorem provers like E or Vampire (classic ATP systems) use first-order logic tactics, not raw language models. In that sense, DeepSeek-Prover-V2 occupies a unique niche: an open LLM built for a proof assistant.
  
• Licensing and Openness: DeepSeek-Prover-V2 is fully open-source. Unlike closed models (GPT-4, GPT-3.5, Anthropic’s Claude, etc.), the Prover-V2 weights and code are public. According to DeepSeek, the model files are under a permissive MIT-like license​. (Note: DeepSeek’s own “Model License” includes use-based restrictions, but it has been summarized in media as MIT-compliant​). This contrasts with many high-end LLMs that restrict research use. The open license means users can inspect, modify, and deploy Prover-V2 freely.

Below is a summary table comparing some key aspects of DeepSeek-Prover-V2 versus other recent theorem-proving models:

Model	Params	Focus	Training/Data	Context Length	MiniF2F Pass	License
DeepSeek-Prover-V2 (671B)	671B (MoE)	Lean 4 theorem proving (formal)	Synthetic RL pipeline (chain-of-thought + Lean proofs)​	100K+ (huge)​	88.9%​	MIT-like (open)​
DeepSeek-Prover-V2 (7B)	7B (dense)	Lean 4 proving (formal)	Initialized from V1.5, fine-tuned on proofs	32K​	82.0%	MIT-like
DeepSeek-Prover-V1.5 (2024)	7B	Lean 4 proving	Supervised + RLPAF (no MoE)​	8K (typical)	63.5%​	MIT-like
LEGO-Prover (ICLR’24)	N/A (LM-based)	Lean 4 proving	Growing library + GPT-3.5 prompts​	8K (typical)	50.0%​	Open (code available)
GPT-4 (OpenAI)	~175B (dense)	General LLM (multi-domain)	Pretrained on Internet, not formal-targeted	~8K	~22–25%​arxiv.org	Closed
Others (Kimia, BFS, STP, etc.)	(up to 72B)	Various Lean provers (LLM-based)	Unknown public data; poorer results【45†】	~8K	≤~74%【45†】	Varied

Notes: The figures above come from DeepSeek’s papers and related sources. The DeepSeek models are the only ones achieving high pass rates on MiniF2F​. The “Others” row includes recent open attempts (Kimina-Prover 72B, BFS-Prover 7B, STP 7B, etc.) for which DeepSeek provided benchmark bars【45†】; none reach DeepSeek’s level. All numbers (except GPT-4) are from open sources.

Key Strengths and Innovations

DeepSeek-Prover-V2 introduces several advances that underlie its strong results:

• Recursive “Cold-Start” Pipeline: DeepSeek’s biggest innovation is using one model (DeepSeek-V3) to decompose problems and another (7B prover) to solve substeps, then stitching together full proofs. This generates a rich synthetic dataset of proof plans + formal proofs, bootstrapping the training. It’s akin to providing the model with its own “teacher” hints. No previous open prover model did this at scale.
  
• Reinforcement Learning from Formal Feedback: After the cold-start pretraining, DeepSeek fine-tunes the model with reinforcement learning, using Lean’s proof checker as a judge, see: ​github.com​. Roughly speaking, if the generated proof is valid, the model gets positive reward; if not, negative. This tight loop of feedback tunes the model to produce correct proofs. The use of RL with a proof assistant is a novel approach in the LLM-based proving field.
  
• Chain-of-Thought Integration: The model is explicitly trained to output a proof plan (natural-language reasoning) followed by the formal Lean proof. During training, each synthetic example pairs DeepSeek-V3’s informal reasoning chain with the corresponding Lean code​. Thus DeepSeek-Prover-V2 learns to bridge the gap between intuitive mathematics and rigorous formalization in one shot – a key reason for its success. Many other models either just produce final proofs or rely on a separate planner.
  
• Massive Scale with Efficiency: At 671B parameters (MoE), Prover-V2 is much larger than previous provers. However, DeepSeek makes it practical: they use a 32K-token context for the 7B model and up to ~163K tokens for the 671B MoE​. They also apply FP8 quantization and safetensors to cut memory usage​, see: ainvest.com. As a result, despite its size, the model can run on current hardware (e.g. it “weighs ~650GB” in RAM). It even supports multiple precision (FP8/BF16) for faster inference​. This combination of large capacity and speed is unique.
  
• New Benchmark (ProverBench): DeepSeek didn’t just release models, but also a new dataset. ProverBench collects 325 freshly formalized math problems (15 from AIME contests, 310 from textbooks). This fills a gap in evaluating math LLMs on high-school to undergrad math. By providing this benchmark to the community, DeepSeek enables apples-to-apples comparisons. The figure above shows that DeepSeek-V2 outperforms on ProverBench-AIME (solving 6/15 problems) while earlier models are far behind【45†】.
  
• Open Source and Reproducibility: The Prover-V2 code, model weights, training data, and even proof outputs for MiniF2F are all available publicly . Developers have commented that this is a welcome democratization of math AI – anyone can download the weights from Hugging Face and experiment. For example, one can retrieve the trained model with AutoTokenizer.from_pretrained("DeepSeek-Prover-V2-7B") and reproduce the official results. DeepSeek also published a technical report and a PDF paper link on their GitHub​. All this openness contrasts with many large-model releases.
  
• Example Usage: Here is a minimal example (from the official docs) showing how to prompt DeepSeek to prove a Lean theorem. In this Python snippet, we ask the model to complete a Lean goal by first giving a proof plan and then code: python Copy Edit
  
  model_id = "DeepSeek-Prover-V2-7B" # or -671B tokenizer = AutoTokenizer.from_pretrained(model_id) prompt = f"Complete this Lean 4 code:\n```lean4\n{formal_statement}\n```" model = AutoModelForCausalLM.from_pretrained(model_id, device_map="auto", torch_dtype=torch.bfloat16, trust_remote_code=True) outputs = model.generate(**tokenizer(prompt, return_tensors="pt").to(model.device), max_new_tokens=8192) print(tokenizer.decode(outputs[0])) (This code is adapted from DeepSeek’s Quick Start guide​: github.com.)

Limitations and Future Improvements

Despite its breakthroughs, DeepSeek-Prover-V2 has limitations and areas for improvement:

• Compute and Size: The 671B model is extremely large. Even quantized to 8-bit, the weights are on the order of hundreds of GB​. This means only organizations or cloud users can realistically run it. The 7B variant is more modest (and still state-of-the-art) but with 32K context it too demands multiple high-end GPUs. Users without such hardware may struggle.
  
• Focused Domain: Prover-V2 is only trained on Lean 4 statements. It cannot directly prove arbitrary math problems in plain English. (You must first express a problem in Lean 4.) Similarly, it doesn’t handle other proof assistants like Coq or Isabelle. Its specialization is a double-edged sword: fantastic for Lean, but not a general math student.
  
• Incomplete Coverage: Even with 671B parameters, the model did not solve most problems. On PutnamBench, it solved only 49 of 658 (~7.5%)​. That means its success is impressive but still far from human experts. Many complex theorems remain out of reach. Future work will need to scale the approach even further or refine the search.
  
• No Official Peer-Reviewed Paper Yet: As of release, there was no peer-reviewed publication detailing all methods. DeepSeek provides a PDF and GitHub notes, but outside reviewers have not fully vetted the claims. (Some media noted “no research paper at time of writing”​.) The community must wait for a thorough paper to understand all technical details.
  
• Licensing Details: DeepSeek claims an “MIT” license, but their GitHub includes a custom “Model License” with some use-case restrictions. It’s unclear how strict these are (e.g. for commercial or sensitive use). Users should review the license on the HuggingFace/GitHub before deploying in production.
  
• Limited Fine-Tuning Recipes: The current release focuses on inference. There is no open script for re-running the full RL/proof search pipeline. Advanced users who want to further train or adapt the model will need to reverse-engineer parts of the process. DeepSeek did not (yet) release code for the MCTS or RL loop. This may change if the team publishes more on GitHub.

Context and Community Response

The launch of DeepSeek-Prover-V2 made big waves in the AI and math communities. On April 30, 2025, DeepSeek’s team (notably Huajian Xin and Zhihong Shao) announced on social media that the new model “solves nearly 90% of MiniF2F problems” and dramatically beats previous state-of-the-art on PutnamBench (their Twitter posts echoed the benchmark numbers)​. Tech news outlets quickly picked up the story.

For example, Binance News wrote that Prover-V2 is “built on a mixture-of-experts (MoE) architecture and utilizes the Lean 4 framework for formal reasoning” and is now available on Hugging Face for researchers to use. Cointelegraph highlighted the open-source angle, noting the release “under the permissive open-source MIT license” and emphasizing that weights can now be downloaded and run locally​.

AIInvest praised the efficiency innovations: “61 Transformer layers, maximum position of 163,800, FP8 quantization, Safetensors file format” – details directly drawn from DeepSeek’s documentation.

In online forums, the reaction has been mostly excitement. On AI and theorem-proving subreddits, users posted snippets of DeepSeek’s results and proof examples, marveling at how a machine can now tackle high-school olympiad problems formally. Some pointed out that by including detailed proof plans in the output, the model feels like a “co-pilot” for mathematicians. Others noted challenges: How to scale hardware, how to trust a ML prover, etc.

The introduction of ProverBench (with AIME contest problems) was also hailed as a valuable new test set – some users even started organizing “proof battles” on ProverBench problems.

Developers from other teams chimed in too. A few mentioned that, although impressive, DeepSeek-V2 still leaves room: for instance, maybe combining its output with a symbolic search or SMT solver could solve even harder cases. Some noted that verifying the model’s generated proofs in Lean gives a strong correctness check – if Lean accepts it, the theorem is truly proven (unlike informal LLM math). This combination of ML planning + formal verification is seen by many as a powerful trend.

Quotes from the release: DeepSeek’s own announcement said: “We introduce DeepSeek-Prover-V2, an open-source LLM designed for formal theorem proving in Lean 4”​. On social media, the team summarized the results: “Solves nearly 90% of MiniF2F problems – Significantly improves the SoTA performance on the PutnamBench”. Community members quoted these tweets and celebrated that an “entire chain-of-thought proof is now synthesized end-to-end by an AI.”

Conclusion

DeepSeek-Prover-V2 represents a major step forward in automated theorem proving by AI. It combines cutting-edge language models, novel training pipelines, and reinforcement learning to achieve results that were previously unreachable in the open-source world. The release is not just a technical milestone but also a platform for further research: with the code, data, and benchmarks out in the open, the community can now experiment with formal math reasoning at an unprecedented scale.

Looking ahead, we can expect rapid iteration. Possible next steps include optimizing the model for speed, expanding to other proof assistants, or integrating it into interactive theorem environments. For now, Prover-V2 is an astonishing showcase: a neural “mathematician” that can digest contest problems and spit out formal proofs.

As one reporter put it, it’s a glimpse into AI’s potential to tackle deep mathematical reasoning – though it also reminds us of the careful checks and big compute still needed.