The right model for every task. Try Nexus
Docs
Log in
Get started
Deepseek logo

DeepSeek Prover V2

Ready
model path:accounts/fireworks/models/deepseek-prover-v2
Deploy on demand

DeepSeek-Prover-V2, an open-source large language model designed for formal theorem proving in Lean 4, with initialization data collected through a recursive theorem proving pipeline powered by DeepSeek-V3.

DeepSeek Prover V2 API Features

On-demand Deployment

Docs

On-demand deployments allow you to use DeepSeek Prover V2 on dedicated GPUs with Fireworks' high-performance serving stack with high reliability and no rate limits.

Metadata

State
Ready
Created on
1 MAY, 2025
Kind
Base model
Provider
Deepseek
Huggingface
deepseek-ai/DeepSeek-Prover-V2-671B

Specifications

Calibrated
Yes
Mixture-of-Experts
Yes
Parameters
671B

Supporting Functionality

Fine-tuning
Not Supported
Serverless
Not Supported
Context Length
163k tokens
Function Calling
Not Supported
Embeddings
Not Supported
Rerankers
Not Supported
Supporting image input
Not Supported

DeepSeek Prover V2 FAQs

DeepSeek Prover V2 is an open-source large-language model designed for automated formal-theorem proving in Lean 4, created by DeepSeek AI. It is trained via a recursive proof-generation pipeline powered by DeepSeek-V3, integrating informal reasoning with formal proof construction.