Lean LSP
JSON →Interact with the Lean theorem prover via the Language Server Protocol (LSP), enabling LLM agents to understand, analyze, and modify Lean projects.
Install
npx @modelcontextprotocol/inspector Tools · 1
- lean_lsp MCP server for Lean LSP
Environment variables
LEAN_LSP_MCP_TOKENLEAN_STATE_SEARCH_URLLEAN_HAMMER_URLLOOGLE_URL
Links
★ 386 GitHub stars