DeepSeek AI has officially unveiled DeepSeek-Prover-V2-671B, a powerful open-source large language model specifically built for formal theorem proving in Lean 4. With this release, DeepSeek takes a major step forward in bridging formal mathematics and AI.
🔍 Advanced Recursive Proof Strategy
At the core of DeepSeek-Prover-V2 lies a novel recursive proof search methodology, initiated through a cold-start pipeline. DeepSeek-V3, another model developed by the team, is prompted to decompose complex mathematical problems into smaller, manageable subgoals.
Once these subgoals are proven, their solutions are combined into a chain-of-thought reasoning process, providing a rich foundation for further training via reinforcement learning. This allows the model to learn not only from formal proofs but also from the informal thinking process that underpins them.
This hybrid approach—blending informal intuition with formal rigor—marks a significant advancement in how AI understands and constructs mathematical proofs.
📈 State-of-the-Art Performance
DeepSeek-Prover-V2-671B delivers exceptional results across benchmark datasets:
- 88.9% pass rate on the MiniF2F-test
- Solves 49 out of 658 problems from PutnamBench, outperforming all previous models in neural theorem proving
🧪 ProverBench: A New Benchmark for Formal Math
Accompanying the model is ProverBench, a newly introduced benchmark dataset consisting of 325 formalized math problems. This includes:
- 15 problems from recent AIME competitions
- 310 problems spanning Number Theory, Algebra, Linear Algebra, Calculus, and more
🔓 Open Access for Researchers
Both versions of the model are now available on Hugging Face:
- DeepSeek-Prover-V2-671B (671 billion parameters)
- DeepSeek-Prover-V2-7B, a lighter variant with extended 32K token context, built on DeepSeek-Prover-V1.5-Base
This open-source release empowers researchers, developers, and mathematicians to explore new frontiers in AI-assisted theorem proving and automated formal reasoning.
🚀 A Milestone in Formal Mathematics and AI
DeepSeek-Prover-V2 represents a major milestone in applying large language models to formal mathematical domains. By seamlessly integrating informal reasoning and formal proof synthesis, it opens up exciting new possibilities for:
- Automated theorem discovery
- Formal verification of scientific work
- Next-generation educational tools in mathematics
Whether you’re a researcher in AI, a formal methods expert, or a math enthusiast, this release is a compelling glimpse into the future of machine reasoning.