Schema | Aristotle MCP Server

Aristotle MCP Server

Describes the environment variables required to run the server.

Name	Required	Description	Default
`ARISTOTLE_API_KEY`	Yes	Your Aristotle API key

Guidance the server publishes about itself, which clients place ahead of the tool catalog so the model reads it before choosing anything.

This server publishes no instructions, or was last inspected before Glama recorded them.

Server capabilities have not been inspected yet.

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.

Interactive templates invoked by user choice

Name	Description
No prompts

Contextual data attached and managed by the client

Name	Description
`list_projects_resource`	A live list of the user's recent projects.

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