servers / lean-lsp-mcp
lean-lsp-mcp
communitystdiolocalwrite capablehealthy
Lean Theorem Prover MCP
01Tools · 23
How to read this: tool names here are observed from a live tools/list handshake. The Risk label is a heuristic inferred from the tool name (write/destructive verbs), not from executing the tool — a conservative guess, not a verified capability. We never escalate risk from a description. Found one that's wrong? Tell us — we fix on report.
| Tool | Risk | Side effects | Approval |
|---|---|---|---|
| lean_file_outline Get imports and declarations with type signatures. Token-efficient. | read | false | unknown |
| lean_term_goal Get the expected type at a position. | read | false | unknown |
| lean_references Find all references to a symbol (including the declaration). Position cursor at the symbol. | read | false | unknown |
| lean_build Build the Lean project and restart LSP. Use only if needed (e.g. new imports). | unknown | unknown | unknown |
| lean_code_actions Get LSP code actions for a line. Returns resolved edits for TryThis suggestions (simp?, exact?, apply?) and other quick fixes. | read | false | unknown |
| 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). | read | false | unknown |
| lean_hover_info Get type signature and docs for a symbol. Essential for understanding APIs. | read | false | unknown |
| lean_local_search Fast local search to verify declarations exist. Use BEFORE trying a lemma name. | read | false | unknown |
| 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"
| read | false | unknown |
| lean_loogle Search Mathlib by type signature via loogle.lean-lang.org.
Examples: `Real.sin`, `"comm"`, `(?a → ?b) → List ?a → List ?b`,
`_ * (_ ^ _)`, `|- _ < _ → _ + 1 < _ + 1`
| read | false | unknown |
| lean_multi_attempt Try multiple tactics without modifying file. Returns goal state for each. | read | false | unknown |
| lean_profile_proof Run `lean --profile` on a theorem. Returns per-line timing and categories. SLOW - avoid on theorems that already hit heartbeat limits. | read | false | unknown |
| 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.
| read | false | unknown |
| lean_run_code Run a code snippet and return diagnostics. Must include all imports. | write | true | unknown |
| lean_state_search Limit: 6req/30s. Find lemmas to close the goal at a position. Searches premise-search.com. | read | false | unknown |
| lean_verify Check theorem axioms + optional source scan. Only scans the given file, not imports. | unknown | unknown | unknown |
| 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. | read | false | unknown |
| lean_get_widgets Get panel widgets at a position (proof visualizations, #html, custom widgets). Returns raw widget data - may be large. | read | false | unknown |
| 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).
| read | false | unknown |
| lean_diagnostic_messages Get compiler diagnostics (errors, warnings, infos) for a Lean file. | read | false | unknown |
| lean_completions Get IDE autocompletions. Use on INCOMPLETE code (after `.` or partial name). | read | false | unknown |
| 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.
| read | false | unknown |
| 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. | unknown | unknown | unknown |
02Install & source
uvx lean-lsp-mcp
uvx- repohttps://github.com/oOo0oOo/lean-lsp-mcp
- licenseMIT
- adoption477 stars · 76 forks
03Access granted
Execute code · write
The access this server can exercise, inferred from its verified tools — not a declared OAuth scope.
05Provenance & freshness
sourcesGitHub repo search [p4]
last_checked2026-08-16 14:22Z
next_check2026-08-17 07:37Z
cadenceevery 17h
verifiedtools_list:passed handshake:passed metadata:passed tools_list:passed handshake:passed metadata:passed
index_statusindex — 9 unique facts >= 5
06Badge
Add the “as seen on MCPExplorer” badge to your README. 
[](https://mcpexplorer.com/servers/lean-lsp-mcp)
Next step
This is one server. A loadout combines the right servers, governance, and proven plays for a whole job — assembled deliberately, not tool-dumped.
Explore loadouts →