Proveedores y modelosDeepSeek

DeepSeek Prover V2

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

LLM de código abierto especializado en demostración formal de teoremas en Lean 4, basado en una cadena recursiva de demostración de teoremas.

A simple vista

CampoValor
ID de modelodeepseek-prover-v2
Fecha de lanzamiento del modelo2025-04-30
Modalidades de entradaTexto
Modalidades de salidaTexto
Ventana de contexto-
Precisión del peso-
CaracterísticasMatemáticas, razonamiento
Inferencia nativaNo
NuevoNo
Puntos finales soportadosPOST /v1/chat/completions, POST /v1/responses

Precios

CargaEspecificacionesTarifa
Por mensajeFijado$0.020

Solicitud de ejemplo

$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"}]}'

Parámetros

This modelo acepta los parámetros estándar de finalización de chat (véase la referencia API.

Notas

Especializada en demostración formal de teoremas en Lean 4. Enrutado a través de OpenRouter.

Machine-legible esquema: GET https://api.empiriolabs.ai/v1/models/deepseek-prover-v2.