DeepSeek Prover v2: A New Era of AI in Mathematical Proving
In recent years, we have witnessed the rapid development of artificial intelligence in many fields, but mathematics—especially the formal proving of complex theorems—remained for a long time the domain of human intellect. However, this is beginning to change with the arrival of the DeepSeek Prover v2 model, introduced by the Chinese company DeepSeek AI. This open-source model, designed specifically for formal proving in the Lean 4 environment, represents a fundamental shift in the automation and formalization of mathematical proofs using AI.
Who Is Behind DeepSeek Prover v2 and How the Model Was Developed
The DeepSeek AI team is behind the development of DeepSeek Prover v2, focusing on the development of large language models and their application in various fields. The model was created in response to the growing need for automation in mathematical research, where formal verification of proofs is often time-consuming and requires extensive knowledge. DeepSeek AI leveraged its experience in developing large language models and combined it with state-of-the-art techniques in the field of formal proving.
The development of DeepSeek Prover v2 was based on a hybrid training approach. The model was trained not only on extensive mathematical data, but also on synthetic data generated using previous versions of the model (such as DeepSeek-V3), which helped break down complex problems into smaller subtasks. So-called chain-of-thought learning also played an important role, enabling the model to follow the logical structure of proofs step by step. The result is a model that can not only generate formal proofs, but also break them down and synthesize them into coherent solutions.
Key Features and Architecture
DeepSeek Prover v2 is built on a Mixture-of-Experts (MoE) architecture with a total of 671 billion parameters, of which approximately 37 billion parameters are activated during a single inference step. This architecture enables efficient processing of complex and multi-step mathematical tasks that require deep logical reasoning. One of the model’s most notable features is its enormous context window—up to 163,840 tokens. This is several times larger than that of most competing models and allows DeepSeek Prover to work with very long and complex mathematical texts without losing context. The model is designed to generate end-to-end formal proofs in Lean 4, meaning that it can both break down complex problems into subgoals and synthesize these partial proofs into a complete formal solution.
Results and Comparison with the Competition
DeepSeek Prover v2 achieves leading results on standard benchmarks in mathematical proving. For example, it achieved an 88.9% success rate on the MiniF2F test, placing it among the best open models currently available. On PutnamBench, which contains some of the most difficult mathematical problems, it solved 49 out of 658 problems. The model also handled several current problems from the AIME (American Invitational Mathematics Examination).
Compared with competing models such as Google’s Minerva or Meta’s LeanDojo, DeepSeek Prover v2 stands out primarily for its model size, context window length, and emphasis on fully automated proof construction. While other models often focus only on translating informal mathematics into a formal language, DeepSeek Prover v2 handles the entire process, from the problem statement to a complete formal proof.
Another key aspect of DeepSeek Prover v2 is its openness. The model is available under the MIT license, allowing it to be used in both academic and commercial environments. The code and model weights are freely available for download, for example, on the Hugging Face platform or directly from DeepSeek AI’s GitHub.
Significance for Mathematics and the Future
DeepSeek Prover v2 represents a significant step toward automating mathematical research. It enables faster and more reliable verification of complex proofs, which can accelerate the discovery of new insights and increase confidence in mathematical results. The model can serve not only as a tool for mathematicians, but also as a research platform for further development of AI in the field of formal proving. DeepSeek Prover v2 shows that the gap between informal mathematical reasoning and the fully formalized construction of proofs is rapidly narrowing. As these models’ capabilities grow, new possibilities are opening up for collaboration between humans and AI in mathematics and other exact sciences.
