Providers and ModelsDeepSeek

DeepSeek Prover V2

DeepSeek Prover V2
DeepSeek · Text Generation
POST /v1/chat/completions

Open-source LLM specialized in formal theorem proving in Lean 4, built on a recursive theorem-proving pipeline.

At a glance

FieldValue
Model iddeepseek-prover-v2
Input modalitiesText
Output modalitiesText
Context window-
Weight precision-
Featuresmath, reasoning
Native inferenceNo
NewNo
Supported endpointsPOST /v1/chat/completions, POST /v1/responses

Pricing

ChargeSpecRate
Per Messagefixed$0.020

Example request

$curl https://api.empiriolabs.ai/v1/chat/completions \
>  -H 'Authorization: Bearer $EMPIRIOLABS_API_KEY' \
>  -H 'Content-Type: application/json' \
>  -d '{"model": "deepseek-prover-v2", "messages": [{"role":"user","content":"Hello"}]}'

Parameters

This model accepts the standard chat completion parameters (see the API reference).

Notes

Specialized for formal theorem proving in Lean 4. Routed through OpenRouter.

Machine-readable schema: GET https://api.empiriolabs.ai/v1/models/deepseek-prover-v2.