gleachkr/aristotle-mcp
3.3
If you are the rightful owner of aristotle-mcp and would like to certify it and/or have it hosted online, please leave a comment on the right or send an email to dayong@mcphub.com.
Aristotle MCP Server is a minimal Model Context Protocol server designed for the Aristotle API, facilitating theorem proving in Lean and formalizing mathematical problems.
Tools
6
Resources
0
Prompts
0
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.