lean-lsp-mcp
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 server. | http://leanpremise.net |
| 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_STATE_SEARCH_URL | No | URL for a self-hosted premise-search.com instance. | https://premise-search.com |
Capabilities
Server capabilities have not been inspected yet.
Tools
Functions exposed to the LLM to take actions
| Name | Description |
|---|---|
No tools | |
Prompts
Interactive templates invoked by user choice
| Name | Description |
|---|---|
No prompts | |
Resources
Contextual data attached and managed by the client
| Name | Description |
|---|---|
No resources | |
Latest Blog Posts
MCP directory API
We provide all the information about MCP servers via our MCP API.
curl -X GET 'https://glama.ai/api/mcp/v1/servers/project-numina/lean-lsp-mcp'
If you have feedback or need assistance with the MCP directory API, please join our Discord server