{"slug":"oOo0oOo/lean-lsp-mcp","name":"Lean LSP","description":"Interact with the Lean theorem prover via the Language Server Protocol (LSP), enabling LLM agents to understand, analyze, and modify Lean projects.","category":"development","tags":[],"official":false,"stars":386,"transport":"stdio","install":[{"cmd":"npx @modelcontextprotocol/inspector","imports":[]}],"tools":[{"name":"lean_lsp","description":"MCP server for Lean LSP"}],"env_vars":["LEAN_LSP_MCP_TOKEN","LEAN_STATE_SEARCH_URL","LEAN_HAMMER_URL","LOOGLE_URL"],"auth_type":"none","github":"https://github.com/oOo0oOo/lean-lsp-mcp","homepage":"","server_url":"","status":"active","source":"mcpservers.org","updated_at":"Thu May 28"}