DeepSeek publishes a 671B open-weight theorem prover for Lean 4
DeepSeek uploaded DeepSeek-Prover-V2 to Hugging Face on April 30: a 671B-parameter open-weight model built on DeepSeek-V3-Base that writes Lean 4 proofs, plus a 7B sibling with a 32K context window. The pipeline bootstraps itself — DeepSeek-V3 decomposes a theorem into Lean subgoals, a smaller prover searches each subgoal, and the resolved steps are stitched back into chain-of-thought data used to cold-start reinforcement learning. DeepSeek reports an 88.9% pass ratio on MiniF2F-test and 49 of 658 PutnamBench problems solved, which it calls state of the art for neural theorem proving.
Formal verification is the one part of the stack where generated code can be checked instead of trusted, and the missing piece was always a prover good enough to automate it. With 671B weights downloadable and a 7B variant that fits on a single GPU, a team can wire proof search into CI and let Lean reject bad proofs rather than asking a second model for an opinion. The marginal cost of that loop is the hardware you already own, not an API invoice.

WHY IT MATTERS
If machine-checked proofs become a cheap local primitive, verified code moves from research demo to CI gate: an agent proposes a patch, Lean decides whether the reasoning holds, and reviewers stop being the last line of defense on correctness claims. That is a materially different reliability story from asking a second model to agree with the first.
.png)





