概要

Google DeepMindは2026年5月、数学特化AIシステム「AlphaProof Nexus」が353問のエルデシュ未解決予想のうち9問を自律的に証明したと発表した。解決した9問には、56年間にわたって専門数学者が取り組んでも答えが出なかった2問が含まれる。さらに、整数数列のオンライン百科事典（OEIS）に収録された492の未証明予想のうち44問も証明した。成功率は約2〜9%にとどまるものの、これらはいずれも「数十年間、専門数学者がほぼ進展を見ていない知識の最前線」に位置する問題であり、AIが人間の証明を検証するだけでなく独自に発見できることを示した画期的な成果として注目されている。DeepMindはこの成果について、「AGI（汎用人工知能）には程遠い」と明言している。

技術的な仕組み

AlphaProof Nexusは「大規模言語モデルの生成能力」と「Lean形式証明支援システム」を組み合わせたアーキテクチャを採用している。AIが証明ステップをLean言語で提案し、コンパイラが各論理ステップを厳密に検証する。誤りのある証明は即座に却下され、コンパイラから返されるエラーメッセージがフィードバックとして次の試みに反映される反復ループにより精度を高める仕組みだ。

システムは複雑さの異なる4つのエージェント変種（A〜D）で構成されている。最もシンプルなエージェントAはGemini 3.1 ProとLeanコンパイラのフィードバックのみを使用し、B・C・DとなるにつれてAlphaProofの統合、進化的コンポーネント、Eloベースのランキングシステムが段階的に追加される。エルデシュ予想の証明には当初エージェントDが使用されたが、研究チームが事後分析を行ったところ、最もシンプルなエージェントAでも（難問ではコストは高くなるものの）9問すべてを証明できることが判明し、研究者たちを驚かせた。研究者たちはこれを「言語モデルの急速な改善」と「コンパイラのフィードバックがLLMの推論を正しく方向付ける力」によるものだと説明している。

コストと実用的な意義

各問題の解決にかかった推論コストは数百ドルと極めて低コストだった。エルデシュ予想は組み合わせ論・数論・グラフ理論にまたがる難問群であり、従来は高度に専門化された数学者でなければ取り組めなかった領域だ。今回の成果はAIによる形式検証の経済的効率を大幅に改善するものであり、スマートコントラクト監査やゼロ知識証明の生成など、暗号資産産業をはじめとする複数の分野での応用も期待されている。また、AlphaProof NexusはHilbert関数に関する15年来の未解決問題を解決し、凸最適化の既知の上界も改善したとされる。

AGIとの距離と今後の展望

DeepMindはAlphaProof Nexusが「AGIではない」と強調している。エルデシュ予想全体での成功率は約1〜2%にとどまっており、難易度の低い問題に集中していることも数学者テレンス・タオが以前に指摘したAIの特性と一致している。それでも、AIが数十年単位の未解決問題に対して独自の証明を発見できるようになったことは、数学研究とAIの協働という新たな段階への入口を示している。今後は人間の数学者との協働ツールとして、研究の加速に寄与する可能性がある。