lean-aristotle-mcp
Harmonic does not (as of this pass) publish an official MCP server for the Aristotle API. A working community MCP server, lean-aristotle-mcp (maintained by GitHub user septract), wraps the Aristotle cloud API so AI assistants can invoke theorem proving during Lean development. It authenticates with a user's own Aristotle API key. Recorded here as a real, usable server for this API and clearly marked community/non-official — not a Harmonic product.
One-click install for Cursor, VS Code, Claude, and 20+ other MCP clients, powered by API Commons MCP Install — visit install.apicommons.org for more information.
Documentation
Documentation link · transport stdio
Tools
prove— Fill `sorry` statements in a Lean code snippet.prove_file— Prove all sorries in a Lean file with automatic import resolution.formalize— Convert natural-language mathematics into Lean 4.check_proof— Poll the status of an async prove job.check_prove_file— Poll the status of an async prove_file job.check_formalize— Poll the status of an async formalize job.
About MCP
The Model Context Protocol (MCP) is an open protocol Anthropic introduced for connecting LLM-based agents to external tools and data sources. Providers publish MCP servers that expose their API surface as structured, discoverable tools — an MCP-compatible client (Claude Desktop, Cursor, Cline, Continue, etc.) can connect to the server and call its tools without any per-provider integration code.
Browse every MCP server on the APIs.io network or compare with the broader Agent Skill surfaces of the same providers.
Work with this as data
Every MCP server here is available over the APIs.io API and to AI agents over MCP.