leanforge-mcp

leanforge-mcp

Lean 4 で AI 駆動の形式証明検索を行う MCP サーバーです。定理を sorry 付きで送信すると、機械検証済みの証明が返されます。AlphaProof Nexus（DeepMind、2026 年 5 月）の Agent A を実装しています。

技術スタック： Python 3.12+ . FastMCP 3.4+ . FastAPI . React/Vite . Tailwind . Zustand . Biome . Lean 4 / Mathlib

---

目次

• 概要
• クイックインストール
• できること
• ツール
• 要件
• ドキュメント
• ステータス
• ライセンス

---

概要

sorry プレースホルダーを含む Lean 4 の定理を渡すと、N 個のエージェントが並列にループ処理を実行します。LLM が証明の編集案を提示し、Lean コンパイラーが判定し、エラーが LLM にフィードバックされます。sorry を含まないコンパイルに最初に成功したエージェントが勝者になります。

-- Input
theorem sum_formula (n : ℕ) : 2 * ∑ i ∈ Finset.range (n + 1), i = n * (n + 1) := by
  sorry

-- Output (machine-verified)
theorem sum_formula (n : ℕ) : 2 * ∑ i ∈ Finset.range (n + 1), i = n * (n + 1) := by
  induction n with
  | zero => simp
  | succ n ih => rw [Finset.sum_range_succ]; ring_nf; linarith

コンパイラーだけがオラクルです。sorry なしでコンパイルできれば、その証明は正しいということです。

---

クイックインストール

git clone https://github.com/sandraschi/leanforge-mcp
cd leanforge-mcp
uv sync
Copy-Item config.example.toml config.toml

次に、claude_desktop_config.json に追加します。

{
  "mcpServers": {
    "leanforge": {
      "command": "uv",
      "args": ["--directory", "C:\\path\\to\\leanforge-mcp", "run", "python", "-m", "leanforge_mcp"],
      "env": { "DEEPSEEK_API_KEY": "...", "ANTHROPIC_API_KEY": "..." }
    }
  }
}

Lean + Mathlib のワークスペース設定については、INSTALL.md を参照してください（約 4GB、初回のみの設定です。2026-07-09 時点で Goliath にはすでにプロビジョニングされ、検証済みです）。

---

できること

"Prove that the sum of the first n natural numbers is n*(n+1)/2"

"Submit this MiniF2F problem and check back in 10 minutes"

"Show me all the proof attempts for job abc-123 -- why is it stuck?"

"Run validate_lean on this tactic proof to see if it compiles"

---

ツール

ツール	説明
submit_theorem	定理文を送信し、ジョブ ID を取得します（非同期）
submit_lean_file	sorry プレースホルダーを含む .lean ファイル全体を送信します
get_proof_status	ジョブのステータスをポーリングします。完了時には証明を返します
list_attempts	エージェント／ターンごとの試行の経過を確認します
list_jobs	すべてのジョブをステータスの概要とともに一覧表示します
validate_lean	Lean 4 を直接コンパイルします（ジョブ追跡なし）
verify_proof	検証済みカーネル（con-leche、con-ron）で証明済みファイルを再確認します。Lean >= 4.35.0 のワークスペースが必要です。docs/VERIFIED_KERNELS.md を参照してください
cancel_job	実行中のジョブをキャンセルします
leanforge_shutdown	サーバーを正常にシャットダウンします（実行中のジョブをキャンセルして終了します）
get_mathlib_search	Mathlib の定理を自然言語で検索します

---

要件

• Python 3.11+
• elan 経由の Lean 4（winget install leanprover.elan）
• oleans をキャッシュした Mathlib ワークスペース（約 4GB、初回のみの設定。INSTALL.md を参照）
• tier-1 用の deepseek-prover-v2:7b を搭載した Ollama（ローカル、無料）
• tier-2/3 用の DeepSeek または Anthropic API キー（任意）

---

ポートと設定

項目	値
MCP サーバー	stdio（uv run python -m leanforge_mcp）
Web バックエンド（FastAPI）	http://127.0.0.1:10867
Web フロントエンド（Vite）	http://127.0.0.1:10868
設定ファイル	config.toml（config.example.toml からコピーしてください。gitignore 対象です）
環境変数	DEEPSEEK_API_KEY（tier 2）、ANTHROPIC_API_KEY（tier 3）。.env.example を参照してください。キーはサーバー環境に保持され、ブラウザーには渡されません

---

ドキュメント

ドキュメント	内容
INSTALL.md	前提条件、Lean ワークスペースのセットアップ、Claude Desktop の設定
docs/ONBOARDING.md	初めて利用する方向けのセットアップ：費用、注意点、動作確認
docs/CONFIGURATION.md	すべての設定オプションと環境変数
docs/TOOLS.md	パラメーターと使用例を含むツールの詳細リファレンス
docs/ARCHITECTURE.md	証明ループ、段階的なエスカレーション、ジョブのライフサイクル、SQLite スキーマ
docs/LEAN.md	Lean 4 言語リファレンス、タクティックガイド、参考文献、リンク集
docs/VERIFIED_KERNELS.md	verify_proof が存在する理由、con-leche/con-ron とは何か、ワークスペースのアップグレード方法
docs/LEAN_PRIMER.md	エンジニア向け Lean 4 クイック入門（短縮版）
docs/ALPHAPROOF_NEXUS.md	技法：AlphaProof Nexus 論文の解説
docs/COVERAGE_GAP.md	DeepMind が MSM のカバレッジを獲得でき、スタートアップには難しい理由
docs/BENCHMARK_RESULTS.md	MiniF2F、PutnamBench、Erdős の結果
docs/DEVELOPMENT.md	貢献方法、開発環境のセットアップ、テストコマンド
docs/TROUBLESHOOTING.md	よくあるエラーと解決方法
llms-full.txt	LLM 向けの完全なコンテキスト：ツール、エンドポイント、設定、ポート

---

ロードマップ

フェーズ	内容	ステータス
A	コアループ：LLM が提案し、Lean が判定し、エラーをフィードバック	完了
B	正確性の強化、エッジケースへの対応、タイムアウトの調整	完了（2026-07-09） -- デフォルト引数の切り詰めと偽の重複を利用した攻撃に対する改ざん防止機能を実装し、プロセス間のジョブ所有権とキャンセルを修正し、ステートレスなプロンプトへの対策を追加しました。実機で56/56件のテストに合格しています。docs/ASSESSMENT_2026-06-24.md を参照してください
C	パフォーマンスと安全性：REPL ワーカープール（実際のボトルネックはコンパイル時間）、LLM のタイムアウトと再試行、トークンとコストの計測（バッチ実行前に必ずチェック）	進行中 -- TODO.md を参照してください
D	マルチエージェント並列スケジューリング（論文の Agent B）-- N 個のループを並列実行し、最初に完了したものを採用	予定
E	自己批評ステップ -- コンパイル前に LLM が自分の証明をレビューし、明らかなエラーを早期に検出	予定
F	Web アプリの証明エクスプローラー -- 試行した証明経路のインタラクティブなツリービュー、タクティックのリアルタイムストリーミング	予定
G	前提選択 -- タクティックを生成する前に、Mathlib から関連する補題を検索	予定
H	累積コンテキストウィンドウ管理 -- 長いエラーチェーンを単純に連結するのではなく、スマートに要約	予定
I	ベンチマークダッシュボード -- モデルや設定ごとの MiniF2F、PutnamBench、Erdős の結果を追跡する Web アプリのページ	目標
J	人間参加型 -- エージェントが行き詰まったときに一時停止し、人間にヒントを求めるため現在の状態を提示	目標
K	証明のキャッシュ -- 部分証明を重複排除し、繰り返し使う補題を瞬時にコンパイル	目標

各フェーズで可能になること

A + B により、定理を送信して証明を受け取れるようになります。 動作して有用ですが、シングルスレッドで、各ターンでコンパイル全体が必要になり、支出制御もありません。Phase C でこれらの課題を解決します。

D で状況が一変します。N 個のエージェントを並列に動かせば、所要時間は「1 つの LLM にかかる時間」から「N 個の LLM のうち最速のものにかかる時間」へ短縮されます。 LLM が行き詰まる定理では、これにより 5 分かかっていたものが 30 秒になります。

E により、明らかに誤った戦術に LLM がコンパイル時間を費やすのを防げます。 追加コストはわずか（試行ごとに LLM 呼び出しが 1 回増えるだけ）で、論文によると Agent A だけでも解決率が約 15 ポイント向上します。

F はユーザーにとってのメリットです。「status: running」を眺めてポーリングする代わりに、LLM がリアルタイムで戦術を試す様子を確認し、どの経路を断念したかを把握して、最終的に成功または失敗した理由を理解できます。

G は最もよくある失敗モードに対処します。LLM が、現在のコンテキストに存在しない補題に対する正しい戦術を書いてしまうケースです。前提の選択（戦術生成前に行う小規模な検索ステップ）により、この問題を大幅に減らせます。

H は目に見えませんが、非常に重要です。LLM の失敗した試行が 10 回以上に増えると、エラーのコンテキストがモデルのウィンドウを超えてしまいます。スマートな要約により、LLM をノイズで埋め尽くすことなく、関連する情報を維持できます。

ギャップの詳細な分析：docs/ASSESSMENT_2026-06-24.md

---

ライセンス

MIT