Lean Lsp Mcp

Lean Lsp Mcp provides an MCP server that enables agentic interaction with the Lean theorem prover through the Language Server Protocol, offering tools for LLM agents to access diagnostics, goal states, term information, and hover documentation. The server integrates external search capabilities including LeanSearch, Loogle, Lean Finder, Lean Hammer, and Lean State Search to help agents discover relevant theorems and definitions within Lean projects. It solves the problem of programmatically analyzing and interacting with Lean code by exposing the language server's functionality through a standardized interface that AI agents can use.