MCP server that allows agentic interaction with the Lean theorem prover via the Language Server Protocol using [leanclient](https://github.com/oOo0oOo/leanclie
How to install lean-lsp-mcp?
ooo0ooo/lean-lsp-mcp
$git clone https://github.com/ooo0ooo/lean-lsp-mcpInstalls into the current project.
›Prefer a prompt? Paste this to your agent
Install lean-lsp-mcp by running `git clone https://github.com/ooo0ooo/lean-lsp-mcp`, then use it for the current task and follow its documentation at https://github.com/ooo0ooo/lean-lsp-mcp.
README.md
| 1 | <h1 align="center"> |
| 2 | lean-lsp-mcp |
| 3 | </h1> |
| 4 | |
| 5 | <h3 align="center">Lean Theorem Prover MCP</h3> |
| 6 | |
| 7 | <p align="center"> |
| 8 | <a href="https://pypi.org/project/lean-lsp-mcp/"> |
| 9 | <img src="https://img.shields.io/pypi/v/lean-lsp-mcp.svg" alt="PyPI version" /> |
| 10 | </a> |
| 11 | <a href=""> |
| 12 | <img src="https://img.shields.io/github/last-commit/oOo0oOo/lean-lsp-mcp" alt="last update" /> |
| 13 | </a> |
| 14 | <a href="https://github.com/oOo0oOo/lean-lsp-mcp/blob/master/LICENSE"> |
| 15 | <img src="https://img.shields.io/github/license/oOo0oOo/lean-lsp-mcp.svg" alt="license" /> |
| 16 | </a> |
| 17 | </p> |
| 18 | |
| 19 | 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. |
| 20 | |
| 21 | ## Key Features |
| 22 | |
| 23 | * **Rich Lean Interaction**: Access diagnostics, goal states, term information, hover documentation and more. |
| 24 | * **External Search Tools**: Use `LeanSearch`, `Loogle`, `Lean Finder`, `Lean Hammer` and `Lean State Search` to find relevant theorems and definitions. |
| 25 | * **Easy Setup**: Simple configuration for various clients, including VSCode, Cursor and Claude Code. |
| 26 | |
| 27 | ## Setup |
| 28 | |
| 29 | ### Overview |
| 30 | |
| 31 | 1. Install [uv](https://docs.astral.sh/uv/getting-started/installation/), a Python package manager. |
| 32 | 2. Make sure your Lean project builds quickly by running `lake build` manually. |
| 33 | 3. Configure your IDE/Setup |
| 34 | 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). |
| 35 | |
| 36 | ### 1. Install uv |
| 37 | |
| 38 | [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` |
| 39 | |
| 40 | ### 1b. Alternative: Install with Nix |
| 41 | |
| 42 | If you use Nix, you can install the package directly from GitHub: |
| 43 | |
| 44 | ```bash |
| 45 | nix profile install github:oOo0oOo/lean-lsp-mcp |
| 46 | ``` |
| 47 | |
| 48 | Or run it without installing: `nix run github:oOo0oOo/lean-lsp-mcp`. |
| 49 | |
| 50 | This provides the MCP server only. You still need a Lean toolchain (`elan`/`lake`) for your project, same as the `uv` setup below. |
| 51 | |
| 52 | ### 2. Run `lake build` |
| 53 | |
| 54 | `lean-lsp-mcp` will run `lake serve` in the project root to use the language server (for most tools). Some clients (e.g. Cursor) might timeout during this process. Therefore, it is recommended to run `lake build` manually before starting the MCP. This ensures a faster build time and avoids timeouts. |
| 55 | |
| 56 | ### 3. Configure your IDE/Setup |
| 57 | |
| 58 | <details> |
| 59 | <summary><b>VSCode (Click to expand)</b></summary> |
| 60 | One-click config setup: |
| 61 | |
| 62 | [](https://insiders.vscode.dev/redirect/mcp/install?name=lean-lsp&config=%7B%22command%22%3A%22uvx%22%2C%22args%22%3A%5B%22lean-lsp-mcp%22%5D%7D) |
| 63 | |
| 64 | [](https://insiders.vscode.dev/redirect/mcp/install?name=lean-lsp&config=%7B%22command%22%3A%22uvx%22%2C%22args%22%3A%5B%22lean-lsp-mcp%22%5D%7D&quality=insiders) |
| 65 | |
| 66 | OR using the setup wizard: |
| 67 | |
| 68 | Ctrl+Shift+P > "MCP: Add Server..." > "Command (stdio)" > "uvx lean-lsp-mcp" > "lean-lsp" (or any name you like) > Global or Workspace |
| 69 | |
| 70 | OR manually adding config by opening `mcp.json` with: |
| 71 | |
| 72 | Ctrl+Shift+P > "MCP: Open User Configuration" |
| 73 | |
| 74 | and adding the following |
| 75 | |
| 76 | ```jsonc |
| 77 | { |
| 78 | "servers": { |
| 79 | "lean-lsp": { |
| 80 | "type": "stdio", |
| 81 | "command": "uvx", |
| 82 | "args": [ |
| 83 | "lean-lsp-mcp" |
| 84 | ] |
| 85 | } |
| 86 | } |
| 87 | } |
| 88 | ``` |
| 89 | |
| 90 | If you installed VSCode on Windows and are using WSL2 as your development environment, you may need to use this config instead: |
| 91 | |
| 92 | ```jsonc |
| 93 | { |
| 94 | "servers": { |
Related
6 picksType
- chrome-devtools-mcpMCP server for Chrome DevToolsJul 2026
- desktopcommandermcpMCP server for terminal commands, file operations, and process managementJul 2026
- langfuse-mcpLangfuse MCP server for accessing and analyzing telemetry data via natural languageJun 2026
- mcp_debugPostman for your MCP server with a Claude chat that calls your toolsJun 2025
- tauri-plugin-mcpAllows AI agents (e.g., Cursor, Claude Code) to debug within Tauri apps via screenshot capture, window management, DOM access, and simulated user inputs.Jul 2026
- toon-memoryMCP server giving AI coding agents offline, token-efficient persistent memory — 21 tools, 80% fewer tool calls, recall decisions, patterns, and bugs across sessions. No LLM, no server; works with 15+ agents.Jul 2026
