Aristotle MCP Server
Enables LLMs to prove theorems in Lean and formalize mathematical problems using the Aristotle API, supporting both formal Lean code and natural language problem submissions.
README
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.
Recommended Servers
playwright-mcp
A Model Context Protocol server that enables LLMs to interact with web pages through structured accessibility snapshots without requiring vision models or screenshots.
Audiense Insights MCP Server
Enables interaction with Audiense Insights accounts via the Model Context Protocol, facilitating the extraction and analysis of marketing insights and audience data including demographics, behavior, and influencer engagement.
Magic Component Platform (MCP)
An AI-powered tool that generates modern UI components from natural language descriptions, integrating with popular IDEs to streamline UI development workflow.
VeyraX MCP
Single MCP tool to connect all your favorite tools: Gmail, Calendar and 40 more.
Kagi MCP Server
An MCP server that integrates Kagi search capabilities with Claude AI, enabling Claude to perform real-time web searches when answering questions that require up-to-date information.
graphlit-mcp-server
The Model Context Protocol (MCP) Server enables integration between MCP clients and the Graphlit service. Ingest anything from Slack to Gmail to podcast feeds, in addition to web crawling, into a Graphlit project - and then retrieve relevant contents from the MCP client.
Qdrant Server
This repository is an example of how to create a MCP server for Qdrant, a vector search engine.
Neon Database
MCP server for interacting with Neon Management API and databases
Exa Search
A Model Context Protocol (MCP) server lets AI assistants like Claude use the Exa AI Search API for web searches. This setup allows AI models to get real-time web information in a safe and controlled way.
E2B
Using MCP to run code via e2b.