Fournisseurs et modèlesDeepSeek

DeepSeek Prover V2

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

LLM open source spécialisé dans la démonstration formelle de théorèmes en Lean 4, basé sur un pipeline récursif de démonstration de théorèmes.

En un coup d’œil

TerrainValeur
Identifiant de modèledeepseek-prover-v2
Date de sortie du modèle2025-04-30
Modalités d’entréeTexte
Modalités de sortieTexte
Fenêtre de contexte-
Précision du poids-
CaractéristiquesMathématiques, raisonnement
Inférence autochtoneNon
NouveauNon
Points de terminaison pris en chargePOST /v1/chat/completions, POST /v1/responses

Tarification

ChargeSpecTaux
Par messagefixé$0.020

Exemple de demande

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

Paramètres

This modèle accepte les paramètres standards de complétion du chat (voir la référence API.

Notes

Spécialisé dans la démonstration de théorèmes formels en Lean 4. Acheminé via OpenRouter.

_Machine schéma lisible: _ GET https://api.empiriolabs.ai/v1/models/deepseek-prover-v2.