lean-lsp-mcp

An MCP server giving AI agents access to Lean proof states, diagnostics and search.

• Developer / Organization: Oliver Dressler and contributors
• Category: Open-source skills & interfaces
• Purpose: Expose Lean editor and search capabilities to AI agents.
• Key features: MCP access to Lean goals, diagnostics and search for use inside an agent harness.
• Availability: Open-source software; MIT
• License: MIT (source (opens in a new tab))
• Website / Source code: https://github.com/oOo0oOo/lean-lsp-mcp (opens in a new tab)
• Version: GitHub release v0.31.0
• Version source: Official release or documentation (opens in a new tab)
• Last checked: 2026-11-01