oOo0oOo/lean-lsp-mcp

Lean Theorem Prover MCP
MCP server that allows agentic interaction with the Lean theorem prover via the Language Server Protocol using 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, 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 (rg) for local search and source scanning (lean_verify warnings).
1. Install uv
Install uv 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 directly from GitHub:
Or run it without installing: nix run github:oOo0oOo/lean-lsp-mcp.
This provides the MCP server only. You still need a Lean toolchain (elan/lake) for your project, same as the uv setup below.
2. Run lake build
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.
3. Configure your IDE/Setup
VSCode (Click to expand)
One-click config setup:
OR using the setup wizard:
Ctrl+Shift+P > "MCP: Add Server..." > "Command (stdio)" > "uvx lean-lsp-mcp" > "lean-lsp" (or any name you like) > Global or Workspace
OR manually adding config by opening mcp.json with:
Ctrl+Shift+P > "MCP: Open User Configuration"
and adding the following
If you installed VSCode on Windows and are using WSL2 as your development environment, you may need to use this config instead:
If that doesn't work, you can try cloning this repository and replace "lean-lsp-mcp" with "/path/to/cloned/lean-lsp-mcp".
Cursor (Click to expand)
1. Open MCP Settings (File > Preferences > Cursor Settings > MCP)
2. "+ Add a new global MCP Server" > ("Create File")
3. Paste the server config into mcp.json file:
Claude Code (Click to expand)
Run one of these commands in the root directory of your Lean project (where lakefile.toml is located):
You can find more details about MCP server configuration for Claude Code here.
Mistral Vibe (Click to expand)
(These instructions cover Mac/Linux.)
1. Edit ~/.vibe/config.toml.
2. Paste the following into the file (e.g. at the end):
If there are no existing MCP servers, you may have to remove mcp_servers = [].
4. Install ripgrep (optional but recommended)
For the local search tool lean_local_search, install ripgrep (rg) and make sure it is available in your PATH.
5. Install the Lean 4 skill (optional but recommended)
With any agentic coding platform such as Claude Code or Codex, you can install the Agentic Coding Skill: Lean 4 Theorem Proving. This skill provides additional prompts and templates for interacting with Lean 4 projects, including guidance on using lean-lsp-mcp.
MCP Tools
List of available tools
See Tools documentation for the full list of available tools.
Disabling Tools
Many clients allow the user to disable specific tools manually (e.g. lean_build).
**VSCode**: Click on the Wrench/Screwdriver icon in the chat.
**Cursor**: In "Cursor Settings" > "MCP" click on the name of a tool to disable it (strikethrough).
You can also disable tools at server startup:
- LEAN_MCP_DISABLED_TOOLS: Comma-separated tool names (for example lean_run_code,lean_build).
- LEAN_MCP_INSTRUCTIONS: Replacement server instructions string.
- LEAN_MCP_TOOL_DESCRIPTIONS: JSON object to override tool descriptions.