Aristotle MCP

What it does

Wraps the Aristotle API to give LLMs the ability to interact with formal verification systems. It enables AI to prove mathematical theorems in the Lean language and convert informal mathematical problems into formal specifications.

Tools

• prove_lean_file: Submits a Lean file for proving and returns a Project ID.
• prove_informal: Submits a natural language problem with formal context for proving.
• prove_lean_code: Submits raw Lean code strings for proving.
• prove_informal_text: Submits natural language text for formalization.
• get_project_status: Checks the progress and retrieves the solution code for a project.
• list_recent_projects: Lists all recent proof projects.

Installation

Add the following to your claude_desktop_config.json:

{
  "mcpServers": {
    "aristotle-mcp": {
      "command": "uv",
      "args": ["run", "--path", "/path/to/aristotle-mcp", "main.py"],
      "env": {
        "ARISTOTLE_API_KEY": "your-api-key-here"
      }
    }
  }
}

Supported hosts

• Claude Desktop