Google DeepMindが開発した数学研究向けAI「AlphaProof Nexus」の研究論文が、2026年10月8日付の科学誌『Science』に掲載された。米国科学振興協会（AAAS）の発表によると、研究チームは未解決の「エルデシュ問題」353件のうち9件、整数数列のデータベース「OEIS」に収録された未解決予想492件のうち44件について、コンピューターで正しさを検証できる証明を発見した。エルデシュ問題の成果には、1970年に提起されて以来、56年間未解決だった二つの問いも含まれる。AIによる数学の問題解決は、数学オリンピックなどの競技問題にとどまらず、実際の数学研究で未解決問題の証明を発見する段階へと進みつつある。
ただし、今回の成果が初めて発表されたのは10月ではない。George Tsoukalas氏らによる論文は5月21日にarXivで公開され、6月8日に改訂されている。今回新たに報じられたのは、その研究が査読を経て学術誌に掲載されたことだ。成果の意義を正しく理解するには、単に解決した問題の数を見るだけでなく、どのような問題を対象とし、AIが生成した証明をどこまで機械的に検証できたのか、そして人間の数学者がどのような役割を担ったのかを確認する必要がある。
エルデシュ問題9件、OEIS予想44件を証明。その成功率は何を意味するのか
AlphaProof Nexusが挑戦した353件のエルデシュ問題は、数学の未解決問題から無作為に選ばれたものではない。
著者らが公開した論文の第3節と付録B.2によると、研究チームは2026年2月初めの時点で、オープンソースプロジェクト「Formal Conjectures」にLean形式で記述されていたエルデシュ問題353件すべてを評価対象とした。
Leanは、数学の命題や証明を形式言語で記述し、その論理的な正しさをコンピューターで検証できる証明支援システムだ。今回の研究では、AIが証明を発見できなかった場合、最大3,000エピソードで探索を打ち切る条件を設けた。ここでいうエピソードとは、AIが複数回のやり取りを通じて証明案を作成し、修正を重ねる一連の試行を指す。
一方、OEIS（On-Line Encyclopedia of Integer Sequences）に収録された予想については、対象の選び方が異なる。
研究チームはまず、整数の並びとその数学的性質を収録するOEISから、未解決の予想2,649件を収集した。そのうえで、Geminiに500件を選ばせた。選定条件は、数学的に興味深く、簡単には解けない一方で、著名な未解決問題を避け、自動証明に適していると考えられることだった。
選ばれた500件のうち、Leanのバージョン更新によって実行できなくなった8件を除外し、最終的に492件を評価した。
| 評価対象 | 試行件数 | 証明に成功した件数 | 対象の選定方法 |
|---|---|---|---|
| エルデシュ問題 | 353 | 9 | 2026年2月初めにLeanで形式化されていた問題を全件評価 |
| OEISの未解決予想 | 492 | 44 | 2,649件からGeminiが500件を選び、実行できなかった8件を除外 |
成功率を計算すると、エルデシュ問題は約2.5％（9÷353）、OEISの予想は約8.9％（44÷492）となる。
ただし、この数字をそのまま「AIが数学の未解決問題を解ける確率」と考えることはできない。エルデシュ問題には、すでにLeanで形式化されている問題に対象が限られるという偏りがある。OEISについては、さらに自動証明に適した問題を選んでいる。
また、解決したとされる9件には、元の問題から派生した別の命題や、同じ問題番号に含まれる複数の設問が含まれる。独立した九つの著名な未解決問題を、それぞれ元の形のまま完全に解決したという意味ではない。
それでも、実際の研究で未解決とされてきた問題に対し、AIが形式的な証明を発見したことは重要な成果といえる。
56年間未解決だった二つの問いを解決
今回の成果で特に注目されるのが、1970年から未解決だった二つの設問だ。
いずれも、数学者ポール・エルデシュ（Paul Erdős）とアンドラーシュ・シャルケジ（András Sárközy）が提起したエルデシュ問題12に含まれる。
この問題は、整数の集合に特定の割り切り関係が生じないようにしながら、どれだけ多くの数を集められるかを問うものだ。
例えば、ある集合に3、7、8が含まれているとする。このとき、7と8の和は15となり、それらより小さい3で割り切れてしまう。
問題12では、このような関係が起きないようにする。つまり、集合から異なる三つの数を選んだとき、最も小さい数が残り二つの和を割り切ることがないようにしなければならない。
最初の設問は、この制約を満たしながら、1からNまでに含まれる要素の数が、Nの平方根に比例する一定の大きさを保つような無限集合を構成できるか、というものだった。
AlphaProof Nexusは、数を小さなグループに分け、それらを十分に離して配置したうえで、無限に組み合わせる方法を見つけた。
証明では、異なる素数で割った余りを調整する「中国剰余定理」と、長さ3の等差数列を含まない集合の構成方法を組み合わせている。これにより、割り切り関係を避けながら、必要な数の多さを確保できることを示した。
二つ目の設問についても、さらに多くの要素を持つ集合を構成することで解決した。ただし、問題12にはほかにも設問があり、問題全体が完全に解決されたわけではない。
もう一つ、成果を理解しやすい例がエルデシュ問題125だ。
この問題では、3進法で表したときに0と1だけを使う非負整数の集合Aと、4進法で表したときに0と1だけを使う非負整数の集合Bを考える。
それぞれの集合から一つずつ数を選んで足し合わせると、さまざまな整数が得られる。では、こうして得られる数は、整数全体の中で一定以上の割合を占め続けるのだろうか。
AIが発見した証明は、その問いに否定的な答えを与えた。
具体的には、得られる数の集合の「下密度」がゼロになることを示した。下密度とは、1からNまでの整数の中で、その集合に属する数が占める割合について、Nを大きくしていったときの下限側の振る舞いを表す指標だ。
下密度がゼロということは、Nを大きくしていくと、得られる数の割合がいくらでも小さくなるような範囲が現れることを意味する。ただし、すべての大きな範囲で割合が一様にゼロへ近づくと証明したわけではない。
この証明では、3の累乗と4の累乗が非常に近い値になる場合があることを利用し、数の分布を異なる規模で繰り返し分析することで結論を導いている。
Geminiが証明を考え、Leanが正しさを検証する仕組み
AlphaProof Nexusの中核にあるのは、大規模言語モデルによる証明の生成と、Leanによる形式検証を繰り返す仕組みだ。
論文の第2節によると、基本構成ではGemini 3.1 Proが証明の方針を考え、Leanで記述されたコードを作成する。そのコードをLeanで検証し、エラーが出れば、その内容を参考にAIが証明案を修正する。
入力として与えられるのは、証明すべき命題や必要な定義を記述したLeanファイルだ。証明がまだ完成していない部分には、sorryという特別な記述が置かれている。
sorryは、Leanで未証明の部分を一時的に残しておくための仕組みだ。AIの仕事は、この未証明部分を実際の証明に置き換え、すべての論理的な手順をLeanが検証できる状態にすることにある。
AIがコードを変更するたびにLeanが確認し、検証に失敗すればエラーメッセージを返す。AIはその情報をもとに、別の証明方針を試したり、補題を追加したりしながら探索を進める。
一度の試行で証明が完成しなくても、それまでに試した方法や残された課題を記録し、次の試行に引き継ぐ。
基本構成では、複数の証明探索エージェントが互いに状態を共有せず、独立して証明を探す。
これに対し、機能を拡張した構成では、途中まで作成した証明案を共有データベースに蓄積し、別のエージェントがその続きを改良できるようにしている。
さらに、Gemini 3.0 Flashを評価モデルとして利用し、証明方針がどれだけ明快か、未証明部分を解決できそうか、発想に新規性があるかといった観点から、複数の証明案を比較する。
評価結果は、チェスなどの実力評価にも用いられるEloレーティングの仕組みで数値化され、次にどの証明案を優先して探索するかを決める材料となる。
このような評価モデルが必要なのは、完成した証明と未完成の証明案では、評価の方法が異なるためだ。
完成した証明はLeanによって論理的な正しさを検証できる。しかし、未完成の証明案については、現時点で正しいかどうかだけでなく、今後の探索によって完成する見込みがあるかを判断しなければならない。
もっとも、評価モデルが高い順位を付けたからといって、その証明案が正しいとは限らない。評価モデルは探索の優先順位を決める役割にとどまり、最終的な証明の正しさはLeanが確認する。
また、拡張構成では、証明の一部を専門的な証明システム「AlphaProof」に任せることもできる。
AlphaProofは、与えられた部分問題について、証明を発見した場合はその結果を返し、反証を見つけた場合は命題が成り立たないことを示す。どちらも得られなければ、解決できなかったことを返す。
Geminiが証明全体の構成を考え、難しい部分を専門ツールに任せることで、複数の方法を組み合わせた探索を実現している。
機械が証明を認めても、元の問題を解決したとは限らない
形式検証を使ううえで重要なのは、Leanが正しいと認めた証明が、本当に元の数学問題に対する答えになっているかという点だ。
Leanでは、未証明部分にsorryが残っていても、コードの型検査を通すことができる。しかし、それは証明が完成したことを意味しない。
そのため、AlphaProof Nexusでは、最終的な証明にsorryが残っていないことを必須条件としている。
さらに、SafeVerifyという検証ツールを使い、元の命題が不適切に変更されていないか、許可されていない公理が追加されていないかなども確認する。
これは、AIが証明できない部分を勝手に正しいと仮定したり、証明すべき命題を簡単なものに書き換えたりして、見かけ上の成功を生み出すことを防ぐためだ。
ただし、こうした仕組みでも解決できない問題がある。それは、自然言語で書かれた数学の問題を、最初からLeanの形式言語に正しく置き換えられているかという点だ。
Leanが検証するのは、あくまで形式言語で記述された命題に対する証明である。その命題が、数学者が本来解こうとしていた問題と一致しているかは、別途確認する必要がある。
研究チームは、エルデシュ問題の証明に成功するたびに、チーム内の数学の専門家が元の問題文と形式化された命題を照合し、両者が一致していることを確認したと説明している。
OEISの予想についても、まず数列の最初の数項が形式化された定義から正しく再現されることを示す「テスト補題」を証明させている。
そのうえで、証明に成功した44件について、形式化が正しいことと、それまで未証明だったことを人間が確認した。
もちろん、数列の最初の数項が一致しただけでは、予想全体が正しく形式化されているとは限らない。機械による事前検証と専門家による確認を組み合わせているのは、そのためだ。
実際に、エルデシュ問題125と741の一部では、元の問題文に含まれる「密度」という言葉の解釈を修正する必要があった。
当初は通常の自然密度として扱っていたものを、それぞれ下密度と上密度に改めたところ、修正後の命題についても証明を得ることができたという。
問題125の公開カタログにも、過去の文献で密度という言葉の意味が曖昧だった経緯が記されている。
この事例は、形式的に正しい証明を発見するだけでなく、そもそも何を証明すべきなのかを明確にすることの重要性を示している。
研究では、AIが証明に失敗した場合の分析も行われた。
例えば、問題の核心となる難しい部分を、元の命題を少し言い換えただけの補題に移し、その補題をsorryのまま残すケースがあった。
また、AIが「数学の文献ですでに証明されている」と主張した補題を人間が調べたところ、実際には存在しない定理だった例も確認された。
つまり、形式検証を組み込んだからといって、生成AIのハルシネーション（もっともらしい誤情報の生成）がなくなるわけではない。
形式検証の強みは、AIが途中で誤った推論や架空の定理を持ち出しても、それらを根拠に未完成の証明を完成品として認めないことにある。
複雑な仕組みがなくても9件を証明、費用は1問数百ドル
今回の研究には、AIによる証明探索システムの設計について、興味深い結果も含まれている。
高度な機能を備えたAlphaProof Nexusの構成が解決した9件のエルデシュ問題について、研究チームは後から基本構成との比較実験を行った。
その結果、証明案の共有や進化的探索、AlphaProofとの連携を使わない基本構成でも、同じ9件すべてを証明できたという。
つまり、汎用的な大規模言語モデルに証明を生成させ、Leanによる検証と修正を繰り返す比較的単純な仕組みでも、研究レベルの未解決問題に対応できることが示された。
ただし、この比較は高度な構成がすでに解決していた9件を対象に、後から行われたものだ。基本構成を使って353件すべてを改めて探索し、同じ成果が得られたことを示したわけではない。
また、複雑な構成が不要だと結論づけられるわけでもない。
論文の第5節によると、難しい問題125と138では、進化的探索とAlphaProofを組み合わせた高度な構成の方が、基本構成などに比べて費用効率が2〜5倍高かった。
一方、それ以外の問題では、高度な構成の費用効率はおおむね半分にとどまった。
証明案を共有するデータベースの管理や、評価モデルによる順位付けにも計算資源が必要になるため、仕組みを複雑にすれば必ず効率が上がるわけではない。
比較的簡単な問題では単純な構成が有利になる一方、難しい問題では複数の探索方法を組み合わせる価値が高まる可能性がある。
この結果は、数学研究AIの性能を高めるうえで、専用モデルの能力だけでなく、汎用モデルにどのような問題を与え、検証器からのフィードバックをどう活用するかが重要であることを示している。
著者らも、基本構成が高い性能を示した背景として、大規模言語モデルそのものの能力向上と、Leanから得られるエラーメッセージの有効性を挙げている。
一方、今回の研究で報告された「1問当たり数百ドル」という費用には注意が必要だ。
この金額は、問題を発見から解決まで導くために必要な総費用ではない。研究チームは353件のエルデシュ問題を幅広く探索しており、その中から証明可能な問題を見つけるだけでも相当な計算資源を費やしている。
また、論文の図3に示された比較費用には、AlphaProof自体の推論コストが含まれていない。
著者らの見積もりでは、AlphaProofには1問当たり約27.5 TPU時間、金額にして約60ドルの費用がかかる。
AIによる探索は試行ごとのばらつきも大きく、同じ問題でも証明が見つかるまでに必要な計算量は一定ではない。
したがって、「数百ドルで未解決問題を解決できる」という数字を、任意の数学問題を持ち込めばその費用で解いてもらえるという意味に受け取るべきではない。人間の数学者による研究費用との単純な比較にも使えない。
数学研究への応用は最適化理論や代数幾何にも広がる
AlphaProof Nexusの成果は、エルデシュ問題やOEISの予想にとどまらない。
研究チームは、最適化理論、代数幾何、グラフ理論など、実際の数学研究にもこのシステムを活用している。
最適化理論では、凸凹構造を持つmin-max問題を解く「Anchored Gradient Descent-Ascent」というアルゴリズムについて、収束性能を保証する新たな結果を得た。
この問題は、一方の変数について目的関数を最小化し、もう一方の変数について最大化するという、二つの相反する操作を含む最適化問題だ。
研究チームは、アルゴリズムの更新幅を決めるパラメータをAIが変更できるようにし、どのような設定ならより強い収束保証を得られるかを探索させた。
その結果、最終反復における勾配ノルムの二乗について、正確なO(1/t)の収束率を証明した。ここでtは反復回数を表し、O(1/t)は、反復回数が増えるにつれて勾配ノルムの二乗の上界がどの程度小さくなるかを示す。
重要なのは、AIが人間の用意したアルゴリズムの正しさを確認しただけではないという点だ。
AI自身がより強い保証を得られるパラメータの設定を探し、その設定でアルゴリズムが収束することまで証明した。
この成果については、4月に独立したプレプリントも公開されている。
ただし、理論上の収束保証が改善したからといって、実際の大規模AIモデルの学習速度が向上したことを意味するわけではない。今回の結果は、滑らかな凸凹問題という特定の条件下で得られたもので、実際のAI学習に適用した場合の高速化を測定したものではない。
代数幾何でも、AIは新たな証明を発見している。
対象となったのは「純粋O列」と呼ばれる数列に関する問題で、余次元3、タイプ2という特定の条件のもとで「対数凹性」が成り立つことを証明した。
対数凹性とは、数列の隣り合う三つの項について、中央の項の二乗が両隣の項の積以上になる性質を指す。
この条件は、数列があるところまで増加し、その後減少するという「単峰性」よりも強い性質だ。今回の証明によって、すでに知られていた単峰性より強い結果が得られた。
ただし、純粋O列のすべてについて対数凹性を証明したわけではなく、対象は特定の条件を満たす場合に限られる。
グラフ理論でも、古くから研究されている「グラフ再構成予想」に関連する成果が報告された。
グラフ再構成予想は、グラフから頂点を一つずつ取り除いて得られる部分グラフの情報をもとに、元のグラフを復元できるかを問う問題だ。
研究チームは、頂点を二つのグループに分け、同じグループ内の頂点同士を辺で結ばない「二部グラフ」に着目し、特定の追加条件を満たす場合に、提案した再構成アルゴリズムが正しく動作することを証明した。
一方、追加条件のない一般的な二部グラフに関する命題は、現在も未解決のままだ。
こうした成果からは、AIによる証明探索が複数の数学分野に広がっていることが分かる。ただし、分野全体の未解決問題を解決したわけではなく、論文の第4節で示されているように、それぞれ証明の対象や成立条件には明確な制約がある。
公開された証明を数学者が検証し、次の研究に生かせるか
Google DeepMindは、AlphaProof Nexusが生成した証明をGitHubの公開リポジトリで提供している。
リポジトリには、Leanで記述された形式的な証明と、その内容を人間が理解しやすい自然言語で説明した証明が収録されている。Lean環境で証明を検証するためのビルド手順も公開されている。
これにより、第三者の研究者は、DeepMindが「証明に成功した」と報告した結果をそのまま受け入れるのではなく、公開された証明を自ら調べることができる。
ただし、ここでも確認すべき点は複数ある。
まず、LeanとSafeVerifyが確認するのは、形式言語で記述された命題に対する証明が論理的に成立しているか、そして証明の過程で不適切な変更が行われていないかという点だ。
次に、人間の数学者は、その命題が元の数学問題を正しく表しているかを確認する必要がある。
さらに、査読や公開後の議論を通じて、研究方法の妥当性や成果の新規性、既存の数学研究にとっての意義が評価される。
機械による形式検証、問題の意味を確認する人間の判断、研究成果としての学術的評価は、それぞれ異なる役割を担っている。
また、完成した証明が公開されていることと、その証明にたどり着くまでの探索過程を誰もが再現できることも同じではない。
今回の研究では、完成した証明を検証する手段が提供されている一方、第三者が同じ探索を実行し、同じ費用で同じ成果を得られることまで保証されているわけではない。
研究チーム自身も、現在のシステムには明確な限界があると認めている。
今回の成功例は、組合せ論や凸最適化、数論など、Leanの数学ライブラリが比較的充実している分野に集中している。大規模な新しい数学理論を構築しなければならない問題や、既存の定義・定理を形式化するだけでも多大な労力が必要な問題には、依然として対応が難しい。
それでも、AIが作成した証明や途中の検討結果が、人間の数学者の研究に役立つ可能性はすでに示されている。
例えば、エルデシュ問題12の公開カタログには、DeepMindが発見した証明が、その後の数学者による議論を通じて簡略化・改善されたことが記録されている。
また、研究チームの数学者らは、AIが最終的な証明を完成できなかった場合でも、途中まで作成した証明案によって問題の構造への理解が深まり、残された難しい部分に検討を集中できたと報告している。
この点は、AIによる数学研究の今後を考えるうえで重要だ。
数学研究では、ある命題が正しいことを証明するだけでなく、その証明がなぜ成立するのかを理解し、より簡潔な方法を見つけ、別の問題へ応用していくことにも価値がある。
AlphaProof Nexusの成果は、AIが未解決問題に対して形式的な証明を発見できることを示した一方で、その成果を数学の知識として定着させるには、依然として人間の理解と検証が欠かせないことも明らかにした。
今後は、解決できる問題の数を増やすだけでなく、発見された証明を第三者がどこまで理解し、簡略化し、別の研究へ発展させられるかが重要になる。
AIが証明を発見し、機械がその正しさを検証し、人間が数学的な意味を読み解いて次の研究につなげる。 AlphaProof Nexusは、そうした人間とAIの協働による数学研究が、すでに現実の成果を生み始めていることを示している。