DeepSeek-Prover-V2
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