oOo0oOo/lean-lsp-mcp

lean-lsp-mcp – Lean定理証明器のためのMCPサーバー

概要 – Lean 4言語サーバー上で動作する、Pythonベースの Model Context Protocol (MCP) サーバーです。Leanの診断情報、ゴール、ホバー情報、および一連の検索ツール (LeanSearch, Loogle, Lean Finder, Lean Hammer) を tools として公開し、LLMエージェント (Claude Code, Cursor, Mistral Vibeなど) が呼び出せるようにします。つまり、LLMがコードアシスタントのようにLeanプロジェクトと対話できるようになります。

主な機能

• Leanの診断情報、現在の証明ゴール、項の定義、ホバードキュメントのクエリ。
• 外部検索サービス (LeanSearch, Loogle, Lean Finder, Lean Hammer) を実行して関連する定理を特定。
• 高速なコード実行のためのオプションのREPLベース lean_run_code。
• 環境変数またはMCPクライアントJSON (VS Code, Cursor, Claude Code, Mistral Vibe) を介して設定可能。
• 3つのトランスポートをサポート：stdio (デフォルト)、streamable-http、およびレガシーな sse。
• 安全なリモートアクセスのためのOpenAIのSecure MCP Tunnelに対応。

導入方法

1. uv Pythonパッケージマネージャーをインストールします (またはNixを使用)。
2. Leanプロジェクトがビルド可能であることを確認します (lake build)。
3. オプションのツールをインストールします – ローカル検索用の ripgrep、高速コード実行用の repl パッケージ、および必要に応じてローカルのLoogleバイナリ。
4. MCP対応IDE (VS Code, Cursor, Claude Code, Mistral Vibe) にサーバーエントリを追加します – ほとんどの例では uvx lean-lsp-mcp を実行する1行の設定で済みます。
5. (オプション) 環境変数を設定して、ログの調整、特定のツールの無効化、タイムアウトの調整、または認証の有効化を行います。

典型的なワークフロー

• LLMが “MyProof.lean の現在のゴールは何ですか？” のようなリクエストを送信します。
• MCPサーバーがLean LSPを呼び出し、ゴール状態を抽出して簡潔なテキストブロックを返します。
• 補題が見つからない場合、LLMは lean_loogle または lean_search を呼び出して、リモートまたはローカルのインデックスを検索し、一致する定理を返します。
• LLMが証明ステップを試したい場合、lean_run_code (REPLモード) または lean_multi_attempt を呼び出してコードスニペットをテストできます。

セキュリティ上の注意

• このサーバーはプロジェクト内の任意のファイルを読み取り、ビルドを実行し、検索ツールのためにネットワークにアクセスできるため、信頼できる環境で実行するか、コンテナ化 (Dockerイメージを提供) してください。
• HTTP経由で公開する場合は、LEAN_LSP_MCP_TOKEN を設定してベアラートークン認証を行うか、OpenAIのSecure MCP Tunnelを使用してください。

利用状況

• エージェントベースの定理証明システムを構築する研究者 (例: Ax-Prover, Numina-Lean-Agent, MerLean, M2F) がこのツールを引用しています。
• Lean Together 2026などのカンファレンスで発表されています。

詳細情報

• PyPIパッケージ: lean-lsp-mcp
• ソースコードとドキュメント: https://github.com/oOo0oOo/lean-lsp-mcp
• ツールの全リストは docs/tools.md を参照
• 新しいツールの追加方法は docs/adding-a-tool.md に記載されています。

ライセンス – MIT (引用を推奨しますが、必須ではありません)。