{"library":"lean-lsp-mcp","type":"library","category":null,"description":"A Python library implementing the Model Context Protocol (MCP) for integration with the Lean Theorem Prover's language server (LSP). It enables AI agents to inspect Lean environments, check proofs, get goals, and run commands via the Lean LSP. Version 0.26.2 (current) supports Python >=3.10. Release cadence is active, with frequent updates.","language":"python","status":"active","version":"0.26.2","tags":["lean","theorem-prover","mcp","lsp"],"last_verified":"Sun Jun 07","install":[{"cmd":"pip install lean-lsp-mcp","imports":["from lean_lsp_mcp import LeanLspClient"]}],"homepage":"https://github.com/oOo0oOo/lean-lsp-mcp","github":"https://github.com/oOo0oOo/lean-lsp-mcp","docs":null,"changelog":null,"pypi":null,"npm":null,"openapi_spec":null,"status_page":null,"smithery":null,"compatibility":null}