Lean Theorem Prover MCP
Listed on its own since 2026-09-25. Until then it was part of iflow-mcp-ooo0ooo-lean-lsp-mcp, where its earlier checks remain.
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":"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` and `Lean Hammer` 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`) for local search and source scanning (`lean_verify` warnings). ### 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` ### 1b. Alternative: Install with Nix If you use Nix, you can install the package direct…
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.