What is Lean LSP MCP?
Lean LSP MCP, by Oliver Dressler, connects an MCP client to the Lean theorem prover through Lean's language server. The agent reads diagnostics and goal states, hovers for types, tries several tactics at once, checks which axioms a finished proof relies on, and searches Mathlib locally or through LeanSearch, Loogle, Lean Finder and Lean Hammer.
It is MIT-licensed, written in Python, has about 548 GitHub stars and 28 contributors, and released v0.33.0 on 3 November 2026. Several research systems for automated formal mathematics, including Numina-Lean-Agent and Ax-Prover, list it as their Lean interface.
How to install Lean LSP MCP
uvx lean-lsp-mcpIs Lean LSP MCP worth it?
Lean LSP MCP is the standard way to put an agent in front of Lean 4. A language model guessing at proofs from memory produces text that looks right and fails to compile; this server lets it read the live goal state after each tactic, see the exact error, and try again. Its 22 tools cover the loop a mathematician runs in the editor: lean_goal and lean_diagnostic_messages to see where a proof stands, lean_multi_attempt to test several tactics at one position, lean_verify to list the axioms a theorem depends on (anything beyond the standard three, such as sorryAx, means the proof is unsound), and lean_build for the whole project.
The search tools are where agents save the most time, since finding the right Mathlib lemma is half of formal proof. Most of the remote services, LeanSearch, Loogle, Lean Finder and Lean Hammer premise search, are rate limited to 3 requests per 30 seconds each, and the docs ask users not to overload these free services. Local Loogle removes the limit at a cost: the first Mathlib index peaked at about 13 GiB of memory in the developer's measurements, and a warm load uses about 7 GiB.
The catch: this is a research tool in beta, and the README is direct about the risks. Build and run tools execute Lean code, which can read and write files, and the remote search tools send your queries to third-party services. File tools are fenced to the project, its dependencies and the Lean standard library, and the bundled Docker image disables lean_run_code by default. The HTTP transport defaults to 127.0.0.1, and HTTP and SSE accept a bearer token through LEAN_LSP_MCP_TOKEN, but that is a single shared secret, not per-user access control.
Our take: for anyone doing formal proofs with an agent, this is plumbing rather than a choice, with about 14,700 PyPI downloads in a week and published research built on it. The real work is on your side: run lake build first so the client does not time out, add the REPL for speed, and budget memory if you go local with Loogle.
Where it earns its place
A PhD student formalising a combinatorics paper in Mathlib
Close routine lemmas without hunting for every Mathlib name
The agent reads the goal, searches Loogle and LeanSearch for matching lemmas, tries several tactics with lean_multi_attempt, and runs lean_verify on the result. Free; the remote search limit of 3 requests per 30 seconds sets the pace.
A verification engineer at a fintech start-up
Keep machine-checked proofs of core invariants up to date as code changes
After each change, the agent rebuilds the Lean project, reads the diagnostics, repairs broken proofs, and confirms with lean_verify that no sorry crept in. Run it in the bundled Docker image with the source mounted read-only.
An AI lab building a theorem-proving agent
Give the agent a reliable Lean interface without writing one
Serve it over streamable HTTP on 127.0.0.1 with a bearer token, enable the REPL for fast snippet runs, and self-host Loogle or Lean Hammer to escape the public rate limits. Numina-Lean-Agent and Ax-Prover both list it as their Lean interface.
Before you commit
- Setup
- Install uv, run lake build in your Lean project, then add uvx lean-lsp-mcp to your client (one-click buttons for VS Code; claude mcp add lean-lsp uvx lean-lsp-mcp for Claude Code). Optional ripgrep for local search and the REPL for faster runs. Nix is also supported.
- Integrations
- 22 tools over the Lean language server via leanclient; LeanSearch, Loogle, Lean Finder and Lean Hammer premise search; optional leanprover-community REPL and local Loogle. Works with VS Code, Cursor, Claude Code and Mistral Vibe; OpenAI Secure MCP Tunnel for ChatGPT and Codex.
- Data and privacy
- Runs locally. Proof code and goals go to your model provider; search queries go to the remote search services unless you self-host them or disable those tools. Returned paths are made relative to hide host directories.
- Cost at scale
- Free under MIT. Heavy use means self-hosting Loogle or Lean Hammer to avoid rate limits, and enough memory for local Loogle (about 7 GiB warm) and each REPL (16384 MiB budget by default).
- Limits
- Most remote search tools are limited to 3 requests per 30 seconds. HTTP and SSE serve one project only. The REPL memory cap is not enforced on Windows, and local Loogle runs only on Linux and macOS.
What’s good
- Live goal states and diagnostics after every tactic
- lean_verify flags proofs that rely on sorry or extra axioms
- Four Mathlib search services plus local search
- Runs on stdio, HTTP or SSE; Docker image included
What’s not
- Remote search capped at 3 requests per 30 seconds
- Local Loogle needs about 13 GiB to build its index
- Executes project Lean code; beta by its own description
- Clients can time out unless lake build runs first
Best for
Mathematicians, formal-methods engineers and researchers who want Claude Code, Cursor or VS Code agents to write and check Lean 4 proofs.
Lean LSP MCP alternatives
Lean LSP MCP: common questions
- Is Lean LSP MCP worth it?
- If an agent is going to write Lean proofs, this is the server it should be looking through, because it shows the model exactly what the proof checker sees. We rate it 4.5 out of 5.
- How much does Lean LSP MCP cost?
- Free and open source (MIT). The remote search services it calls are free community services.
- What are the downsides of Lean LSP MCP?
- Remote search capped at 3 requests per 30 seconds; local Loogle needs about 13 GiB to build its index; executes project Lean code; beta by its own description; clients can time out unless lake build runs first.
- Who is Lean LSP MCP best for?
- Mathematicians, formal-methods engineers and researchers who want Claude Code, Cursor or VS Code agents to write and check Lean 4 proofs.
- How much does Lean LSP MCP cost for a team or in production?
- Free under MIT. Heavy use means self-hosting Loogle or Lean Hammer to avoid rate limits, and enough memory for local Loogle (about 7 GiB warm) and each REPL (16384 MiB budget by default).
- Is Lean LSP MCP safe for company data?
- Runs locally. Proof code and goals go to your model provider; search queries go to the remote search services unless you self-host them or disable those tools. Returned paths are made relative to hide host directories.
- What are the best Lean LSP MCP alternatives?
- The closest alternatives we have reviewed are MCP Solver and Serena.
Answers checked Nov 7, 2026.
Make Lean LSP MCP? Show this rating on your site
