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 |
Capabilities
Features and capabilities supported by this server
| 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_build | Build the Lean project and restart LSP. Use only if needed (e.g. new imports). |
| lean_file_contents | DEPRECATED: Will be removed soon. DEPRECATED. Get file contents with optional line numbers. |
| lean_file_outline | Get imports and declarations with type signatures. Token-efficient. |
| lean_diagnostic_messages | Get compiler diagnostics (errors, warnings, infos) for a Lean file. |
| 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. "no goals" = proof complete. |
| lean_term_goal | Get the expected type at a position. |
| lean_hover_info | Get type signature and docs for a symbol. Essential for understanding APIs. |
| lean_completions | Get IDE autocompletions. Use on INCOMPLETE code (after |
| lean_declaration_file | Get file where a symbol is declared. Symbol must be present in file first. |
| lean_multi_attempt | Try multiple tactics without modifying file. Returns goal state for each. |
| lean_run_code | Run a code snippet and return diagnostics. Must include all imports. |
| lean_local_search | Fast local search to verify declarations exist. Use BEFORE trying a lemma name. |
| lean_leansearch | Limit: 3req/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_loogle | Search Mathlib by type signature via loogle.lean-lang.org. Examples: `Real.sin`, `"comm"`, `(?a → ?b) → List ?a → List ?b`,
`_ * (_ ^ _)`, `|- _ < _ → _ + 1 < _ + 1` |
| 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. |
| lean_state_search | Limit: 3req/30s. Find lemmas to close the goal at a position. Searches premise-search.com. |
| lean_hammer_premise | Limit: 3req/30s. Get premise suggestions for automation tactics at a goal position. Returns lemma names to try with `simp only [...]`, `aesop`, or as hints. |
| lean_profile_proof | Run |
Prompts
Interactive templates invoked by user choice
| Name | Description |
|---|---|
No prompts | |
Resources
Contextual data attached and managed by the client
| Name | Description |
|---|---|
No resources | |