{"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"],"install":[{"cmd":"pip install lean-lsp-mcp","imports":["from lean_lsp_mcp.client_utils 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,"provenance":{"verified_status":"import_fail","verified_at":"Fri Jul 03","last_verified":"Fri Jul 03","next_check":"Fri Jul 10","install_tag":null}}