Aristotle MCP Server
# Aristotle MCP Server
A minimal Model Context Protocol (MCP) server for the Aristotle API, enabling LLMs to prove theorems in Lean and formalize mathematical problems.
## Installation
This project uses `uv` for dependency management.
```bash
uv sync
```
## Configuration
You need an Aristotle API key. Set it in your environment:
```bash
export ARISTOTLE_API_KEY="your-api-key-here"
```
## Running the Server
Run the server using `uv`:
```bash
uv run main.py
```
This will start the MCP server over stdio.
## Tools
- `prove_lean_file(file_path)`: Submit a Lean file for proving. Returns Project ID.
- `prove_informal(file_path, formal_context_path)`: Submit a natural language problem. Returns Project ID.
- `prove_lean_code(lean_code)`: Submit Lean code string. Returns Project ID.
- `prove_informal_text(text, formal_context_path)`: Submit natural language string. Returns Project ID.
- `get_project_status(project_id, save_solution_to)`: Check status and retrieve solution code.
- `list_recent_projects()`: List recent projects.
## Resources
- `aristotle://projects`: JSON list of recent projects.
- `aristotle://projects/{project_id}`: Detailed status and content of a specific project.
TDQS
Scored across 6 tools
There is significant overlap between prove_informal, prove_informal_text, prove_lean_code, and prove_lean_file, as all four handle proof submission with only minor input format differences. This creates ambiguity for an agent trying to select the right tool, especially between the informal text and file variants. The get_project_status and list_recent_projects are distinct, but the core proving tools are poorly differentiated.
The naming follows a consistent snake_case pattern throughout, which is good. However, there is a minor inconsistency: most tools use verb_noun (e.g., get_project_status, prove_informal), but list_recent_projects uses verb_adjective_noun, which slightly deviates from the pattern. Overall, the naming is mostly predictable and readable.
With 6 tools, the count is reasonable for a server focused on mathematical proof automation. It covers key operations like project listing, status checking, and proof submission. However, the set feels slightly thin as it lacks tools for managing or updating existing projects, but it is well-scoped for the core workflow.
The tool surface covers basic submission and status checking, but there are notable gaps. For example, there are no tools to update, cancel, or delete projects, and no way to retrieve proof results beyond status. This could lead to dead ends for agents needing to manage project lifecycles, though core submission workflows are supported.