Lean LSP

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 theuvsetup below.

lean-lsp-mcpwill runlake servein 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 runlake buildmanually before starting the MCP. This ensures a faster build time and avoids timeouts.

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 openingmcp.jsonwith:

Ctrl+Shift+P > "MCP: Open User Configuration"

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

5. Install the Lean 4 skill (optional but recommended)

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 examplelean_run_code,lean_build).
- LEAN_MCP_INSTRUCTIONS: Replacement server instructions string.
- LEAN_MCP_TOOL_DESCRIPTIONS: JSON object to override tool descriptions.

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."}'

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

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

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-pathso relativefile_patharguments resolve inside the intended Lean project. For HTTP, bindlean-lsp-mcpto loopback and use--mcp-server-url http://127.0.0.1:8000/mcpin 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

Keeptunnel-client runhealthy while testing connector discovery or tool calls. In ChatGPT connector settings, chooseTunnelas the connection type.

Transport viastreamable-httpandssesupports 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 theLEAN_LSP_MCP_TOKENenvironment 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 matchingAuthorization: Bearer ...header are rejected before tool dispatch.

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

Clients should then include the token in theAuthorizationheader.

1. Add REPL to your Lean project'slakefile.toml:

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-pathmust point at a built project that depends on Mathlib. The local binary is compiled for that project's Lean toolchain and runs throughlake env, so Lake supplies the project's own dependency environment. Loogle's native dependency hash detects changed.oleanfiles and rebuilds a stale index automatically.

Falls back to remote API if local loogle fails.

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)

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

- LEAN_PROJECT_PATH=/workspace
- LEAN_MCP_DISABLED_TOOLS=lean_run_code

- LEAN_MCP_DISABLED_TOOLSis a startup default and can be overridden bydocker run -e.
- Using--network nonecan break tools that require network access (leansearch,loogle,leanfinder,state_search,hammer_premise) and dependency downloads.
- The entrypoint exits immediately ifLEAN_PROJECT_PATHdoes not exist.