DeepSeek logo

DeepSeek-Prover-V2

DeepSeekOpen WeightsPending Human Review

DeepSeek-Prover-V2 is a family of language models specialized for formal theorem proving in Lean 4. It uses subgoal decomposition and reinforcement learning to convert difficult proof tasks into verifiable intermediate steps. The 671B checkpoint is trained from DeepSeek-V3-Base, while the 7B checkpoint builds on Prover-V1.5-Base and supports a 32K context. The published model repository provides weights, inference instructions, and proof benchmarks. Formal validity depends on checking generated code in the Lean environment and matching its theorem statement.

2025-04-30
671B and 7B
Mixture of Experts (671B tier); dense Transformer (7B tier)
MIT

Specifications

Parameters
671B and 7B
Architecture
Mixture of Experts (671B tier); dense Transformer (7B tier)
License
MIT
Type
text
Modalities
text

Benchmark Scores

Advanced Specifications

Model Family
DeepSeek
API Access
Not Available
Chat Interface
Not Available
Variants
DeepSeek-Prover-V2-671BDeepSeek-Prover-V2-7B

Capabilities & Limitations

Capabilities
Lean 4 theorem provingformal proof generationsubgoal decomposition
Known Limitations
Proofs need verification in the intended Lean environment.The two size tiers have different bases and context limits.
Notable Use Cases
formal mathematicsproof-assistant automationtheorem-proving research

Related Models