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.
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.
- 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
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.
One command — uvx lean-lsp-mcp