DeepSeek-Prover-V2

DeepSeek-Prover-V2 (released April 30, 2025) is DeepSeek's formal-mathematics model family for generating and verifying proofs in Lean 4. The headline 671B MoE (built on DeepSeek-V3-Base) and a practical 7B variant (built on Prover-V1.5-Base, 32K context) share a key innovation: subgoal decomposition — DeepSeek-V3 breaks theorems into subgoals during training, the prover solves each, and the traces become cold-start data for RL with binary feedback from Lean's kernel verifier.

The 671B model hit 88.9% on MiniF2F and set records on PutnamBench at release; the 7B runs on a 16GB consumer GPU (or ~5GB quantized) making formal proving accessible. Released under the MIT license on Hugging Face.

Honest limits: the 671B needs datacenter hardware (~650GB weights); headline benchmarks are DeepSeek's own; it proves in Lean 4 only — informal math reasoning is not its strength; later open provers (Goedel-Prover-V2, Kimina-Prover) match or beat it far more efficiently.