【さすがグーグル】GoogleDeepMindの数学者AI、50年来の未解決難問を一気に9件証明

Google DeepMindの数学証明AIがエルデシュ問題を９件解決

　Google DeepMindの研究チームは、AIによる形式証明探索フレームワーク「AlphaProof Nexus」を開発し、その成果をarXivで発表した。同システムは、大規模言語モデル（LLM）の生成能力と、定理証明アシスタント「Lean」の厳密なコンパイル機構を自律的なループで融合させている。

　LLMが証明のステップをコードとして生成し、Leanコンパイラが論理の正当性を検証する。エラーが発生した場合はその情報をLLMにフィードバックし、コンパイルが成功するまで修正と検証を繰り返す。


　この仕組みにより、LLM特有の論理の飛躍や事実の捏造を排除し、数学的に正しい証明を構築する。同システムは「AlphaProof」と呼ばれる強化学習ベースの定理証明器を内部ツールとして呼び出す機能も持つ。

　特定のサブゴールに行き詰まった際、AlphaProofに証明や反証を委託する。反証された結果は直ちに共有データベースに記録し、他の並行するエージェントが同じ誤ったルートを探索する計算リソースの無駄を防ぐ役割を果たしている。

　同システムは、Erdos Problems repositoryに登録されている未解決問題353件のうち9件を解決した。中には56年間未解決だった問題が2件含まれている。さらに、オンライン整数列大辞典（OEIS）における未解決の予想492件中44件の証明にも成功した。

　1問あたりの推論にかかるコストは数百ドルに抑えられている。代数幾何学、グラフ理論、最適化理論など複数の数学分野でも新たな知見を発見し、実際の研究に応用されている。同時期には、OpenAIの内部モデル「GPT-5.5 Pro」もエルデシュが提起した平面単位距離問題を解決している。

　エルデシュは平面上のn個の点において単位距離となるペアの数について予想を立てていたが、GPTは代数的整数論を用いてこれを反証し、その後人間の数学者がGPTの構築手法を改良した。テック大手によるAI開発競争は、数学の未解決問題を解く能力の向上という形で表面化している。

AlfaProof Nexusがもたらした数学研究のパラダイムシフト

　AlphaProof Nexusがエルデシュ問題を解決した事実は、単なる問題解決を超えて数学という学問の進め方そのものを根底から覆すパラダイムシフトをもたらしている。

　その意義は主に六つの側面に集約される。第一に、高度な独創性を求められ数学者の登竜門とされてきたポール・エルデシュの難問にAIが到達し、五十年以上未解決だった研究レベルのオープンプロブレムを突破した点である。

　第二に、大規模言語モデルと定理証明アシスタントのLeanを組み合わせることで、もっともらしい嘘であるハルシネーションを排除し、人間の主観や疑念を完全に排した絶対的に正しい証明を構築できると実証したことである。

　第三に、これまで天才のひらめきや優秀な数学者の多大な労力に依存していた数学的発見が、一問あたり数百ドルの推論コストに還元され、数学的発見を計算リソースの予算で管理する道を開いた点が挙げられる。

　第四に、整数の解剖学とマルコフ過程理論という異なる抽象領域を結合させるなど、人間が長年見落としていた未知かつクリエイティブな解法を自律的に提示し、テレンス・タオをはじめとする専門家から高く評価された点である。

　第五に、AIは単に問題を解くだけでなく、過去の文献に埋もれていた問題定義の曖昧さや誤った定式化を自律的に発見して修正する役割も担っており、人間は大局的な証明構造のデザインや新しい数理概念の定義といった高次元の探求に集中するという、新たな協調関係が生まれつつある。

　最後に、AIによる証明の量産スピードが人間の査読者のレビュー能力を圧倒することで、既存の学術ジャーナルにおける査読システムが機能不全に陥る状況が生じているほか、高度な証明において誰を発見者としてクレジットすべきかという帰属に関する論争を引き起こすなど、学術コミュニティの制度や文化にルールの再考を迫っている。