Google DeepMind が発表した「AlphaProof Nexus」は、AI による数学証明のアプローチを根本的に転換する。356 個のエルデシュ問題（未解決の推測）に取り組み、うち 9 件の証明に成功。その中には 56 年間の未解問題 2 件が含まれている。推論あたりのコスト数百ドルという経済的実現性も示し、AI が学術研究の自動化へ進む可能性を示唆した。

Lean コンパイラによる記号的検証フレームワーク

AlphaProof Nexus の強みは、OpenAI の自然言語ベースのアプローチと異なり、Lean 形式化証明言語を用いた完全な自動検証である。システムは Gemini 3.1 Pro を用いて証明の各ステップを Lean の形式言語で生成し、Lean コンパイラが各行をリアルタイムチェック。エラーメッセージが次の試行へ直接フィードバックされる仕組みだ。

この「記号的フィードバックループ」により、統計的な言語モデルも単なる確率的推測ではなく、形式的な正確性に基づいて学習できる。OpenAI の自然言語方式では見落とされる微妙な論理破綻も、Lean は即座に指摘する。

4段階エージェント設計による段階的強化

AlphaProof Nexus は以下の4つのエージェント段階を持つ：

  • Agent(A): 基本的な LLM ループとコンパイラフィードバック
  • Agent(B): AlphaProof の強化学習クエリを統合
  • Agent(C): 進化的コンポーネントと Elo レーティング形式の証明スケッチ比較
  • Agent(D): 全機能を統合した最上位バージョン

このアーキテクチャにより、試行錯誤の効率を段階的に引き上げ、複雑な証明へのアクセス可能性を高めている。

ベンチマーク結果：成功率2.5%、コスト数百ドル

  • Erdős 問題: 356 件中 9 件解決（成功率 2.5%）、うち 56 年間未解 2 件含む
  • 整数列百科事典（OEIS）: 492 の推測中 44 件を証明
  • 代数幾何学: 15 年来のヒルベルト関数問題 1 件を解決
  • 推論コスト: 問題あたり数百ドル（従来の計算コストと比較して破格の安さ）

成功率 2.5% は Erdős 問題ベンチマークの業界標準（1～2%）に近いが、記号的検証による 100% の正確性保証が獲得される。従来は数学者による手検証が不可欠だったが、Lean 形式証明なら機械検証が可能。

業界への影響：開発者・研究者向けの新ツール

AlphaProof Nexus の登場は、AI 推論の用途を「自然言語生成」から「形式的問題解決」へ拡張する先例となった。数学者・暗号研究者・形式検証エンジニアは、AI を 定理証明の半自動化ツールとして活用できる。検証速度と経済性の向上により、学術出版や産業応用での検証プロセスが加速する可能性もある。

同時に、Lean のような形式言語の知識が、今後の AI 開発チームにおいてより重要な資産になることも示唆している。