Aristotle MCP

Ce qu'il fait

Encapsule l'API Aristotle pour donner aux LLM la capacité d'interagir avec des systèmes de vérification formelle. Il permet à l'IA de prouver des théorèmes mathématiques dans le langage Lean et de convertir des problèmes mathématiques informels en spécifications formelles.

Outils

• prove_lean_file : Soumet un fichier Lean pour preuve et renvoie un ID de projet.
• prove_informal : Soumet un problème en langage naturel avec un contexte formel pour preuve.
• prove_lean_code : Soumet des chaînes de code Lean brutes pour preuve.
• prove_informal_text : Soumet un texte en langage naturel pour formalisation.
• get_project_status : Vérifie la progression et récupère le code de solution pour un projet.
• list_recent_projects : Liste tous les projets de preuve récents.

Installation

Ajoutez les éléments suivants à votre fichier claude_desktop_config.json :

{
  "mcpServers": {
    "aristotle-mcp": {
      "command": "uv",
      "args": ["run", "--path", "/path/to/aristotle-mcp", "main.py"],
      "env": {
        "ARISTOTLE_API_KEY": "votre-clé-api-ici"
      }
    }
  }
}

Hôtes supportés

• Claude Desktop