MCP that allows agentic interaction with the Lean theorem prover via the Language Server Protocol using leanclient. This server provides a range of tools for AI models to understand, analyze and interact with Lean projects.

Currently beta testing: Please help us by submitting bug reports, feedback and feature requests.

• Rich Lean Interaction: Access diagnostics, goal states, term information, and hover documentation.
• Agent-Focused Toolset: Includes tools for theorem search (leansearch.net), code completion, and project builds.
• Easy Setup: Simple configuration for various IDEs, including VSCode and Cursor.

1. Install uv, a Python package manager.
2. Make sure your Lean project builds quickly by running lake build manually.
3. Add JSON configuration to your IDE/Setup and configure LEAN_PROJECT_PATH.

Install uv for your system.

E.g. on Linux/MacOS:

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

lean-lsp-mcp will run lake build in the project root upon startup. Some IDEs (like Cursor) might timeout during this process. Therefore, it is recommended to run lake build manually before starting the MCP. This ensures a faster startup time and avoids timeouts.

E.g. on Linux/MacOS:

cd /path/to/lean/project
lake build

Note: Your build does not necessarily need to be successful, some errors or warnings (e.g. declaration uses 'sorry') are OK.

VSCode and VSCode Insiders are supporting MCPs in agent mode. For VSCode you might have to enable Chat > Agent: Enable in the settings.

1. One-click config setup:

OR manually add config to settings.json (global):

{
    "mcp": {
        "servers": {
            "lean-lsp": {
                "command": "uvx",
                "args": ["lean-lsp-mcp"],
                "env": {
                    "LEAN_PROJECT_PATH": "/path/to/lean/project"
                }
            }
        }
    }
}

2. Next change the env variable LEAN_PROJECT_PATH to point to the root of your Lean project. This is required for the MCP to work. You can also remove this from the config and set this env variable differently.

3. Click "Start" above server config, open a Lean file, change to agent mode in the chat and run e.g. "auto proof" to get started:

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 and adjust the LEAN_PROJECT_PATH to point to the root of your Lean project:

{
    "mcpServers": {
        "lean-lsp": {
            "command": "uvx",
            "args": ["lean-lsp-mcp"],
            "env": {
                "LEAN_PROJECT_PATH": "/path/to/lean/project"
            }
        }
    }
}

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 -e LEAN_PROJECT_PATH=$PWD

# 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 -e LEAN_PROJECT_PATH=$PWD

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

Other setups, such as Claude Desktop or OpenAI Agent SDK should work with similar configs.

Lean LSP MCP currently provides various tools to interact with the Lean theorem prover:

Get detailed instructions on how to use the Lean LSP MCP to automatically prove theorems. This is a tool call because many clients do not support prompts yet, it is also available as a prompt. You can check out the current instruction prompt in prompts.py.

Get all diagnostic messages for a Lean file. This includes infos, warnings and errors.

Get the proof goal at a specific location (line or line & column) in a Lean file.

Get the term goal at a specific position (line & column) in a Lean file.

Retrieve hover information (documentation) for symbols, terms, and expressions in a Lean file (at a specific line & column).

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

Code auto-completion: Find available identifiers or import suggestions at a specific position (line & column) in a Lean file.

Attempt multiple lean code snippets on a line and return goal state and diagnostics for each snippet. This tool is useful to screen different proof attempts before using the most promising one.

Search for theorems in Mathlib using leansearch.net (natural language search).

Check if all proofs in a file are complete. This is currently very simple and will be improved in the future.

Get the contents of a Lean file, optionally with line number annotations.

Rebuild the Lean project and restart the Lean LSP server.

Get detailed instructions on how to use the Lean LSP MCP to automatically prove theorems. See above (Meta tools).

Here are a few example prompts and interactions to try. All examples use VSCode (Agent Mode) and Gemini 2.5 Pro (Preview).

Open unfinished proof. Run prompt "auto proof" in VSCode (Agent Mode) or Cursor will use the lean_auto_proof_instructions tool to get detailed instructions on how to use the Lean LSP MCP to automatically prove theorems.

Open Algebra/Lie/Abelian.lean. Example prompt:

"Analyze commutative_ring_iff_abelian_lie_ring thoroughly using various tools such as goal, term goal, hover info. Explain the key proof steps in english.".

Open an incomplete proof such as putnam 1964 b2. Example prompt:

"First analyze the problem statement by checking the goal, hover info and looking up key declarations. Next use up to three queries to leansearch to design three different approaches to solve this problem. Very concisely present each approach and its key challenge."

Many IDEs allow 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).

There are many valid security concerns with the Model Context Protocol (MCP) in general!

This MCP is meant as a research tool and is currently in beta. While it does not handle any sensitive data such as passwords or API keys, it still includes various security risks:

• Access to your local file system.
• No rate limiting on tool calls.
• No input or output validation.

Please be aware of these risks. Feel free to audit the code and report security issues!

For more information, you can use Awesome MCP Security as a starting point.

• LeanTool
• LeanExplore MCP

MIT licensed. See LICENSE for more information.

Citing this repository is highly appreciated but not required by the license.

@software{lean-lsp-mcp,
  author = {Oliver Dressler},
  title = {{Lean LSP MCP: Tools for agentic interaction with the Lean theorem prover}},
  url = {https://github.com/oOo0oOo/lean-lsp-mcp},
  month = {3},
  year = {2025}
}