Lean 4 MCP server for proof-state queries, offline navigation, and C FFI inspection.
Query interactive tactic or term goals at a cursor position in .lean files.
Look up Lean declarations and jump to definitions using the offline .ilean cache.
Analyze module import/dependency hierarchies forward, reverse, or both.
Inspect Lean @[extern] declarations, C implementations, and Lean sysroot include flags.
Click on "Deploy Server".
Wait a few minutes for the server to deploy. Once ready, it will show a "Started" state.
In the chat, type @ followed by the MCP server name and your instructions, e.g., "@lean-lsp-mcp Show me the proof state at line 42 in MyTheorem.lean"
That's it! The server will respond to your query, and you can continue using it as needed.
Here is a step-by-step guide with screenshots.
lean-lsp-mcp is an open-source, standalone Model Context Protocol (MCP) server
providing AI coding agents (Claude Code, Cursor, Windsurf, Zed, Antigravity) with
high-performance tools for Lean 4 formal verification, offline navigation, and C FFI
inspection.
NB! Still pre-alpha!
From npm (published bin lean-lsp-mcp / lean4-lsp-mcp):
npx lean4-lsp-mcp
# or
npm install -g lean4-lsp-mcp
lean-lsp-mcpFrom a clone:
git clone https://github.com/r-irbe/lean4-lsp-mcp.git
cd lean4-lsp-mcp
npm install
npm run build
node dist/index.jsThe server speaks MCP over stdio. Point your Lean 4 project at the process
working directory (or set LEAN_PROJECT_ROOT); elan / lake should be on PATH.
Related MCP server: lsp-mcp-server
Interactive Proof State & AltProof Advisor (lean_goal): Queries $/lean/plainGoal (target: "tactic" or "filtered"), $/lean/plainTermGoal (target: "term"), or the static/hybrid AltProof tactic & route advisor (target: "altproof") via persistent lake serve broker sessions.
Live Diagnostics & Abstract Interpretation (lean_diagnostics): Streams compiler elaboration errors, warnings, unsolved goals, and static abstract-interpretation certificates (NatSubTruncation on a - b without b <= a, NatDivModByZero on / d without 0 < d).
Counterexample-First Proving (lean_counterexample_search): Synthesizes and runs an isolated Plausible property test outside the project root using Galois-pruned interval domains (a <= 100, 0 < d, a + b <= 100) and AST threshold constants (strategy: "slice" | "dense").
Sub-5ms Offline .ilean Navigation (lean_lookup_symbol, lean_decl_references, lean_module_hierarchy, lean_dependency_subgraph): Direct binary/JSON parsing of .lake/build/lib/**/*.ilean files for instant jump-to-definition, declaration reference graphs (uses / usedBy), and module import/dependent DAGs without starting lake serve.
Unified Multi-Source Search & Librarian Concordance (lean_search, lean_book_index_lookup, lean_cross_itp_concordance): Local ripgrep declaration search, Loogle, LeanSearch, Reservoir, arXiv, Kuzu knowledge graph, 65+ author-curated textbook indexes, and cross-prover tactic concordance (lean4, coq, isabelle, hol_light, agda).
Metrics, Axiom Closure, Blueprints & C FFI (lean_metrics, lean_module_census, lean_axiom_closure, lean_blueprint, lean_blueprint_scaffold, lean_proof_skeleton, lean_ffi, lean_exec, lean_resync, lean_server_status): Project censuses, Milner Place-Link bigraph projections, #print axioms trust checks, PlasTeX Blueprint scaffolding, and C FFI sysroot inspection.
+-----------------------------------------------------------------------------+
| lean-lsp-mcp ARCHITECTURE |
+-----------------------------------------------------------------------------+
| |
| [ AI Host ] (Antigravity / Claude Code / Cursor / Windsurf / Copilot) |
| | |
| stdio JSON-RPC (MCP Protocol) |
| v |
| [ lean-lsp-mcp Server ] |
| |-- Request Dispatcher, Alias Normalizer & LRU Search Cache |
| |-- .ilean Zero-Latency Indexer (Sub-5ms symbol & reference lookup) |
| |-- Abstract Interpreter (Interval/Zone/Octagon + AltProof Advisor) |
| |-- Plausible Counterexample Harness (Galois-pruned scratch runner) |
| |-- Lake Serve Broker Client (Multiplexed persistent FileWorkers) |
| |-- Clangd C FFI Sysroot Bridge (Injects `lean --print-prefix` headers) |
| | |
| +---> Lean 4 Toolchain (`lake serve` broker / `lake env lean`) |
| +---> Project Filesystem (`.lake/build/lib/**/*.ilean`, `.olean`) |
| |
+-----------------------------------------------------------------------------+See instructions.md for full copy-paste examples and parameter pitfall notes.
Tool Name | Required Parameters | Key Optional Parameters |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| (none) |
| (none) | (none) |
|
| (none) |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| (none) |
|
|
|
|
|
| (none) |
| (none) |
|
Prefer the published bin. After a local clone and npm run build, you can
also use node dist/index.js.
~/.claude/claude_desktop_config.json or project .mcp.json){
"mcpServers": {
"lean-lsp": {
"command": "npx",
"args": ["-y", "lean4-lsp-mcp"],
"env": {
"PATH": "${HOME}/.elan/bin:/usr/bin:/bin"
}
}
}
}The server serves the project it is launched in. Root resolution is: the
LEAN_PROJECT_ROOT directory when set, else the launch directory when it holds
a Lake marker, else the nearest Lake root above it, else the launch directory
unchanged (never another project). Lake markers are lakefile.lean,
lakefile.toml, lake-manifest.json, and packages/; a directory with only
lean-toolchain is used as a last resort.
Pin the root explicitly when your host starts MCP servers from an unrelated working directory:
{
"mcpServers": {
"lean-lsp": {
"command": "lean-lsp-mcp",
"env": { "LEAN_PROJECT_ROOT": "/path/to/your/lake/project" }
}
}
}lakefile.toml projects are fully supported (lake env lean is used for every
Lean invocation, so project modules are on LEAN_PATH). lean_server_status
reports the resolved root, how it was found, and the exact stdin invocation in
use.
.cursor/mcp.json){
"mcpServers": {
"lean-lsp": {
"command": "lean-lsp-mcp"
}
}
}From a clone, after npm run build:
{
"mcpServers": {
"lean-lsp": {
"command": "node",
"args": ["dist/index.js"]
}
}
}Cross-language C FFI inspector: Lean @[extern] declarations, C implementations, and Lean sysroot include flags
| Name | Required | Description | Default |
|---|---|---|---|
| action | No | FFI inspection action (default: inspect) | |
| externName | No | Optional Lean @[extern] identifier or C function name |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the burden of behavioral disclosure. 'Inspector' implies a read-only, informational operation, and the listed artifacts show scope, but the description does not explain what each action returns, whether side effects occur, or how 'jump_to_c' behaves in a headless/agent context.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single, front-loaded sentence with no filler. Every phrase adds meaningful information about the tool's domain and scope.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
This is a multi-action tool with no output schema and no annotations, so the description should clarify what the 'sysroot', 'inspect', and 'jump_to_c' actions actually produce or do. The enum names are suggestive, but the description does not explain return values or action semantics clearly enough for fully confident agent invocation.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so the input schema already documents both 'action' and 'externName' adequately. The description adds domain context for the tool's purpose but does not elaborate on parameter-specific behavior beyond what the enum and descriptions provide.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description names a specific operation ('inspector') and a precise resource domain: Lean @[extern] declarations, C implementations, and sysroot include flags. It clearly distinguishes this tool from the sibling Lean goal/symbol/module tools, which concern different aspects of the Lean environment.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The description provides clear context: use this when working with Lean's C FFI layer, extern declarations, or C implementation navigation. It does not explicitly name alternatives or when-not-to-use conditions, but the domain is specific enough that no exclusions are necessary.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Queries interactive Lean 4 tactic proof state at cursor position ($/lean/plainGoal)
| Name | Required | Description | Default |
|---|---|---|---|
| col | No | 1-based column number | |
| line | Yes | 1-based line number | |
| filePath | Yes | Absolute or relative path to the .lean file | |
| character | No | Synonym for col |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations provided, the description carries the full behavioral burden. 'Queries' implies a read-only operation and 'interactive proof state' indicates it depends on an active Lean session, which is useful. It does not disclose what the returned goal state looks like or whether the file must be open/saved, leaving some behavior implicit.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single sentence with no filler. It front-loads the core action and resource, and the embedded LSP method adds precise context without extra length.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a simple query tool, the description covers the essential purpose and location semantics. However, with no output schema and no annotations, details about the return value and operational prerequisites (e.g., file must be open in a Lean session) are left unspecified.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so the schema already documents all four parameters. The description adds only the general notion of 'cursor position', which loosely ties filePath, line, and col/character together but does not add meaningful detail beyond the schema.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description uses a specific verb ('Queries') and names a precise resource: 'interactive Lean 4 tactic proof state at cursor position'. It also includes the LSP method identifier ($/lean/plainGoal), which adds precision. It does not explicitly contrast with the sibling lean_term_goal, though 'tactic proof state' implies a distinction.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The phrase 'at cursor position' conveys that the tool should be used when an agent needs the proof state at a particular location in a Lean file. However, it provides no explicit guidance on when to choose this tool over lean_term_goal or other siblings, and no exclusions are stated.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Offline zero-latency symbol lookup and jump-to-definition via pre-compiled .ilean cache
| Name | Required | Description | Default |
|---|---|---|---|
| symbol | Yes | Lean declaration name (e.g. RealQ.bellmanOp or BoundedRewardKernel) | |
| preferOfflineIlean | No | Use fast .ilean cache (default true) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the behavioral burden. It discloses that the tool operates offline, uses a pre-compiled .ilean cache, and is optimized for zero-latency lookups, which are meaningful beyond the schema. It stops short of stating whether cache writes or refresh operations can occur, but for a lookup operation the read-only intent is reasonably clear.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
A single well-formed sentence that front-loads the primary action and then specifies the mechanism. There is no redundancy or filler.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
For a two-parameter lookup tool with full schema descriptions, the description plus schema is largely sufficient for an agent to select and invoke it. It does not describe the return payload or cache-miss behavior, but the core selection and invocation context is present.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema coverage is 100%, so the parameter meanings are already fully documented. The description adds no additional semantics beyond reinforcing the cache behavior already reflected in preferOfflineIlean.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
States a specific verb and resource: symbol lookup and jump-to-definition, with the exact mechanism (.ilean cache). This is clearly distinct from sibling tools focused on goals, module hierarchy, or FFI inspection.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
The intent is implied: use this when you need a fast offline symbol lookup or jump-to-definition. It does not explicitly state when to prefer or avoid sibling tools, so no exclusion guidance is provided.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Forward and reverse module import dependency hierarchy analysis
| Name | Required | Description | Default |
|---|---|---|---|
| direction | No | Direction of dependency traversal (default: both) | |
| moduleName | Yes | Full module name (e.g. EASCI.ReinforcementLearning.Core) |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
With no annotations, the description carries the full disclosure burden. It does convey that traversal can be forward/reverse and that the subject is dependency hierarchy, but it does not say what the tool returns, whether dependencies are direct or transitive, or what 'analysis' produces. Some behavior is disclosed, but key traits are left implicit.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
A single compact phrase with no filler; the subject and directional scope are front-loaded. Every word contributes to the meaning, so it earns a top conciseness score.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
There is no output schema and no annotations, so the description needs to specify the result shape or behavioral outcome, but it only labels the operation as 'analysis'. For a tool that returns a hierarchy, the absence of any return/format or depth information leaves an agent without a clear model of what invoking it will produce.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
Schema description coverage is 100%, so the schema already explains moduleName and direction values. The description adds the forward/reverse framing but no additional parameter semantics beyond the enum descriptions, matching the baseline for full schema coverage.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description identifies the resource as module import dependency hierarchy and the key scope axis as forward/reverse, which is distinct from the sibling tools that target goals, symbols, and FFI inspection. It lacks a direct action verb like 'returns' or 'computes', so it is clear but not maximally explicit.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
No when-to-use guidance or alternative routing is given. The intended use is inferable from the name and sibling list, but the description never states when to choose this over other Lean inspection tools or what the prerequisites are.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Queries expected term type under cursor ($/lean/plainTermGoal)
| Name | Required | Description | Default |
|---|---|---|---|
| col | No | 1-based column number | |
| line | Yes | 1-based line number | |
| filePath | Yes | Absolute or relative path to the .lean file | |
| character | No | Synonym for col |
Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?
No annotations are provided, so the description carries the full burden of behavioral disclosure. The verb 'queries' implies a read-only operation, but nothing else is revealed—no mention of error cases, return format, or prerequisites. The tool's behavior depends on the file state, and the description offers no hints.
Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.
Is the description appropriately sized, front-loaded, and free of redundancy?
The description is a single, front-loaded sentence that states the purpose immediately and includes the protocol method in parentheses as supplementary info. There is no fluff or redundancy.
Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.
Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?
The description provides the core purpose but does not elaborate on return values or edge cases, and there is no output schema to fill that gap. For a simple query tool, it is minimally adequate but lacks richer context that could help an agent understand the tool's full behavior.
Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.
Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?
All four parameters are already documented in the schema with descriptions (e.g., column is '1-based column number', line is '1-based line number'). The tool description adds no parameter-specific meaning, but with 100% schema coverage, the baseline of 3 is appropriate.
Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.
Does the description clearly state what the tool does and how it differs from similar tools?
The description states a specific verb ('Queries') and a clear resource ('expected term type under cursor'), making the tool's function unambiguous. It also differentiates from siblings like lean_goal (queries goals) and lean_lookup_symbol (looks up symbols) by focusing on term type at a cursor position.
Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.
Does the description explain when to use this tool, when not to, or what alternatives exist?
No guidance is given on when to use this tool versus its siblings. The description does not mention any selection criteria, alternatives, or exclusions. An agent is left without context on when this tool is the right choice compared to lean_goal or others.
Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.
Recent tool additions, removals, and schema changes observed during successful MCP inspections.
v0.1.0lean_c_ffi_inspectlean_goallean_lookup_symbollean_module_hierarchylean_term_goalScored across 5 tools
Each tool targets a distinct concern: tactic proof state, term type inspection, symbol lookup, module dependency analysis, and C FFI inspection. There is no overlap or ambiguity between these operations, even the two goal-related tools are clearly differentiated by context.
All tool names follow a uniform pattern with the 'lean_' prefix and snake_case, using noun-based or verb-noun combinations consistently (e.g., lean_goal, lean_lookup_symbol). The naming is predictable and easy to infer purpose from.
With 5 tools, the server is well-scoped for a Lean LSP integration, providing a focused set of capabilities without redundancy or bloat. Each tool serves a clear purpose in the interactive theorem proving workflow.
The tool set covers essential Lean-specific operations like goal queries and symbol lookup, but lacks common LSP features such as hover, diagnostics, or references. However, for a specialized Lean server, the core proving workflows are well-represented, with only minor gaps.
Architecture compiler for AI code. 11 tools, 92 actions, 872 Lean4 proofs, 100/100 self-cert.
Code intelligence for coding agents: semantic, AST, graph, and full-text search. 279+ languages.
AI-native programming language and toolchain for accountable, verifiable agent-driven development.
Code intelligence platform for AI agents. 20 tools for architecture, security & impact analysis.
