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.

uv sync

Configuration

You need an Aristotle API key. Set it in your environment:

export ARISTOTLE_API_KEY="your-api-key-here"

Running the Server

Run the server using uv:

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.