D

Deepseek Prover V2 671B

Developed by deepseek-ai
An open-source large language model designed for Lean 4 formal theorem proving, collecting data through recursive theorem proving processes, combining informal and formal mathematical reasoning.
Downloads 9,693
Release Time : 4/30/2025

Model Overview

DeepSeek-Prover-V2 is an open-source large language model specifically designed for Lean 4 formal theorem proving. Its initial data is collected through a recursive theorem proving process powered by DeepSeek-V3. This model unifies informal and formal mathematical reasoning into a single framework and achieves state-of-the-art performance in neural theorem proving.

Model Features

Recursive Theorem Proving Process
Collects data through a recursive theorem proving process, using DeepSeek-V3 as a unified tool for subgoal decomposition and formalization to generate cold-start reasoning data.
Reinforcement Learning
After fine-tuning the proof model on synthetic cold-start data, a reinforcement learning phase further enhances its ability to connect informal reasoning with formal proof construction.
High Performance
Achieves an 88.9% pass rate on the MiniF2F test and solves 49 problems from PutnamBench.

Model Capabilities

Formal theorem proving
Mathematical reasoning
Subgoal decomposition
Lean 4 code generation

Use Cases

Mathematical Formalization
MiniF2F Problem Solving
Using DeepSeek-Prover-V2 to solve formal mathematical problems in the MiniF2F dataset.
Achieves an 88.9% pass rate on the MiniF2F test.
PutnamBench Problem Solving
Using DeepSeek-Prover-V2 to solve mathematical problems in PutnamBench.
Solves 49 problems from PutnamBench.
Education
Textbook Problem Formalization
Using DeepSeek-Prover-V2 to formalize textbook math problems into Lean 4 code.
The ProverBench dataset contains 325 formalized problems.
Featured Recommended AI Models
AIbase
Empowering the Future, Your AI Solution Knowledge Base
© 2025AIbase