English Français العربية

com.axiomatic-ai/prover

Registre officiel Autres

Lean 4 MCP server: compile, prove theorems, and formalize math with Mathlib.

Code source Documentation

Installation

Ajoutez ceci à la configuration MCP de votre client (Claude Desktop : claude_desktop_config.json ; Cursor : .cursor/mcp.json ; VS Code et les autres utilisent la même forme « mcpServers »).

Remote (streamable-http)
Claude Code 
claude mcp add --transport http prover 'https://prover.axiomatic-ai.com/mcp/'
Configuration JSON (Claude Desktop, Cursor, VS Code) 
{
    "mcpServers": {
        "prover": {
            "type": "http",
            "url": "https://prover.axiomatic-ai.com/mcp/"
        }
    }
}

Documentation

Tirée du README du projet sur GitHub, actualisée chaque semaine. Les liens ouvrent GitHub.

Sommaire
  1. Axiomatic Prover — MCP Server
  2. Connect
  3. Tools
  4. Links

Axiomatic Prover — MCP Server

Lean 4 MCP server: compile and prove theorems with Mathlib.

Connect

Add to your MCP client (e.g. Claude Desktop claude_desktop_config.json):

{
  "mcpServers": {
    "ax-prover": {
      "type": "streamable-http",
      "url": "https://prover.axiomatic-ai.com/mcp/"
    }
  }
}

Authentication uses OAuth 2.1 via GitHub — your MCP client handles the flow automatically.

Tools

Submit (async — returns a job_id)
ToolDescription
lean4_buildCompile Lean 4 source code in a Mathlib-enabled sandbox. Code is sent to external cloud services for compilation; if proving, also for AI processing.
lean4_prove_theoremsAutomatically prove Lean 4 theorems that contain sorry. Code is sent to external cloud services for compilation and AI proving.
Poll
ToolDescription
lean4_get_job_statusPoll for the status and result of any ax-prover job.

All submit tools are asynchronous — they return a job_id immediately. Poll with lean4_get_job_status(job_id) until status is completed or failed.

Questions fréquentes

Qu'est-ce que com.axiomatic-ai/prover ?

Lean 4 MCP server: compile, prove theorems, and formalize math with Mathlib.

Comment installer com.axiomatic-ai/prover ?

Il fonctionne comme serveur distant. Dans Claude Code : claude mcp add --transport http prover 'https://prover.axiomatic-ai.com/mcp/'. Pour les autres clients, collez la configuration JSON de cette page dans leurs réglages MCP.

Faut-il une clé API pour com.axiomatic-ai/prover ?

Son entrée au registre n'indique aucune clé ni secret obligatoire. Certaines fonctions peuvent tout de même demander un compte auprès du service auquel il se connecte.

com.axiomatic-ai/prover est-il open source ?

Son code est public sur GitHub, mais le dépôt ne déclare pas de licence standard.

Qui maintient com.axiomatic-ai/prover ?

Il est publié par Axiomatic-AI. AI.tn le référence sans le maintenir ni le recommander.

Issu du registre MCP officiel. Être listé n'est pas une recommandation : vérifiez le code et les permissions d'un serveur avant de lui donner accès à vos données.