11月12日、Dataconomyが「Nobel panel validates OpenAI's Yang-Mills existence proof」と題した記事を公開した。AIが数十年間誰も解けなかった数学の最難関問題に踏み込んだ——ノーベル賞受賞者を委員長とする専門家パネルがその証明を「妥当」と判断したという事実は、数学・物理・AIの各コミュニティに少なからぬ衝撃を与えている。

ノーベル賞受賞者が委員長を務める審査パネルが承認

ノーベル賞受賞者のDavid Grossが委員長を務める5名の専門家パネルは、OpenAIが機械検証で提出したYang-Mills存在証明を審査し、「量子Yang-Mills理論の存在を証明するものとして妥当である」と結論付けた。

Yang-Mills理論とは、素粒子物理学の標準模型を支える量子場の理論の一つだ。その数学的な厳密な存在証明は、Clay数学研究所が懸賞金100万ドルを掛けたミレニアム懸賞問題の一つに数えられており、数十年にわたって未解決のままだった。

なぜYang-Mills問題はこれほど長く未解決だったのか

Yang-Mills存在問題が難解である根本的な理由は、物理理論としての成功と数学的厳密性のあいだにある深い溝にある。Yang-Mills理論は素粒子の相互作用を記述する理論として実験的に強力な説明力を持つ一方、その背後にある数学——無限次元の関数空間上で定義される経路積分や、連続極限における解の存在——を厳密に定式化することは、既存の数学的道具立てでは手に余る作業だった。物理学者がヒューリスティックに「正しい」と信じてきた結果を、数学として証明するには、まったく異なる方法論の開拓が必要であり、それが数十年の膠着を生んでいた。今回OpenAIが挑んだのは、まさにその正面突破だ。

ただし、今回の評価には重要な留保がある。これはClay数学研究所の100万ドルのミレニアム賞に関する裁定ではない。 Yang-Mills作業部会（Working Group）は、同研究所との現時点での関係を否定しており、今回の証明は問題のもう一つの核心である「質量ギャップ」の存在を証明するものではないと明言している。

質量ギャップとは、真空状態と理論の励起状態を分ける最小の正のエネルギーのことで、ミレニアム問題が要求する証明の中核要件だ。

Leanによる機械検証と審査の内容

OpenAIは9月9日に書面によるYang-Mills存在証明を完成させ、続いて9月18日には量子色力学（QCD）をカバーする証明を生成。10月16日にLeanによる形式化を完了し、同日Grossに証明の管理と公開を依頼した。

Leanは、各論理ステップをソフトウェアが自動検証する「証明支援系（proof assistant）」だ。数学的命題をコードとして記述し、コンピュータが厳密に検証する手法で、近年数学コミュニティでの採用が広がっている。

審査内容としては以下が実施された：

• クリーンビルド（再構築）のパス確認
• 公理の監査（axiom audit）
• コンパレータチェック（エンコードされた定義が、標準的な物理・数学の問題文と一致するかの照合）

証明の具体的な主張は、「任意の単純コンパクトゲージ群に対して、4次元Wilson格子ゲージ理論のスケーリング極限として、Wightman公理を満たす相対論的量子場理論を構成できる」というものだ。

注目すべき点として、パネルは審査にOpenAIのAstraモデルを補助的に使用したと明かしており、「証明を完全には理解していない」とも認めている。また審査はOpenAIが別途作成した書面原稿には依拠していない。

※編集部の考察：Astraモデルはここでは「証明内容の把握を補助するAIツール」として使用されたとみられるが、元記事では詳細な説明がなく、OpenAIが社内で使用している推論・解析支援モデルである可能性が高い。公式な位置付けは現時点では不明だ。

AIが数学証明に挑む意義

今回の事例が特筆されるのは、AIが単に既知の定理を整理・参照したのではなく、未解決の数学的命題に対して新たな形式証明を生成した点にある。Leanのような証明支援系はこれまで主に人間の数学者が補助ツールとして使ってきたが、AIが証明の生成主体となりその後人間が検証するという逆転した構図は、数学研究のプロセスそのものを問い直すものだ。

AIが数学の難問に取り組む試みとしては、DeepMindによるAlphaProofがIMO（国際数学オリンピック）問題を銀メダルレベルで解いた事例が知られているが、ミレニアム懸賞問題のような現代数学の最前線に踏み込んだ事例は前例がなく、今回の取り組みはその点でも際立っている。

未解決事項と今後の公開スケジュール

全1,147ページの証明は未公開の状態だ。作業部会は、品質と正確性に満足した段階で証明と評価レポートをあわせて公開するとしており、現時点で残る課題として以下を挙げている：

• 無限体積極限の一意性
• 一様な質量ギャップの証明
• Wilsonループ面積則

11月10日にはGitHubで2つのリポジトリが公開予定とされていた。一つはOpenAIが10月28日に提出したLeanコード全体、もう一つはパネルによる検証レポートを収録するとされている。また、11月4日付けの第2弾のOpenAI提出物は現在も作業中とされている。

パネルのその他のメンバーは、Michael Douglas、Arthur Jaffe、Igor Klebanov、Nikita Nekrasovの4名で、いずれも数理物理・理論物理の第一線の研究者だ。Grossは現在、カブリ理論物理学研究所の常任メンバーでもある。

AIが数学の最難関問題に踏み込み始めたことを示す事例として、今回の検証結果は数学・物理・AI研究のコミュニティで広く注目を集めるものとなった。

詳細はNobel panel validates OpenAI's Yang-Mills existence proofを参照していただきたい。