lean_build
Build the Lean project and restart LSP. Use only if needed (e.g. new imports).
LABSCO SUMMARY
The goal state stops being something a human has to read out of the editor.
Everything a Lean session actually turns on — what the goal is now, what the tactic did to it, whether the name you are about to type exists — is a call rather than a screenshot. Trying several candidate tactics at once and getting each resulting goal state back, with the file untouched either way, is the one that changes the loop most.
What it is
An MCP front end to the Lean language server for a project on disk — it runs lake serve in the project root — plus several external Mathlib search services reached through the same tool set.
What you get
- The proof state where the work is: goals at a position, goals before and after a line when the column is omitted, and the expected type at a point
- Compiler feedback without a rebuild — diagnostics for a file, and code actions that return resolved edits for simp?, exact? and apply? suggestions
- Tactic experiments that leave the file alone: several candidate tactics tried at once with the resulting goal state for each, and a self-contained snippet compiled for its diagnostics
- Four ways to find a lemma when you do not know its name: a local search that confirms a declaration exists, natural language via leansearch.net, type-signature patterns via loogle.lean-lang.org, and goal-directed suggestions from premise-search.com and Lean Finder
- Premise suggestions for automation tactics at a goal position, returned as lemma names to feed to simp only
- Code navigation: a file outline with type signatures, hover types and docs, completions on incomplete code, declaration source with its context, and every reference to a symbol
- Proof hygiene checks: the axioms a theorem depends on, each explicit hypothesis dropped in a scratch copy to show which are load-bearing, and per-line timing from a profiling run
- Panel widgets at a position, and a widget's JavaScript source by hash, for proofs that render their own visualisations
- Tools removed from the listing by name, and their descriptions replaced, through environment variables — for keeping a build or code-execution tool out of an agent's reach
Requirements
uv, and a Lean project root containing lean-toolchain and a lakefile — run lake build in it by hand first, because the server starts the language server on connect and a cold build times some clients out. LEAN_PROJECT_PATH names that root, and is required outright when the server runs over HTTP or SSE. Install ripgrep for the local search and the source scanning behind the axiom check. The Mathlib search tools call external services, each under its own published rate limit, so heavy lemma hunting is what will pace a long session. MIT licensed.
Setup effort
One command — uvx lean-lsp-mcp
USE CASES
01
Knowing where the proof actually stands
Read the goals at the position, and the expected type where a term is missing, instead of inferring it from the error.
02
Trying tactics without wrecking the file
Send several candidates at once and compare the goal states that come back; nothing is written either way.
03
Finding the lemma you are sure exists
Confirm the name locally first, then reach for natural-language, type-signature or goal-directed search when it does not.
04
Understanding an API you have not used
Hover for the type and docs, read the declaration's source with its context, and see where else it is used.
05
Checking a finished proof is honest
Read the axioms it depends on, and find out which hypotheses it actually needs by dropping them one at a time.
06
Chasing down a proof that takes forever
Profile it for per-line timing, then look at the outline to see what is being elaborated around it.
23 tools
Counted once with only startup setup. Other versions, modes or optional credentials may expose a different list.
lean_code_actions
Get LSP code actions for a line. Returns resolved edits for TryThis suggestions (simp?, exact?, apply?) and other quick fixes.
lean_completions
Get IDE autocompletions. Use on INCOMPLETE code (after . or partial name).
lean_declaration_file
Get the source of a symbol's declaration (declaration slice + context).
Set full_file=True for the whole file (can be very large).
lean_diagnostic_messages
Get compiler diagnostics (errors, warnings, infos) for a Lean file.
lean_file_outline
Get imports and declarations with type signatures. Token-efficient.
lean_get_widget_source
Get JavaScript source of a widget by hash. Useful for understanding custom widget rendering logic. Returns full JS module - may be large.
lean_get_widgets
Get panel widgets at a position (proof visualizations, #html, custom widgets). Returns raw widget data - may be large.
lean_goal
Get proof goals at a position. MOST IMPORTANT tool - use often!
Omit column to see goals_before (line start) and goals_after (line end), showing how the tactic transforms the state. status='complete' means the proof is finished at this point; status='no_goal_at_position' means the position carries no proof state (e.g. outside a proof).
lean_hammer_premise
Limit: 6req/30s. Get premise suggestions for automation tactics at a goal position.
Returns lemma names to try with simp only [...], aesop, or as hints.
lean_hover_info
Get type signature and docs for a symbol. Essential for understanding APIs.
lean_leanfinder
Limit: 10req/30s. Semantic search by mathematical meaning via Lean Finder.
Examples: "commutativity of addition on natural numbers", "I have h : n < m and need n + 1 < m + 1", proof state text.
The version argument selects which mathlib snapshot to query (v4.19.0, v4.24.0, or v4.28.0). Default: v4.28.0.
lean_leansearch
Limit: 90req/30s. Search Mathlib via leansearch.net using natural language.
Examples: "sum of two even numbers is even", "Cauchy-Schwarz inequality", "{f : A → B} (hf : Injective f) : ∃ g, LeftInverse g f"
lean_local_search
Fast local search to verify declarations exist. Use BEFORE trying a lemma name.
lean_loogle
Search Mathlib by type signature via loogle.lean-lang.org.
Examples: Real.sin, "comm", (?a → ?b) → List ?a → List ?b, _ * (_ ^ _), |- _ < _ → _ + 1 < _ + 1
lean_minimal_hypotheses
For each explicit (h : T) hypothesis of a theorem, drop it and re-elaborate a scratch copy of the file. Reports which hypotheses are load-bearing and which are actually unused. Skips implicit {x : α} and instance [inst : C] binders (those are usually inferable / always load-bearing). Does not rewrite the proof body — a body that names h will fail to elaborate without the binder, which is the truthful answer (load-bearing).
Variants are checked in parallel on scratch documents; the file is never edited.
lean_multi_attempt
Try multiple tactics without modifying file. Returns goal state for each.
lean_profile_proof
Run lean --profile on a theorem. Returns per-line timing and categories. SLOW - avoid on theorems that already hit heartbeat limits.
lean_references
Find all references to a symbol (including the declaration). Position cursor at the symbol.
lean_run_code
Run a code snippet and return diagnostics. Must include all imports.
lean_state_search
Limit: 6req/30s. Find lemmas to close the goal at a position. Searches premise-search.com.
lean_term_goal
Get the expected type at a position.
lean_verify
Check theorem axioms + optional source scan. Only scans the given file, not imports.
BEFORE YOU INSTALL
What to know first
Tools you get
23 tools when we connected. The project's Docker image disables lean_run_code via LEAN_MCP_DISABLED_TOOLS, leaving 22. lean_local_search needs ripgrep, and lean_leansearch, lean_loogle, lean_leanfinder, lean_state_search and lean_hammer_premise need network access.
Requires
uvx on PATH
CONTEXT COST
Moderate Standing cost
Rated by the size of the 23 tool definitions that ride along on every turn, not by how many there are
INSTALLATION
Connect your client
Server setup
TERMINAL
uvx lean-lsp-mcpMCP Clients
VS Code
VS CODE · JSON
{
"servers": {
"lean-lsp": {
"type": "stdio",
"command": "uvx",
"args": [
"lean-lsp-mcp"
]
}
}
}VS Code — WSL
VS CODE — WSL · JSON
{
"servers": {
"lean-lsp": {
"type": "stdio",
"command": "wsl.exe",
"args": [
"uvx",
"lean-lsp-mcp"
]
}
}
}Cursor
CURSOR · JSON
{
"mcpServers": {
"lean-lsp": {
"command": "uvx",
"args": [
"lean-lsp-mcp"
]
}
}
}Claude Code
CLAUDE CODE · TERMINAL
claude mcp add lean-lsp uvx lean-lsp-mcpMistral Vibe
MISTRAL VIBE · JSON
{
"mcp_servers": [
{
"name": "lean-lsp",
"transport": "stdio",
"command": "uvx",
"args": [
"lean-lsp-mcp"
],
"tool_timeout_sec": 600
}
]
}
