gleachkr/aristotle-mcp
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
Functions exposed to the LLM to take actions
prove_lean_file
Submit a Lean file for proving. Returns Project ID.
prove_informal
Submit a natural language problem. Returns Project ID.
prove_lean_code
Submit Lean code string. Returns Project ID.
prove_informal_text
Submit natural language string. Returns Project ID.
get_project_status
Check status and retrieve solution code.
list_recent_projects
List recent projects.
Prompts
Interactive templates invoked by user choice
No prompts
Resources
Contextual data attached and managed by the client