Google DeepMindなどの研究者らが、AIによる形式証明探索フレームワーク「AlphaProof Nexus」の論文をarXivで公開した。
大規模言語モデルとLeanを組み合わせ、形式化済みのErdős問題353件のうち9件を機械検証可能な形で証明した。
未解決問題9件をLeanで証明
2026年5月21日、Google DeepMindなどの研究者らは「AlphaProof Nexus」に関する論文をarXivで公開した。
AlphaProof Nexusは、大規模言語モデルと定理証明支援系「Lean（※）」を組み合わせた形式証明探索フレームワークである。
対象となったのは、Erdős Problems repositoryで形式化されていた未解決問題353件で、そのうち9件について「sorry」のないLean証明を出力した。
AlphaProof Nexusは、未完成のLeanファイルを入力として受け取り、Leanコンパイラのフィードバックをもとに誤りを修正しながら証明探索を進める。
基本エージェントはGemini 3.1 Proを使ってLeanコードを修正し、フル機能版ではAlphaProofと進化的探索も組み合わせている。
解決された問題には、1970年にErdősとSárközyが提示した問題 #12(i)、#12(ii) が含まれる。
論文では、この2問が56年間未解決だったと説明されている。
また、問題 #125では、3進表記と4進表記で0と1だけを使う整数集合の和集合について、下密度が0であることを示した。
また、研究チームは、OEISの未解決予想492件にもAlphaProof Nexusを適用した。
その結果、手動レビューで正しく形式化され、未証明だったと確認された44件の予想についても証明を見つけた。
さらに、代数幾何ではHilbert関数に関する約15年未解決だった問題を解決し、最適化理論ではAnchored Gradient Descent-Ascentアルゴリズムの収束率に関する結果も得た。
※Lean：数学の定義、定理、証明をコードとして記述し、各ステップの論理的正しさをコンピュータで検証できる形式証明支援システム。
AI支援は拡大も限界は残る
今回の成果は、AIが数学研究の補助ツールから、証明探索そのものに関与する段階へ進みつつあることを示すものと言える。
数学AIの出力を人間が読むだけでなく、機械が論理的に確認できるため、ハルシネーションや微妙な論理ミスを抑える効果が期待できる。
メリットは、研究者が扱う問題の探索範囲を広げられる点だろう。
非形式的な記述をLeanに落とし込む過程で、定義の解釈や前提条件のずれを見つけられれば、人間の研究プロセスそのものを補強する役割を担う可能性がある。
一方で、今回の成果だけでAIによる数学研究の将来像を断定するのは早いかもしれない。
解決できたErdős問題は353件中9件にとどまり、大半は未解決のままである。
成功例も、Leanの数学ライブラリが比較的成熟し、問題を小さな補題へ分解しやすい領域に多く見られるようだ。
このため、AIが幅広い未解決問題を自動的に解く段階に近づいているとするには、まだ慎重さが必要だろう。
今後は、AIが生成した証明を検証する基盤の拡充と、数学者が対話的に使える設計が重要になりそうだ。
形式証明ベースのAI支援は、数学者を置き換えるものではなく、発想、探索、検証を分担する協働型ツールとして発展していくと考えられる。
関連記事：
Google DeepMind、AIで核融合開発を加速 CFSと提携強化し商業化を推進
