人類数学者への懸賞金が残り少ない？Google DeepMindがエルデシュ問題9問を一挙解決
Google DeepMindは、Gemini 3.1 ProとLean検証器を基盤とするAlphaProof Nexusを発表。50年以上未解決だった問題を含むエルデシュの未解決問題9問を解決し、さらにOEISの44の予想、15年未解決の代数幾何学問題なども証明した。費用は1問あたり数百ドル。
記事インテリジェンス
要点
- AlphaProof Nexusはエルデシュ問題9問（最長56年未解決）を解決。
- システムは4つのエージェントから構成され、最も単純なものはLLMとコンパイラのフィードバックループだけで全問を解決。
- 1問あたり数百ドルという低コストで、AIによる数学発見の可能性を示した。
重要な理由
このニュースが重要なのは、AlphaProof Nexusはエルデシュ問題9問（最長56年未解決）を解決ためです。
技術的影響
モデル選定、推論コスト、プロダクト能力、評価基準に影響する可能性があります。
Google DeepMindは、Gemini 3.1 ProとLean定理証明器を組み合わせたフレームワーク「AlphaProof Nexus」を発表しました。このシステムは、エルデシュの未解決問題9問を解決したと報告されています。その中には1970年に提案され、56年間未解決だった問題も含まれています。
AlphaProof Nexusは4つのエージェントで構成されています。最もシンプルなAgent Aは、Gemini 3.1 ProがLeanの証明コードを生成し、Leanコンパイラがエラーをチェックしてフィードバックを与えるループを繰り返すだけです。この単純な手法だけで9問すべてを解決できたといいます。より高度なエージェントでは、AlphaProof（強化学習ベースのツール）や進化的アルゴリズムを組み合わせていますが、研究者は単純な手法が驚くほど効果的だったと報告しています。
解決されたエルデシュ問題には、数論、組合せ論、幾何学の問題が含まれます。例えば、問題#12は「任意の3つの異なる元a,b,cについて、aがb+cを割り切らない」という条件を満たす無限整数集合の存在を問うもので、AIは中国剰余定理を用いて構築しました。問題#125（1996年）では、特定の進法での桁制限に関する集合の密度がゼロであることを証明。問題#846（1992年）は、局所的には普通だが大域的には分割不可能な平面点集合の存在をラムゼー理論で証明しました。
エルデシュ問題以外にも、OEIS整数列百科事典の44の未解決予想を証明し、代数幾何学における15年未解決のヒルベルト関数の対数凹性問題を解決し、凸最適化におけるアンカー勾配降下法の理論的境界を改善しました。
この研究は、AIによる定理証明が実用的かつ低コストで行える時代が来たことを示しています。全証明コードはGitHubで公開されており、1問あたりのコストは数百ドルです。最も単純なエージェントが複雑なシステムに匹敵する性能を示したことは、大規模言語モデルの進化に伴い、複雑なツールの組み合わせが不要になる可能性を示唆しています。