Lean MCP
Server Configuration
Describes the environment variables required to run the server.
| Name | Required | Description | Default |
|---|---|---|---|
| ELAN_HOME | No | elan kurulum dizini; PATH'e otomatik eklenir | ~/.elan |
| LEAN_MCP_TIMEOUT_MS | No | Tek derleme denemesi için süre sınırı | 180000 |
| LEAN_MCP_PROJECT_DIR | No | Lean projesinin bulunduğu dizin | ./lean-project |
| LEAN_MCP_MAX_OUTPUT_BYTES | No | Yakalanan derleyici çıktısı üst sınırı | 262144 |
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 | {
"listChanged": true
} |
Tools
Functions exposed to the LLM to take actions
| Name | Description |
|---|---|
| lean_checkA | Verilen Lean 4 kodunu yerel Lean derleyicisiyle çalıştırır. Mathlib ve temel Lean kütüphanesi kullanılabilir. Derleme başarılıysa status=success, başarısızsa derleyicinin hata mesajları diagnostics içinde döner. |
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 1 tool
There is only one tool, so no overlap or misselection is possible. An agent cannot confuse lean_check with anything else.
A single snake_case noun-scoped name (lean_check) is internally consistent and clearly readable. Consistency cannot be violated with one tool.
A server named 'Lean MCP' implies a broader Lean workflow, yet it exposes only one execution tool. There is no tool for separate diagnostics retrieval, file handling, or environment information, making the surface very thin.
Execution plus diagnostics return covers the core 'run Lean code' loop, so the primary use case is served. However, related operations such as managing source files, listing library/version info, or iterative editing are absent, leaving notable gaps.