Oliver Dressler

lean-lsp-mcp is an MCP server that facilitates interaction with the Lean theorem prover through the Language Server Protocol. It provides tools for LLM agents to understand, analyze, and interact with Lean projects, offering access to diagnostics, goal states, term information, hover documentation, and more. External search tools are also available.