oOo0oOo/lean-lsp-mcp

何を解決するか

このプロジェクトは、LLMエージェントとLean定理証明器の間の橋渡しを提供します。AIエージェントがLeanプロジェクトをプログラム的に操作できるようにし、コードの分析、証明状態の確認、関連する数学的定理や定義の検索を、人間が証明器とLLMの間で情報を手動でコピー・ペーストする必要なく行えるようにします。

動作方法

leanclientライブラリを使用してLanguage Server Protocol (LSP) を介してLeanと通信するModel Context Protocol (MCP) サーバーを実装しています。このサーバーは、MCP互換エージェント（Claude Code、Cursor、VSCodeなど）が呼び出せる一連のツールを公開しています。具体的には：

• Leanプロジェクトの検査：診断情報、ゴール状態、項情報、ホバー文書のアクセス。
• 定理の検索：Loogle、Lean Search、Lean Hammerなどの外部検索ツールを使用して、既存の証明や定義を検索。
• コードの実行：Leanコードスニペットの実行。高速REPLモードをオプションで利用可能で、反復処理を迅速化。
• ファイルの管理：プロジェクト範囲内のLeanファイルの読み書き。

対象ユーザー

形式数学におけるエージェント型推論システム、自動形式化、自動定理証明の開発に取り組む研究者や開発者向けです。

特徴

• 多様なツールセット：ゴール状態の検査、ローカルソーススキャン（ripgrep経由）、複数のリモート/ローカル検索バックエンドを含む。
• LSP統合：既存のLean Language Serverを活用し、プロジェクトの深い分析を実現。
• 柔軟なデプロイ：stdio、HTTPストリーミング、SSEを含む複数の通信方法をサポート。Dockerコンテナで実行可能で、より良い隔離が可能。
• ローカルLoogleサポート：リモートAPIのレート制限を回避するために、ローカルでLoogle検索エンジンを実行可能。