Schema | Lean LSP MCP

Lean LSP MCP

Overview Schema Source Related Servers Discussions Admin

Server Configuration

Describes the environment variables required to run the server.

Name	Required	Description	Default
`LEAN_LOG_LEVEL`	No	Log level for the server. Options are "INFO", "WARNING", "ERROR", "NONE".	INFO
`LEAN_HAMMER_URL`	No	URL for a self-hosted Lean Hammer Premise Search instance.	http://leanpremise.net
`LEAN_LOOGLE_LOCAL`	No	Set to true, 1, or yes to enable local loogle.
`LEAN_PROJECT_PATH`	No	Path to your Lean project root. Set this if the server cannot automatically detect your project.
`LEAN_LSP_MCP_TOKEN`	No	Secret token for bearer authentication when using streamable-http or sse transport.
`LEAN_LOOGLE_CACHE_DIR`	No	Override the cache directory for local loogle.	~/.cache/lean-lsp-mcp/loogle
`LEAN_STATE_SEARCH_URL`	No	URL for a self-hosted premise-search.com instance.	https://premise-search.com

Instructions

Guidance the server publishes about itself, which clients place ahead of the tool catalog so the model reads it before choosing anything.

General Rules

All line and column numbers are 1-indexed. Columns count characters (codepoints).
This MCP does NOT edit files. Use other tools for editing.

Key Tools

lean_goal: Proof state at position. Omit column for before/after. status field: 'goals', 'complete' (proof done here), or 'no_goal_at_position' (not inside a proof).
lean_diagnostic_messages: Compiler errors/warnings. "no goals to be solved" = remove tactics. Each item carries category: 'linter' is style noise (unused variables and the like) that does not block compilation, 'sorry' marks an unproved declaration (not noise), 'suggestion' holds a Try this: replacement. A hint field appears on recognised failure modes.
lean_term_goal: Expected type at a position.
lean_hover_info: Type signature + docs. Column at START of identifier.
lean_completions: IDE autocomplete on incomplete code.
lean_local_search: Fast local declaration search. Use BEFORE trying a lemma name. sources_searched says whether source text and the symbol index were searched. Only index: consulted makes an empty result proof of absence; warming means the symbol index is still loading, unavailable means no language server is running, error means the lookup failed.
lean_file_outline: Fast token-efficient file skeleton with available type signatures.
lean_multi_attempt: Test tactics without editing at a proof position. Use column for an exact source position; omit it for fast line-based attempts: ["simp", "ring", "omega"]
lean_code_actions: Quick fixes and TryThis suggestions (simp?, exact?) with resolved edits.
lean_declaration_file: Declaration source slice with context and declaration line numbers; generated declarations include their source name when it can be determined. full_file=true returns the whole file (large).
lean_references: All usages of a symbol (capped by max_results, total reports the full count).
lean_run_code: Run standalone snippet. Must include imports.
lean_verify: Axiom check + source scan. Use fully qualified name (e.g. Ns.thm).
lean_minimal_hypotheses: Which explicit hypotheses of a theorem are actually needed.
lean_build: Run lake build + restart LSP. Only if needed (new imports). Use fetch_cache=true only for missing dependency caches. SLOW!
lean_profile_proof: Profile a theorem for performance. Shows tactic hotspots. SLOW!

Search Tools (rate limited)

lean_leansearch (90/30s): Natural language -> mathlib
lean_loogle (3/30s): Type pattern -> mathlib
lean_leanfinder (10/30s): Semantic/conceptual search
lean_hammer_premise (6/30s): Goal -> premises for simp/aesop

Search Decision Tree

"Does X exist locally?" -> lean_local_search
"I need a lemma that says X" -> lean_leansearch
"Find lemma with type pattern" -> lean_loogle
"What's the Lean name for concept X?" -> lean_leanfinder
"What closes this goal?" / "What to feed simp?" -> lean_hammer_premise

After finding a name: lean_local_search to verify, lean_hover_info for signature.

Return Formats

List-returning tools return an object with an items array. Empty = {"items": []}.

Slow Files

On large files, pass timeout_s to lean_diagnostic_messages / lean_goal. A response with partial: true + still_elaborating_lines (or goal status: 'still_elaborating') means Lean is still working - poll again; it is NOT an error or a dead server.

Error Handling

Check isError in responses: true means failure (timeout/LSP error/rate limit), while an empty items with isError: false means no results found -- except lean_local_search, where that only holds when its index field says consulted; otherwise the index was not consulted and the name may still exist.

Capabilities

Features and capabilities supported by this server

Protocol revision2025-11-25

Capability	Details
`tools`	{ "listChanged": false }
`prompts`	{ "listChanged": false }
`resources`	{ "subscribe": false, "listChanged": false }
`experimental`	{}

Tools

Functions exposed to the LLM to take actions

Name	Description
lean_buildA	Build the Lean project and restart LSP. Use only if needed (e.g. new imports).
lean_code_actionsA	Get LSP code actions for a line. Returns resolved edits for TryThis suggestions (simp?, exact?, apply?) and other quick fixes.
lean_completionsA	Get IDE autocompletions. Use on INCOMPLETE code (after `.` or partial name).
lean_declaration_fileA	Get declaration source with the source-line range and surrounding context. `Generated declarations include their source declaration when it is clear. Set full_file=True for the whole file (can be very large).`
lean_diagnostic_messagesB	Get compiler diagnostics (errors, warnings, infos) for a Lean file.
lean_file_outlineA	Get imports and declarations with type signatures. Token-efficient.
lean_get_widget_sourceA	Get JavaScript source of a widget by hash. Useful for understanding custom widget rendering logic. Returns full JS module - may be large.
lean_get_widgetsA	Get panel widgets at a position (proof visualizations, #html, custom widgets). Returns raw widget data - may be large.
lean_goalA	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_premiseA	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_infoB	Get type signature and docs for a symbol. Essential for understanding APIs.
lean_leanfinderA	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_leansearchA	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_searchA	Fast local search to verify declarations exist. Use BEFORE trying a lemma name.
lean_loogleA	Search Mathlib by type signature via loogle.lean-lang.org. Examples: `Real.sin`, `"comm"`, `(?a → ?b) → List ?a → List ?b`, `_ * (_ ^ _)`, `\|- _ < _ → _ + 1 < _ + 1`
lean_minimal_hypothesesA	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_attemptC	Try multiple tactics without modifying file. Returns goal state for each.
lean_profile_proofA	Run `lean --profile` on a theorem. Returns per-line timing and categories. SLOW - avoid on theorems that already hit heartbeat limits.
lean_referencesA	Find all references to a symbol (including the declaration). Position cursor at the symbol.
lean_run_codeB	Run a code snippet and return diagnostics. Must include all imports.
lean_term_goalB	Get the expected type at a position.
lean_verifyA	Check theorem axioms + optional source scan. Only scans the given file, not imports.

Prompts

Interactive templates invoked by user choice

Name	Description
No prompts

Resources

Contextual data attached and managed by the client

Name	Description
No resources

Deploy Server

Shareable, User-Owned Context BackendPeople, applications, and agents read, write, and coordinate together in one context lake. Reach it over MCP, a CLI, a Python SDK, or REST.fulcradynamics.comAd

TDQS

B3.4/5.0

Scored 2026-11-05 09:10 across 22 tools

Disambiguation3/5

Most tools target distinct Lean/LSP operations, but there are four search-related tools (local_search, leanfinder, leansearch, loogle) plus related position-inspection tools (goal, term_goal, hover_info, declaration_file). Descriptions help distinguish them, but the overlap creates real misselection risk for an agent.

Naming Consistency4/5

All tool names use a consistent lean_ snake_case prefix. The underlying pattern is mostly noun/feature-based rather than strictly verb_noun, with minor awkwardness in lean_leanfinder and lean_leansearch, but overall naming is predictable.

Tool Count3/5

The domain is broad enough to justify many capabilities, but 22 tools is a heavy surface for an MCP server. It sits in the borderline 16-25 range and could likely be consolidated or grouped without losing much functionality.

Completeness4/5

The tool set covers the main Lean proof workflow: inspection, search, diagnostics, goal state, code actions, verification, profiling, and widgets. Gaps remain for full LSP coverage, such as rename/formatting operations, but core proof-development needs are well supported.

Maintenance

ActivityActive

ResponsivenessSyncing