lean-lsp-mcp
MCP server for the Lean 4 language server: an agent reads proof goals and errors and searches for theorems inside your project
- 550 ★ on the repository
- Last commit
- MIT
Extended access
Why this level
- The server runs `lake serve` and compiles project code on your machine.
- Theorem search queries go to the external LeanSearch, Loogle and Lean Finder services.
Install
- Works in
In your terminal, with SkillFoxx CLI
npx skillfoxx add mcp/lean-lsp-mcpDetects the agents on your machine, shows the access level and pins the version.
Other ways to install
Access and checks
How we reviewExtended accessThe tool runs code or makes network calls and only reads external data.
- The server runs `lake serve` and compiles project code on your machine.
- Theorem search queries go to the external LeanSearch, Loogle and Lean Finder services.
This is third-party code. Review the repository files before installing.
What it does
lean-lsp-mcp connects an agent to a Lean 4 project through the `lake serve` language server. The agent asks for the proof goal on a given line, file diagnostics, hover documentation, declarations and references of a symbol, completions and a file outline with signatures. Separate tools try code: `lean_run_code` compiles a snippet, and `lean_multi_attempt` checks several tactics at one position and returns the goal and errors for each. For theorem search the server calls LeanSearch, Loogle, Lean Finder and Lean Hammer, and a local search through `ripgrep` is available too. The server runs over `stdio` and needs no configuration. The REPL mode, switched on with `LEAN_REPL=true`, speeds up code runs and tactic trials. `LEAN_MCP_DISABLED_TOOLS` removes tools you do not want.
Who it is for. Mathematicians and developers who prove theorems in Lean 4 with Claude Code, Cursor or Codex and want the agent to see the state of the proof.
Good fit when
- A proof is stuck on one line and the agent needs the goal with hypotheses at that point
- A file does not build and you want every error and warning with positions at once
- Several tactic variants should be checked together instead of editing the file one by one
- You need a Mathlib lemma whose name you do not know: search by meaning through LeanSearch or Loogle
- The module is large and you want an outline of a file's declarations with types before editing
Not a fit when
- The code is written in another language: the server works with Lean only
- The machine has no `lake` and no Lean toolchain, and you cannot install them
- The build is slow and the client drops long runs: run `lake build` by hand first
- Network requests to external theorem search services are not acceptable: you can switch them off, but only local search remains
Example request
The proof of the theorem in Basic.lean is stuck on line 42. Show the goal at that point and try `simp`, `omega` and `linarith`.MCP
- Transport
- stdio, http, sse
- Authentication
- not required
Environment variables
`LEAN_PROJECT_PATH`- Path to the Lean project root. Required for the `streamable-http` and `sse` modes.
`LEAN_REPL`- The value `true` enables fast code runs and tactic trials through the REPL.
Limitations
- You need `uv` and a project that builds with `lake build`. Some clients, Cursor for one, time out on startup, so build the project beforehand.
- Search through LeanSearch, Loogle and Lean Finder goes to external services, not to your machine.
- `ripgrep` is optional, but without it `lean_local_search` and the `lean_verify` warnings do not work.
- The `streamable-http` and `sse` modes require the `LEAN_PROJECT_PATH` variable with the project root.
How to disable. Run `claude mcp remove lean-lsp` or delete the `lean-lsp` entry from the client's `mcp.json`. The `LEAN_MCP_DISABLED_TOOLS` variable switches off individual tools.
FAQ
How do I connect lean-lsp-mcp to Claude Code?
Run `claude mcp add lean-lsp uvx lean-lsp-mcp` in the project root where `lakefile.toml` lives. Add `-s project` to share the setup: the entry lands in `.mcp.json`.
Why build the project before starting the server?
The server runs `lake serve`, and a first build takes a long time. A client can time out on startup, so build ahead with `lake build`.
What does the REPL mode change?
With `LEAN_REPL=true`, `lean_run_code` reuses the import cache and `lean_multi_attempt` tries tactics per line up to five times faster. `LEAN_REPL_PATH` sets the binary, otherwise the server looks in `.lake/packages/`.
Is `ripgrep` required?
No, the server starts without it. But `lean_local_search` and the `lean_verify` warnings work only with `rg` on PATH.
How do I remove tools I do not need?
List them in `LEAN_MCP_DISABLED_TOOLS` separated by commas, for example `lean_run_code,lean_build`. In VS Code and Cursor you can also switch a tool off in the client settings.
Discussion
No questions or reviews yet.
Related
MCP serversA bridge from an LSP language server to the agent: definitions, references, diagnostics, hover and symbol rename
An MCP to LSP bridge: the agent gets types, references, diagnostics and refactoring from rust-analyzer, pyright and gopls.
A plugin for proving theorems in Lean 4: mathlib search, sorry-filling cycles, axiom checks and safety hooks
The agent-lsp MCP server orchestrates language servers into agent workflows: callers, safe edits, renames and diagnostics.
A code knowledge graph for your agent: callers, dependents and blast radius over MCP instead of reading files
cclsp connects LSP language servers to Claude Code over MCP: go to definition, find references, rename symbols and diagnostics with no editor needed
README in short
Installation goes through `uv` and `uvx`, with configs for VS Code, Cursor, Claude Code, Mistral Vibe and Codex. Environment variables, the REPL mode and a link to a separate tools reference follow.