MCP Servers / development / Lean LSP

Lean LSP

JSON →
stdionone★ 386development

Interact with the Lean theorem prover via the Language Server Protocol (LSP), enabling LLM agents to understand, analyze, and modify Lean projects.

github ↗
Install
How to run this server
[ { "cmd": "npx @modelcontextprotocol/inspector", "imports": [] } ]
server path: lean-lsp
Tools
What this server exposes
lean_lsp
MCP server for Lean LSP
Configuration
Environment & auth
authnone
envLEAN_LSP_MCP_TOKEN
envLEAN_STATE_SEARCH_URL
envLEAN_HAMMER_URL
envLOOGLE_URL
Resources
githubhttps://github.com/oOo0oOo/lean-lsp-mcp ↗
Lean LSP — MCP Server · libregistry