Lean LSP

lean-lsp-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:

nix profile install github:oOo0oOo/lean-lsp-mcp

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

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

{
    "servers": {
        "lean-lsp": {
            "type": "stdio",
            "command": "uvx",
            "args": [
                "lean-lsp-mcp"
            ]
        }
    }
}

If you installed VSCode on Windows and are using WSL2 as your development environment, you may need to use this config instead:

{
    "servers": {
        "lean-lsp": {
            "type": "stdio",
            "command": "wsl.exe",
            "args": [
                "uvx",
                "lean-lsp-mcp"
            ]
        }
    }
}

If that doesn't work, you can try cloning this repository and replace "lean-lsp-mcp" with "/path/to/cloned/lean-lsp-mcp".

1. Open MCP Settings (File > Preferences > Cursor Settings > MCP)

1. "+ Add a new global MCP Server" > ("Create File")

1. Paste the server config into mcp.json file:

{
    "mcpServers": {
        "lean-lsp": {
            "command": "uvx",
            "args": ["lean-lsp-mcp"]
        }
    }
}

Run one of these commands in the root directory of your Lean project (where lakefile.toml is located):

# Local-scoped MCP server
claude mcp add lean-lsp uvx lean-lsp-mcp

# OR project-scoped MCP server
# (creates or updates a .mcp.json file in the current directory)
claude mcp add lean-lsp -s project uvx lean-lsp-mcp

You can find more details about MCP server configuration for Claude Code here.

(These instructions cover Mac/Linux.)

1. Edit ~/.vibe/config.toml.

1. Paste the following into the file (e.g. at the end):

[[mcp_servers]]
name = "lean-lsp"
transport = "stdio"
command = "uvx"
args = ["lean-lsp-mcp"]
tool_timeout_sec = 600

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.

Example:

export LEAN_MCP_DISABLED_TOOLS="lean_run_code,lean_build"
export LEAN_MCP_INSTRUCTIONS="Prefer lean_local_search before remote search tools."
export LEAN_MCP_TOOL_DESCRIPTIONS='{"lean_goal":"Primary proof-state inspection tool."}'

MCP Configuration

This MCP server works out-of-the-box without any configuration. However, a few optional settings are available.

Environment Variables

• LEAN_LOG_LEVEL: Log level for the server. Options are "INFO", "WARNING", "ERROR", "NONE". Defaults to "INFO".
• LEAN_LOG_FILE_CONFIG: Config file path for logging, with priority over LEAN_LOG_LEVEL. If not set, logs are printed to stdout.
• LEAN_PROJECT_PATH: Path to your Lean project root. A valid Lean project root must contain lean-toolchain and either lakefile.lean or lakefile.toml. Relative file_path arguments resolve against this root. This variable is required for streamable-http and sse.
• LEAN_MCP_DISABLED_TOOLS: Comma-separated list of tool names to remove from MCP tool listing.
• LEAN_MCP_INSTRUCTIONS: Replacement server instructions string.
• LEAN_MCP_TOOL_DESCRIPTIONS: JSON object mapping tool names to replacement descriptions.
• LEAN_MCP_SCRATCH_SLOTS: Number of parallel scratch documents used for snippet

trials. Defaults to 1; increase it only when parallel attempts are worth the additional Lean process memory.

• LEAN_MCP_MAX_OUTPUT_CHARS: Per-field character budget for goal states and

diagnostic messages. Defaults to 6000; oversized text is elided from the middle so both the local context and the goal target survive. Set to 0 to return everything untruncated.

• LEAN_REPL: Set to true, 1, or yes to enable fast REPL-based lean_run_code and line-based lean_multi_attempt (see REPL Setup).
• LEAN_REPL_PATH: Path to the repl binary. Auto-detected from .lake/packages/repl/ or .lake/packages/REPL/ if not set.
• LEAN_REPL_TIMEOUT: Per-command timeout in seconds (default: 60).
• LEAN_REPL_MEM_MB: Max memory per REPL in MB (default: 16384). Only enforced on Linux/macOS.
• LEAN_LSP_MCP_TOKEN: Secret token for bearer authentication when using streamable-http or sse transport. If set, bearer auth is required for every request.
• LEAN_BUILD_CONCURRENCY: Build concurrency mode for lean_build. Options: allow (default), cancel, share.