ooo0ooo/lean-lsp-mcp

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

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: Memory budget per REPL in MiB (default: 16384). Linux uses a kernel address-space limit (respecting any lower inherited hard limit). macOS samples resident memory of the REPL process tree every 100 ms and kills the group on excess; brief overshoot between samples is possible. Windows does not enforce this budget.
• 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_MODULE: Root module for local Loogle (default: Mathlib). Use a built module such as Init or Mathlib.Data.Nat.Basic to search it and its imports with a smaller index. Indices are separated by project and module.
• LEAN_LOOGLE_LOCAL_ONLY: Set to true, 1, or yes to refuse remote Loogle fallback when local search is unavailable. Defaults to false; this does not disable other remote search tools.
• 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:

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

Protocol compatibility and runtime

This release uses the official Python MCP SDK 2.2.0. The same server supports 2026-07-28 discovery and request metadata as well as legacy initialization; clients do not need a separate endpoint. Tool names, arguments, structured results, and text fallbacks are unchanged. Expected tool errors retain actionable messages; unexpected crash details stay in server logs. Tool configuration is read at startup (CLI options override environment variables); restart to change it. The tool catalog is sorted by name and carries a private 60-second cache hint for modern clients.

Streamable HTTP uses the SDK’s bounded request-body and legacy-session defaults. Expired sessions must reconnect; modern requests do not need session IDs. Keep streaming responses enabled for long-running build progress. A modern request must opt in before receiving MCP log notifications; stderr/file logging remains controlled by LEAN_LOG_LEVEL and the logging configuration.

Build and analysis tools execute project or supplied Lean code, which can have I/O effects even when scratch documents leave source files unchanged. Their MCP annotations therefore make no read-only or idempotence promise. Use trusted projects and code.

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. This is an opaque secret checked by this server, not an OAuth access token. The compatibility mode explicitly disables SDK OAuth resource/audience validation; it does not provide an OAuth authorization server or per-user permissions.

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.35.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//....
• 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}
}