Lean LSP

Lean LSP MCP enables agentive interaction with the Lean theorem prover through the Language Server Protocol. It exposes rich Lean tooling to your editors and AI assistants, helping you diagnose issues, inspect goals and terms, navigate definitions, and perform targeted searches across Lean projects.

How to use

You connect through an MCP client that supports standard MCP servers. The server runs locally and communicates using a standard stdio interface. Start the MCP server with the runtime command and then point your editor to the server. You can also use local search and external tools to augment your experience, including diagnostics, goals, hover information, and term lookups.

How to install

Prerequisites include a Python package manager and a Lean project that builds quickly. Follow these steps to set up the Lean LSP MCP server locally.

1. Install uv on your system. On Linux or macOS, run the following command in a terminal:

curl -LsSf https://astral.sh/uv/install.sh | sh

2. Ensure your Lean project builds quickly. In the project root, run lake build to prepare the project for the language server.

3. Configure your IDE or editor to connect to the MCP server. The following configuration examples show a standard stdio setup compatible with popular editors.

4. (Optional but recommended) Install ripgrep to improve local search results. Make sure rg is available in your PATH.

5. Start the MCP server with the standard stdio command and connect your editor to it using the provided configurations.

Configuration

VSCode setup as a ready-to-use configuration (stdio) is shown here. Copy this into your VSCode user or workspace settings.

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

Windows with WSL2 setup

If you are on Windows using WSL2, use this configuration to run the MCP server through the Windows launcher.

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

Alternate local run hints

If you cannot use the standard path, you can replace the command with a direct path to the MCP server binary or script in your environment. Ensure the final start command remains compatible with your editor’s MCP integration.

Available tools

lean_file_outline

Get a concise outline of a Lean file showing imports and declarations with type signatures (theorems, definitions, classes, structures).

lean_diagnostic_messages

Obtain all diagnostic messages for a Lean file, including infos, warnings and errors.

lean_goal

Retrieve the current proof goal at a specified location (line or line+column) in a Lean file.

lean_term_goal

Get the term goal at a specific position in a Lean file.

lean_hover_info

Fetch hover documentation for symbols, terms, and expressions at a location.

lean_declaration_file

Get the file contents where a symbol or term is declared.

lean_completions

Code auto-completion for available identifiers and import suggestions at a position.

lean_run_code

Run or compile an independent Lean code snippet and return the result.

lean_multi_attempt

Try multiple Lean code snippets on a line and compare the resulting goals and diagnostics.

lean_local_search

Search Lean definitions and theorems in the local project and stdlib using ripgrep.

lean_leansearch

Natural language search for Mathlib theorems via leansearch.net.

lean_loogle

Search Lean definitions/theorems using loogle with optional local mode.

lean_leanfinder

Semantic search for Mathlib theorems with Lean Finder.

lean_state_search

Premise-based search for applicable theorems to current goals.

lean_hammer_premise

Premise search using Lean Hammer to find relevant premises for the current goal.

lean_build

Rebuild the Lean project and restart the Lean LSP server.

mcp_inspector

Inspect MCP state and interactions during development.