lean-lsp-mcp
Server Configuration
Describes the environment variables required to run the server.
| Name | Required | Description | Default |
|---|---|---|---|
No arguments | |||
Instructions
Guidance the server publishes about itself, which clients place ahead of the tool catalog so the model reads it before choosing anything.
This server publishes no instructions, or was last inspected before Glama recorded them.
Capabilities
Features and capabilities supported by this server
Protocol revision2025-11-25
| Capability | Details |
|---|---|
| tools | {} |
Tools
Functions exposed to the LLM to take actions
| Name | Description |
|---|---|
| lean_goalA | Queries interactive Lean 4 tactic proof state at cursor position ($/lean/plainGoal) |
| lean_term_goalB | Queries expected term type under cursor ($/lean/plainTermGoal) |
| lean_lookup_symbolA | Offline zero-latency symbol lookup and jump-to-definition via pre-compiled .ilean cache |
| lean_module_hierarchyB | Forward and reverse module import dependency hierarchy analysis |
| lean_c_ffi_inspectA | Cross-language C FFI inspector: Lean @[extern] declarations, C implementations, and Lean sysroot include flags |
Prompts
Interactive templates invoked by user choice
| Name | Description |
|---|---|
No prompts | |
Resources
Contextual data attached and managed by the client
| Name | Description |
|---|---|
No resources | |
TDQS
Scored 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.