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:

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

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

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

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

# 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

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

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.
• LEAN_HAMMER_URL: URL for a self-hosted Lean Hammer Premise Search instance. Rate limits are skipped when set to a custom backend.
• LEAN_LOOGLE_LOCAL: Set to true, 1, or yes to enable local loogle (see Local Loogle section).
• LEAN_LOOGLE_CACHE_DIR: Override the cache directory for local loogle (default: ~/.cache/lean-lsp-mcp/loogle).
• LOOGLE_URL: URL for a self-hosted Loogle instance (default: https://loogle.lean-lang.org). Rate limits are skipped when set to a custom backend.
• LOOGLE_HEADERS: JSON object of extra HTTP headers for Loogle requests (e.g. '{"X-API-Key": "..."}').

You can also often set these environment variables in your MCP client configuration:

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

Transport Methods

The Lean LSP MCP server supports the following transport methods:

• stdio: Standard input/output (default)
• streamable-http: HTTP streaming
• sse: Server-sent events (MCP legacy, use streamable-http if possible)

stdio supports project inference and switching as you move between Lean projects. streamable-http and sse are single-project deployments: they require LEAN_PROJECT_PATH at startup and reject tool-driven project switching.

You can specify the transport method using the --transport argument when running the server. For sse and streamable-http you can also optionally specify the host and port:

uvx lean-lsp-mcp --transport stdio # Default transport
uvx lean-lsp-mcp --transport streamable-http # Available at http://127.0.0.1:8000/mcp
uvx lean-lsp-mcp --transport sse --host localhost --port 12345 # Available at http://localhost:12345/sse
uvx lean-lsp-mcp --version # Print the installed version

OpenAI Secure MCP Tunnel

For ChatGPT, Codex, Responses API, or other OpenAI surfaces, use OpenAI Secure MCP Tunnel instead of exposing lean-lsp-mcp to the public internet. Create a tunnel in Platform tunnel settings, then run tunnel-client on a host that can reach your Lean project:

export CONTROL_PLANE_API_KEY="sk-..."

tunnel-client init \
  --sample sample_mcp_stdio_local \
  --profile lean-lsp-local \
  --tunnel-id tunnel_0123456789abcdef0123456789abcdef \
  --mcp-command "uvx lean-lsp-mcp --transport stdio --lean-project-path /path/to/lean/project"

tunnel-client doctor --profile lean-lsp-local --explain
tunnel-client run --profile lean-lsp-local

Use --lean-project-path so relative file_path arguments resolve inside the intended Lean project. For HTTP, bind lean-lsp-mcp to loopback and use --mcp-server-url http://127.0.0.1:8000/mcp in the tunnel profile:

export LEAN_PROJECT_PATH="/path/to/lean/project"
uvx lean-lsp-mcp --transport streamable-http --host 127.0.0.1 --port 8000

Keep tunnel-client run healthy while testing connector discovery or tool calls. In ChatGPT connector settings, choose Tunnel as the connection type.

Bearer Token Authentication

Transport via streamable-http and sse supports bearer token authentication. For private OpenAI access, prefer OpenAI Secure MCP Tunnel; bearer auth remains available for HTTP/SSE deployments that clients reach directly.

Set the LEAN_LSP_MCP_TOKEN environment variable (or see section 3 for setting env variables in MCP config) to a secret token before starting the server. If this variable is set, requests without a matching Authorization: Bearer ... header are rejected before tool dispatch.

Example Linux/MacOS setup:

export LEAN_LSP_MCP_TOKEN="your_secret_token"
uvx lean-lsp-mcp --transport streamable-http

Clients should then include the token in the Authorization header.

REPL Setup

Enable fast REPL-based lean_run_code and line-based lean_multi_attempt. Uses leanprover-community/repl tactic mode. Exact column-based attempts still use the LSP path.

1. Add REPL to your Lean project's lakefile.toml:

[[require]]
name = "repl"
git = "https://github.com/leanprover-community/repl"
rev = "v4.34.0"  # Use a REPL tag compatible with your Lean toolchain

2. Build it:

lake build repl

3. Enable via CLI or environment variable:

uvx lean-lsp-mcp --repl

# Or via environment variable
export LEAN_REPL=true

The REPL binary is auto-detected from .lake/packages/repl/ or .lake/packages/REPL/. Falls back to LSP if not found.

Path Policy

File-based tools only operate on files inside the active Lean project, resolved .lake/packages/* dependencies, and the Lean stdlib source tree. Returned file paths are sanitized to avoid leaking host absolute paths:

• Project files are returned relative to the project root, for example src/MyFile.lean.
• Dependency files are returned under .lake/packages/<package>/....
• Stdlib files are returned under .lean-stdlib/....

Symlink escapes outside those roots are rejected.

Local Loogle

Run Loogle locally to avoid the remote API's rate limit (3 req/30s). The binary is built once for the project's Lean toolchain. The first Mathlib index takes a few minutes; subsequent starts load it in seconds.

# Enable via CLI
uvx lean-lsp-mcp --loogle-local

# Or via environment variable
export LEAN_LOOGLE_LOCAL=true

Requirements: git, lake (elan), a built Mathlib project, and substantial memory for indexing. In measurements on current Mathlib, the initial index used ~13 GiB peak RSS and a warm load used ~7 GiB.

Note: Local loogle is currently only supported on Unix systems (Linux/macOS). Windows users should use WSL or the remote API.

Mathlib comes from your project: --lean-project-path must point at a built project that depends on Mathlib. The local binary is compiled for that project's Lean toolchain and runs through lake env, so Lake supplies the project's own dependency environment. Loogle's native dependency hash detects changed .olean files and rebuilds a stale index automatically.

Falls back to remote API if local loogle fails.

Notes on MCP Security

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

This MCP server 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.
• Powerful local build and analysis capabilities.
• External network access for remote search tools unless disabled by the operator.

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

Containerized setup (recommended for stricter isolation)

Build image:

docker build -t lean-lsp-mcp:containerized .

Run with a mounted project root (read-only source + writable Lake cache):

docker run --rm -i \
  -v "$PWD":/workspace:ro \
  -v lean-lsp-mcp-lake-cache:/workspace/.lake \
  lean-lsp-mcp:containerized

The included Docker image defaults to:

• LEAN_PROJECT_PATH=/workspace
• LEAN_MCP_DISABLED_TOOLS=lean_run_code

Notes:

• LEAN_MCP_DISABLED_TOOLS is a startup default and can be overridden by docker run -e.
• Using --network none can break tools that require network access (leansearch, loogle, leanfinder, hammer_premise) and dependency downloads.
• The entrypoint exits immediately if LEAN_PROJECT_PATH does not exist.

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

Development

See Adding a new tool for a step-by-step guide to implementing a new MCP tool (return models, helper modules, registration, tests, and docs).

MCP Inspector

npx @modelcontextprotocol/inspector uvx --with-editable path/to/lean-lsp-mcp python -m lean_lsp_mcp.server

Run Tests

uv sync --all-extras
uv run pytest tests

Publications and Formalization Projects using lean-lsp-mcp

• Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physics arxiv
• Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematics arxiv github
• MerLean: An Agentic Framework for Autoformalization in Quantum Computation arxiv
• M2F: Automated Formalization of Mathematical Literature at Scale arxiv
• A Group-Theoretic Approach to Shannon Capacity of Graphs and a Limit Theorem from Lattice Packings github

Talks

lean-lsp-mcp: Tools for agentic interaction with Lean (Lean Together 2026) youtube

Related Projects

• LeanTool
• LeanExplore MCP

License & Citation

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}
}