Lean LSP MCPサーバー

「Lean LSP MCP」サーバーは何をするのか？

Lean LSP MCPは、モデルコンテキストプロトコル（MCP）サーバーであり、leanclientを用いてAIアシスタントとLean定理証明プロジェクトをLanguage Server Protocol（LSP）経由で接続します。これにより、エージェントやLLMがLeanプロジェクトと対話し、診断情報、ゴール状態、項情報、ホバードキュメントなどにアクセス可能となります。この統合により、Leanユーザー向けの開発ワークフローが効率化され、定理検索、コード補完、プロジェクトビルドなどのエージェント向け豊富なツール群が利用できます。Leanのツール群を自動化や対話形式で簡単に利用できるため、開発者・研究者・AIエージェントにとってLeanの活用体験を向上させます。

プロンプト一覧

リポジトリ内にプロンプトテンプレートに関する情報は見つかりませんでした。

リソース一覧

リポジトリ内に公開されているMCPリソースに関する情報は見つかりませんでした。

ツール一覧

• Lean定理検索: leansearch.net連携によりエージェントが定理検索を行えます。
• コード補完: Leanファイル向けのコード補完候補を提供します。
• プロジェクトビルド: Leanビルドシステム経由でプロジェクトビルドを実行します。
• 診断情報: Leanプロジェクト内の診断情報にアクセスできます。
• ゴール状態＆項情報: プロジェクト分析のためにゴール状態や項情報を取得できます。
• ホバードキュメント: Leanコード要素上のホバーでドキュメントを返します。

このMCPサーバーのユースケース

• Leanプロジェクト診断: Leanプロジェクト内のコード正当性やデバッグのための診断情報を即座に取得・提示
• ゴール状態の探索: 証明開発や戦略立案のために現在のゴール状態を取得・表示
• 定理検索: leansearch.netから関連定理を検索し、証明構築を支援
• Lean用コード補完: Lean向けのインテリジェントなコード補完や提案を提供し、生産性向上
• 自動プロジェクトビルド: 自動化フローやエージェントによるコードレビューの一部としてLeanプロジェクトのビルドをトリガー・監視

セットアップ方法

Windsurf

1. uvがインストールされていることを確認してください。
2. プロジェクトルートでlake buildを実行してLeanプロジェクトをビルドします。
3. Windsurfの設定ファイルを探します。
4. 以下のJSONスニペットでLean LSP MCPサーバーを追加します:

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

5. 保存してWindsurfを再起動し、MCPサーバーが稼働していることを確認します。

Claude

1. uvをインストールし、Leanプロジェクトでlake buildを実行します。
2. Claudeの設定ファイルを開きます。
3. MCPサーバー設定を挿入します:

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

4. 保存してClaudeを再起動し、サーバーが利用可能か確認します。

Cursor

1. uvをインストールし、lake buildを実行します。
2. Cursorの設定ファイルを開きます。
3. Lean LSP MCPサーバーを追加します:

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

4. 変更を保存し、Cursorを再起動します。

Cline

1. uvがインストールされていることを確認し、lake buildを実行します。
2. Clineの設定ファイルを見つけて編集します。
3. サーバーを追加します:

   {
     "mcpServers": {
       "lean-lsp-mcp": {
         "command": "lean-lsp-mcp",
         "args": []
       }
     }
   }
   

4. 保存してClineを再起動します。

APIキーの安全な管理

APIキーが必要な場合は、環境変数を用いて安全に取り扱いましょう。例:

{
  "mcpServers": {
    "lean-lsp-mcp": {
      "command": "lean-lsp-mcp",
      "args": [],
      "env": {
        "API_KEY": "${env:LEAN_LSP_MCP_API_KEY}"
      },
      "inputs": {
        "api_key": "${env:LEAN_LSP_MCP_API_KEY}"
      }
    }
  }
}

FlowHuntフロー内でこのMCPを利用する方法

FlowHuntでのMCP利用

FlowHuntワークフローにMCPサーバーを組み込むには、まずフローにMCPコンポーネントを追加し、AIエージェントに接続します。

MCPコンポーネントをクリックし、設定パネルを開きます。system MCP設定セクションで、以下のJSON形式でMCPサーバー情報を入力してください。

{
  "lean-lsp-mcp": {
    "transport": "streamable_http",
    "url": "https://yourmcpserver.example/pathtothemcp/url"
  }
}

設定が完了すると、AIエージェントがMCPのすべての機能や能力を利用できるようになります。“lean-lsp-mcp"の部分は実際のMCPサーバー名に、URLはご自身のMCPサーバーURLに置き換えてください。

概要

ドキュメントおよびコードから判断すると、Lean LSP MCPはLeanプロジェクト向けに強力なツールサポートを提供していますが、明示的なプロンプトテンプレートやMCPリソース定義は現時点でありません。サンプリングやルートサポートについても記載がありません。全体として、Leanユーザーには実用的ですが、MCPの高度な機能の全てを公開しているわけではありません。

MCPスコア