lean-lsp-mcp
JSON →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.
Traffic · last 30 days stale · no recent hits
total hits 16
actors 5 distinct systems
last hit 16d ago human
top countries 🇺🇸 United States · 🇸🇬 Singapore · 🇫🇷 France · 🇬🇧 United Kingdom