Aristotle MCP Server
Server Configuration
Describes the environment variables required to run the server.
| Name | Required | Description | Default |
|---|---|---|---|
| ARISTOTLE_API_KEY | Yes | Your Aristotle API key |
Capabilities
Server capabilities have not been inspected yet.
Tools
Functions exposed to the LLM to take actions
| Name | Description |
|---|---|
| prove_lean_fileB | Submits a local Lean file to Aristotle to fill in 'sorry' placeholders. Returns the Project ID immediately. |
| prove_informalC | Submits a file containing natural language mathematics (Text, Markdown, LaTeX) to be formalised and proved. Returns the Project ID immediately. |
| get_project_statusB | Checks the status of a specific Aristotle project. Returns full project data including solution if available. |
| list_recent_projectsB | Lists the most recent projects submitted to Aristotle. |
| prove_lean_codeB | Submits Lean code directly to Aristotle to fill in 'sorry' placeholders. Returns the Project ID immediately. |
| prove_informal_textC | Submits natural language mathematics directly to be formalized and proved. Returns the Project ID immediately. |
Prompts
Interactive templates invoked by user choice
| Name | Description |
|---|---|
No prompts | |
Resources
Contextual data attached and managed by the client
| Name | Description |
|---|---|
| list_projects_resource | A live list of the user's recent projects. |
Latest Blog Posts
MCP directory API
We provide all the information about MCP servers via our MCP API.
curl -X GET 'https://glama.ai/api/mcp/v1/servers/gleachkr/aristotle-mcp'
If you have feedback or need assistance with the MCP directory API, please join our Discord server