Lean LSP MCPとは？
Oliver DresslerによるLean LSP MCPは、Leanの言語サーバーを通じてMCPクライアントを定理証明支援系Leanにつなぎます。エージェントは診断とゴールの状態を読み、ホバーで型を確かめ、複数のタクティクを一度に試し、完成した証明がどの公理に依存しているかを確認し、Mathlibをローカルで、またはLeanSearch、Loogle、Lean Finder、Lean Hammerで検索します。
MITライセンスでPythonで書かれ、GitHubのスターは約548、コントリビューターは28人で、2026年11月3日にv0.33.0をリリースしました。Numina-Lean-AgentやAx-Proverなど、形式数学の自動化に取り組む複数の研究システムが、Leanとのインターフェースとしてこれを挙げています。
Lean LSP MCPのインストール方法
uvx lean-lsp-mcpLean LSP MCPは使う価値があるか？
Lean LSP MCPは、エージェントをLean 4の前に座らせる標準的な方法です。記憶から証明を推測する言語モデルは、正しそうに見えてコンパイルできない文章を出します。このサーバーなら、タクティクごとに最新のゴールの状態を読み、正確なエラーを見て、やり直せます。22個のツールは、数学者がエディターで回す流れを カバーします。lean_goalとlean_diagnostic_messagesで証明の現状を見て、lean_multi_attemptで同じ位置に複数のタクティクを試し、lean_verifyで定理が依存する公理を一覧し（sorryAxのように標準の3つ以外があれば証明は健全ではありません）、lean_buildでプロジェクト全体をビルドします。
エージェントが最も時間を節約できるのは検索ツールです。適切なMathlibの補題を見つけることは形式証明の半分を占めるからです。LeanSearch、Loogle、Lean Finder、Lean Hammerの前提検索など、リモートサービスの多くはそれぞれ30秒あたり3リクエストに制限されており、ドキュメントはこれらの無料サービスに負荷をかけすぎないよう求めています。ローカルのLoogleなら制限はなくなりますが代償があります。開発者の計測では最初のMathlibインデックス作成でメモリ使用量が約13 GiBに達し、ウォームロードでも約7 GiBを使います。
注意点：これはベータ版の研究用ツールで、READMEはリスクを率直に書いています。ビルドと実行のツールはLeanコードを実行し、そのコードはファイルを読み書きできます。リモート検索ツールは問い合わせを第三者のサービスに送ります。ファイル系ツールはプロジェクト、その依存関係、Lean標準ライブラリの範囲に制限され、付属のDockerイメージは既定でlean_run_codeを無効にしています。HTTPトランスポートは既定で127.0.0.1を使い、HTTPとSSEはLEAN_LSP_MCP_TOKENによるBearerトークンを受け付けますが、これは共有の秘密が1つあるだけで、ユーザーごとのアクセス制御ではありません。
結論：エージェントで形式証明をする人にとって、これは選択肢というより基盤設備です。1週間のPyPIダウンロードは約14,700件で 、これを土台にした研究も発表されています。本当の作業はこちら側にあります。クライアントがタイムアウトしないよう先にlake buildを実行し、速度のためにREPLを加え、ローカルでLoogleを使うならメモリを確保してください。
真価を発揮する場面
組合せ論の論文をMathlibで形式化している博士課程の学生
Mathlibの名前をいちいち探さずに定型的な補題を片付ける
エージェントがゴールを読み、LoogleとLeanSearchで合う補題を探し、lean_multi_attemptで複数のタクティクを試し、結果にlean_verifyをかけます。無料ですが、リモート検索の30秒あたり3リクエストという制限がペースを決めます。
フィンテック新興企業の検証エンジニア
コードの変更に合わせて主要な不変条件の機械検証済み証明を最新に保つ
変更のたびにエージェントがLeanプロジェクトを再ビルドし、診断を読み、壊れた証明を直し、lean_verifyでsorryが紛れ込んでいないことを確かめます。付属のDockerイメージで、ソースを読み取り専用でマウントして動かします。
定理証明エージェントを開発するAI研究所
自作せずに信頼できるLeanインターフェースをエージェントに与える
Bearerトークン付きで127.0.0.1のストリーミングHTTPとして提供し、REPLを有効にして断片を高速に実行し、LoogleやLean Hammerを自前でホストして公開サービスの制限を避けます。Numina-Lean-AgentとAx-ProverはどちらもLeanとのインターフェースとしてこれを挙げています。
導入前に確認すること
- 導入
- uvを入れ、Leanプロジェクトでlake buildを実行し、クライアントにuvx lean-lsp-mcpを追加します（VS Codeはワンクリックのボタン、Claude Codeはclaude mcp add lean-lsp uvx lean-lsp-mcp）。任意でローカル検索用のripgrepと高速化用のREPL。Nixにも対応します。
- 連携
- leanclient経由でLean言語サーバー上の22個のツール。LeanSearch、Loogle、Lean Finder、Lean Hammerの前提検索。任意でleanprover-communityのREPLとローカルLoogle。VS Code、Cursor、Claude Code、Mistral Vibeで動作し、ChatGPTとCodexにはOpenAI Secure MCP Tunnelを使います。
- データとプライバシー
- ローカルで動作します。証明コードとゴールはモデル提供元に送られます。検索の問い合わせは、自前でホストするかツールを無効にしない限りリモート検索サービスに送られま す。返されるパスは相対パスにされ、マシンのディレクトリを隠します。
- 大規模利用時のコスト
- MITで無料です。大量に使うなら、制限を避けるためにLoogleやLean Hammerを自前でホストし、ローカルLoogle（ウォームで約7 GiB）と各REPL（既定の予算16384 MiB）に十分なメモリを用意する必要があります。
- 制限
- リモート検索ツールの多くは30秒あたり3リクエストまでです。HTTPとSSEは1つのプロジェクトしか扱えません。REPLのメモリ上限はWindowsでは適用されず、ローカルLoogleはLinuxとmacOSでのみ動作します。
良い点
- タクティクごとに最新のゴール状態と診断
- lean_verifyがsorryや余分な公理に頼る証明を検出
- 4つのMathlib検索サービスとローカル検索
- stdio、HTTP、SSEで動作し、Dockerイメージも付属
気になる点
- リモート検索は30秒あたり3リクエストまで
- ローカルのLoogleはインデックス作成に約13 GiBが必要
- プロジェクトのLeanコードを実行し、自らベータ版と明記
- 先にlake buildを実行しないとクライアントがタイムアウトし得る
おすすめの人
Claude Code、Cursor、VS CodeのエージェントにLean 4の証明を書かせて検証させたい数学者、形式手法エンジニア、研究者。
Lean LSP MCPの代替
Lean LSP MCP：よくある質問
- Lean LSP MCPは使う価値があるか？
- エージェントにLeanの証明を書かせるなら、このサーバーを通して見せるべきです。証明検証器が見ているものをそのままモデルに見せてくれるからです。 評価は5点満点中4.5点です。
- Lean LSP MCPの料金は？
- 無料のオープンソース（MIT）。呼び出すリモート検索サービスは無料のコミュニティサービスです。
- Lean LSP MCPの欠点は？
- リモート検索は30秒あたり3リクエストまで; ローカルのLoogleはインデックス作成に約13 GiBが必要; プロジェクトのLeanコードを実行し、自らベータ版と明記; 先にlake buildを実行しないとクライアントがタイムアウトし得る.
- Lean LSP MCPは誰に向いているか？
- Claude Code、Cursor、VS CodeのエージェントにLean 4の証明を書かせて検証させたい数学者、形式手法エンジニア、研究者。
- チームや本番環境でLean LSP MCPを使うと費用はいくらか？
- MITで無料です。大量に使うなら、制限 を避けるためにLoogleやLean Hammerを自前でホストし、ローカルLoogle（ウォームで約7 GiB）と各REPL（既定の予算16384 MiB）に十分なメモリを用意する必要があります。
- Lean LSP MCPは企業データを扱っても安全か？
- ローカルで動作します。証明コードとゴールはモデル提供元に送られます。検索の問い合わせは、自前でホストするかツールを無効にしない限りリモート検索サービスに送られます。返されるパスは相対パスにされ、マシンのディレクトリを隠します。
- Lean LSP MCPの代わりになるものは？
- 当サイトでレビューした中で最も近い代替はMCP Solver 、 Serenaです。
回答確認日：2026年11月7日
Lean LSP MCPの開発元の方へ：この評価をサイトに掲載できます
