MCP server · Harmonic

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.

Open docs → Harmonic provider profile

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.

Provider: Harmonic Type: Documentation link Transport: stdio Host: github.com

Documentation

https://github.com/septract/lean-aristotle-mcp

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.