oOo0oOo/lean-lsp-mcp

解決的問題

本專案在 LLM 代理與 Lean 定理證明器之間建立橋樑。它允許 AI 代理以程式化方式與 Lean 專案互動，使它們能夠分析程式碼、檢查證明狀態，並在無需人工手動在證明器與 LLM 之間複製貼上資訊的情況下，搜尋相關的數學定理與定義。

工作原理

它實作了一個 Model Context Protocol (MCP) 伺服器，透過 leanclient 套件使用 Language Server Protocol (LSP) 與 Lean 通訊。該伺服器公開一組工具，MCP 相容的代理（如 Claude Code、Cursor 或 VSCode）可呼叫這些工具來執行以下操作：

• 檢查 Lean 專案：存取診斷資訊、目標狀態、項資訊與懸停文件。
• 搜尋定理：使用 Loogle、Lean Search 和 Lean Hammer 等外部搜尋工具，尋找現有的證明與定義。
• 執行程式碼：執行 Lean 程式碼片段，支援可選的快速 REPL 模式以加快迭代速度。
• 管理檔案：在專案範圍內讀取與寫入 Lean 檔案。

適用對象

專為從事形式數學、自動形式化與自動定理證明的代理推理系統的研究人員與開發者設計。

特色亮點

• 豐富的工具集：包含目標狀態檢查、本地原始碼掃描（透過 ripgrep）、多種遠端/本機搜尋後端。
• LSP 集成：利用現有的 Lean Language Server 實現對專案的深度分析。
• 彈性部署方式：支援 stdio、HTTP 流式傳輸與 SSE 多種傳輸方式，可於 Docker 容器中執行以獲得更好的隔離性。
• 本地 Loogle 支援：支援執行本地 Loogle 搜尋引擎實例，以避開遠端 API 的速率限制。