Lean Theorem Prover MCP
Until 2026-09-25 this record combined several servers published from one repository. The others now have records of their own: lean-lsp-mcp. Checks from before that date include them.
Wellknown found it in public sources; nobody has proven control of it yet. Claiming takes one click if the repository is under your GitHub account, or a small file on your domain otherwise. Verified owners get the badge, 15-minute checks, status alerts, edits that outrank crawled data, and a ranking boost.
Agents can do it too: POST https://wellknown.network/api/v1/claims with {"agent":"iflow-mcp-ooo0ooo-lean-lsp-mcp","method":"well_known_file"} — machine-readable steps at claim.json, guide at /docs/claim.
Everything here was measured by our prober or read from a registry. Nothing is self-reported.
Attributed to the source that supplied each field. Treated as claims, not facts.
<h1 align="center"> lean-lsp-mcp </h1> <h3 align="center">Lean Theorem Prover MCP</h3> <p align="center"> <a href="https://pypi.org/project/lean-lsp-mcp/"> <img src="https://img.shields.io/pypi/v/lean-lsp-mcp.svg" alt="PyPI version" /> </a> <a href=""> <img src="https://img.shields.io/github/last-commit/oOo0oOo/lean-lsp-mcp" alt="last update" /> </a> <a href="https://github.com/oOo0oOo/lean-lsp-mcp/blob/master/LICENSE"> <img src="https://img.shields.io/github/license/oOo0oOo/lean-lsp-mcp.svg" alt="license" /> </a> </p> MCP server that allows agentic interaction with the [Lean theorem prover](https://lean-lang.org/) via the [Language Server Protocol](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/) using [leanclient](https://github.com/oOo0oOo/leanclient). This server provides a range of tools for LLM agents to understand, analyze and interact with Lean projects. ## Key Features * **Rich Lean Interaction**: Access diagnostics, goal states, term information, hover documentation and more. * **External Search Tools**: Use `LeanSearch`, `Loogle`, `Lean Finder`, `Lean Hammer` and `Lean State Search` to find relevant theorems and definitions. * **Easy Setup**: Simple configuration for various clients, including VSCode, Cursor and Claude Code. ## Setup ### Overview 1. Install [uv](https://docs.astral.sh/uv/getting-started/installation/), a Python package manager. 2. Make sure your Lean project builds quickly by running `lake build` manually. 3. Configure your IDE/Setup 4. (Optional, highly recommended) Install [ripgrep](https://github.com/BurntSushi/ripgrep?tab=readme-ov-file#installation) (`rg`) to reduce hallucinations using local search. ### 1. Install uv [Install uv](https://docs.astral.sh/uv/getting-started/installation/) for your system. On Linux/MacOS: `curl -LsSf https://astral.sh/uv/install.sh | sh` ### 2. Run `lake build` `lean-lsp-mcp` will run `lake serve` in the project root to u…
Mapped onto the structured taxonomy from declared text and observed tool names. Confidence shown for derived entries.
Every source is kept verbatim. Field changes are logged as events.