OpenAIのヤン–ミルズの証明：グロス委員会の評価が確認したことと、未解決のまま残ること

2026年11月10日、デイヴィッド・グロスが委員長を務めるヤン–ミルズ・グループは、OpenAIが10月28日にグループへ提出したLeanのコードを、「Validation of the OpenAI Yang–Mills construction」（OpenAIによるヤン–ミルズ構成の妥当性確認）と題する35ページの評価書とともに公開しました。¹冒頭の判断は2つの文から成ります。1つ目は、グループが証明されたと考えていることを述べています。「任意の単純コンパクトゲージ群について、Wightmanの公理を満たす相対論的な場の量子論を、4次元のWilson格子ゲージ理論のスケーリング極限として構成できること」。2つ目は、証明されていないことを述べています。「無限体積極限が一意であることも、質量ギャップがあることも証明していない」。

したがって、ミレニアム懸賞問題は解かれておらず、評価書もそうは述べていません。同じ文書は「私たちはまだ、証明を完全に理解しているとは主張しない」とし、評価はLeanのソースだけに基づいており、OpenAIの別の非形式的な原稿には基づいていないとしています。

以下では、何が公開されたのか、グループが何を証明済みとし、何を証明されていないとしているのか、Leanのコードがどう確認されたのか、そしてグループが自らの審査に認めている限界を順に紹介します。委員会の最初の声明は10月31日の解説記事で、OpenAIの発表は10月27日の解説記事で扱いました。出典はすべて2026年11月11日に確認しました。評価書はグループ自身によるもので、学術誌の査読は受けていません。

ヤン–ミルズ・グループは11月10日に何を公開したのか#

2つの公開GitHubリポジトリです。委員会は前日の3回目の声明で、その公開を告知していました。⁵11月3日の2回目の声明は、確認作業について「この取り組みは順調に進んでいる」と述べていました。⁶

• yang-mills-group/OpenAI-YM-20261028³：OpenAIが10月28日に提出したままのLeanのソースが置かれています。READMEは、定理とその再ビルドの方法についての、OpenAI自身による説明です。
• yang-mills-group/YM²：評価書、提出物のバイト単位で同一のコピー、グループ独自のLeanの検査、日付入りのビルドと検証の記録、そしてそれらを再実行する手順が置かれています。

3回目の声明は評価書を、「この提出物の結果と私たちによる確認、具体的には、物理学と数学で標準的な問題設定に従って、それが純粋なヤン–ミルズ理論の存在を証明していることをまとめた」文書だと説明しています。声明は、11月2日にグループに加わったRon NissimとFred Rajasekaranに謝意を述べています。¹⁰

公開されたのは、Leanのコードだけです。委員会の最初の声明は、モデルが生成した証明は1,147ページに及び、グループの評価とともに「証明の質と正しさに満足したときに」公開するとしていました。⁷その非形式的な原稿はどちらのリポジトリにもなく、評価書は自らについてこう述べています。「別の非形式的な証明の原稿には依拠していない」。

YMリポジトリは、11月4日付のOpenAIの2つ目の提出物を「作業中」として挙げています。²

評価書によれば、OpenAIの提出物は何を証明しているのか#

構成は、ヤン–ミルズ理論を格子の上に置く標準的な方法である、Wilsonの格子ゲージ理論から始まります。評価書は3つの段階を説明しています。¹

次にグループは、こうして作られた対象が、ほかの何かではなくヤン–ミルズ理論なのかを問います。グループが挙げるのは「格子に由来すること、局所場、正規化されたストレステンソル、短距離での主要な法則、演算子積展開」で、これらは「構成がヤン–ミルズ理論を記述していることの実質的な証拠となる」としています。その結果の1つは、ストレステンソルのトレースの2点関数です。その短距離での主要な係数は「摂動論による予言と一致する」とされています。

評価書は、この結果を4つの特徴と比べています。評価書の読み方では、ジャッフェとウィッテンによるクレイの問題記述¹¹が、構成された理論に求めているものです。¹

評価書は何が証明されていないとしているのか#

冒頭のページは、欠けている点を3つ挙げています。「質量ギャップは主張していない。体積の部分列をまたぐ一意性と、成分理論の一致も未解決である」。¹

2つ目と3つ目が重要なのは、段階2のためです。証明が示す限りでは、体積の別の部分列は別の極限を与えるかもしれず、1つの極限の中の成分理論が同じ理論であることも示されていません。グループは、ジャッフェとウィッテンの定式化は「追加の議論によって極限に必要な性質が確立されない限り、コンパクト性によって得られる部分列の極限を不十分とみなす」と書き、再構成定理と局所場の定理は「コンパクト性を超える実質的な情報を与える」としています。グループは自らの基準も述べています。「ここで採用する存在の基準のもとでは、真空状態の正確な特徴づけは求めていない」。さらに、一意性が欠けていることは「無限体積極限と真のヤン–ミルズの真空が一意であるという一般的な予想と矛盾するものではない」と付け加えています。

評価書の第8節は、この研究が扱っていないことを挙げています。

• 収束する部分列だけでなく収束そのもの、そして無限体積極限の一意性
• 連続理論の確率測度
• 「一様な質量ギャップ」
• Wilsonループの観測量と面積則（閉じ込めは通常、これによって述べられる）
• 1粒子状態と、そのエネルギー運動量スペクトル

本文には、さらに2つの限界が出てきます。「全次数での摂動論との一致は、証明されないままである」。そして、自由場による記述を排除する定理は「ガウス場から作られる複合場による記述のすべてを排除するものではない」。

OpenAI自身のREADMEも、同じ線を引いています。「正の質量ギャップ、連続質量の一般化自由場の一般的な排除、全次数でのMS-barのマッチングは、範囲外である」。³

Leanの証明はどう確認されたのか#

評価書は2つの問いを分けています。¹検証（verification）は、証明がその定義と許された公理から導かれるかを問うもので、Leanのカーネルがそれに機械的に答えます。妥当性確認（validation）は、それらの定義が、物理学者や数学者がヤン–ミルズ理論と呼ぶものを述べているかを問うもので、どのカーネルにも答えられません。

再ビルド：Lean 4.32.0によるクリーンビルドで、プロジェクトの9,470のモジュールが約184分で、エラーなしに再ビルドされました。9,477のLeanのソースファイルはすべて、提出物のマニフェストと一致しました。プロジェクトの250,319の宣言を棚卸ししたところ、解答には追加された公理も、Leanのプレースホルダーの公理の使用もありませんでした。主要な証明が使うのは、3つの標準的な公理 propext、Classical.choice、Quot.sound だけです。

Comparator：Leanでは、定理が扱う対象を著者が定義できます。そのため、証明が通っていても、ひそかに別のことを証明している場合があります。評価書はこう書いています。「提出された形式的な開発は、検証の過程で、問題の命題やその土台にある定義の1つを変え、無効な証明が検証を通ったように見せることができる」。Comparatorは、別途固定された参照用の命題に照らして解答を検査するツールです。OpenAIの公開の定理については10月30日に、グループ独自の統合した定理については11月3日に、演算子積展開についての別の命題については11月5日に、それぞれ通過しました。4つの対照テストは、期待どおりに振る舞いました。正しい証明は受理され、命題を変えたもの、禁じられた公理を使ったもの、定義を変えたものは、それぞれ却下されました。

グループ独自のLeanの検査：グループは、A1からA8と名付けた独立のアダプターを書き、構成された対象が、ほかの場所で述べられた要件を満たすことを証明しました。そのうち2つは、提出物を、その外で作られた形式化と比べるものです。1つは以前のプロジェクトによるOsterwalder–Schraderの公理で、グループによれば「独立に、そして私たちがOpenAIのヤン–ミルズの構成を知る前に」定式化されたものです。もう1つは、別の格子ゲージ理論のリポジトリにある、有限のWilson格子の分布です。リポジトリにある範囲に関する文書は、それぞれが何を扱うかを正確に述べています。たとえばOsterwalder–Schraderへの橋渡しは「そのスカラーの族に関するもので、別に規定された、すべての場についてのOSインターフェースに関するものではない」とされ、それが使う解析的な評価はOpenAIの証明から来ています。⁴

人による審査：グループは、「Leanの定義について、広範な（ただし網羅的ではない）人による審査」を行ったと報告しています。

1つの発見は、OpenAI自身が掲げた定理に関わるものです。評価書によれば、提出の後、OpenAIはグループに、公開したComparatorの検査対象 YangMills.jointExistence が「その証明によって確立された、格子による構成とのつながりの一部を省いていた」と伝えました。グループの統合した検査対象はそのつながりを保っており、評価は「したがって、公開の存在命題だけではなく、そのより強い検査対象と以下に述べる確認に基づいている」としています。

グループは自らの審査にどんな限界を認めているのか#

評価書は、それを率直に書いています。¹

• 理解：「提供されたLeanのコードの消化を助けるために、OpenAIのAstraを使った。私たちはまだ、証明を完全に理解しているとは主張しない」。
• 資料：評価したのはLeanのコードだけです。非形式的な原稿は使われていません。
• 帰属：「OpenAIの研究は、多くの物理学者と数学者による先行研究の上に成り立っている。注意深く帰属を示した完全なレビューは、今後の公開で提供する」。
• 隔離：Comparatorの実行は、開発用のランチャーを使ってmacOS上で行われたため、「悪意がありうるビルドコードの隔離は検査していない」。評価書はこう付け加えています。「追加の外部カーネル実装は使っていない」。
• コードの質：グループは、「Leanのリポジトリにあるコードの質について、いくつかの懸念」を表明しています。250,319の宣言のうち、主定理が使うのは100,168で、「宣言とファイルの型破りな命名」を指摘し、Kitchen.lean という名前のファイルの中の Cake や cookie などを例に挙げています。
• 独立性：「私たちのグループとOpenAIの唯一のつながりは、（提出物を受け付けることを除けば）分析を助けるために同社のAstraモデルを使ったことである。私たちのグループは現在、クレイ数学研究所と何のつながりもない」。

リポジトリの提出に関する方針には、今後の公開と同じく今回の公開にも当てはまる一文があります。「提出物を掲載することは、その主張の支持や認証を意味しない」。²グループの規則によれば、評価には「証明が正しいかどうかについての私たちの判断」が含まれ、グループは「AIモデルが生み出した発見について、学術的な功績を求めない」としています。⁸

ヤン–ミルズのミレニアム懸賞問題は解かれたのか#

いいえ。問題が求めているのは存在と質量ギャップで、評価書は、構成が「ジャッフェ–ウィッテンの問題全体を保証するものではない」としています。¹グループはまた、賞を授与するクレイ数学研究所と、現在つながりはないとしています。Papexでは、ヤン–ミルズ方程式の存在と質量ギャップ（英語）は未解決のまま掲載されており、OpenAIの研究は部分的な主張として載っています。

初期の報道の中には、今回の公開を「証明の妥当性が確認された」とまとめたものもありました。より正確にまとめると、次の4つになります。

1. 経験豊かな物理学者と数学者5人に、2人のメンバーが加わったグループが、明示された存在の基準のもとで、Leanの提出物はヤン–ミルズの場の量子論の存在を証明していると判断しています。
2. Leanのカーネル、Comparator、グループ独自のアダプターはいずれも通過しており、誰でもリポジトリから再実行できます。
3. 無限体積極限の一意性、質量ギャップ、閉じ込め、全次数での摂動論との一致は、証明されていません。
4. グループはまだ証明を完全に理解しているとは主張しておらず、非形式的な原稿もまだ公開されていません。

最初の声明から公開までに何があったのか#

これから何が起きるのか#

グループは、まだ果たしていないことを挙げています。「注意深く帰属を示した」完全なレビュー、11月4日の提出物の評価、そして非形式的な証明についての自らの読解です。範囲に関する文書は、11月の提出物の「追加の摂動論的なマッチングの主張」は、この最初のパッケージの範囲外だとしています。⁴リポジトリは、QCDやカイラルなSU(5)ゲージ理論についてのものを含め、さらなる提出の提案を募っていますが、掲載や審査は約束していません。²

ほかの読者にとって、今回の公開はできることを変えます。Leanのコードが公開されたので、再ビルドとComparatorの実行を、プロセスを隔離したLinux上で、2つ目のカーネルも使って繰り返せます。グループの参照用の命題も公開されているので、専門家は定義を読み、それが正しい定義だと同意するかどうかを述べられます。形式的な命題が非形式的な命題と同じことを意味するかというこの問いこそ、人による審査がまだ必要だとグループ自身が述べているところです。⁴

残る問い#

• 無限体積極限は部分列によるのか。成分理論は互いに等しいのか。
• 1,147ページの非形式的な原稿は公開されるのか。公開されるなら、いつか。
• 11月4日の提出物は何を加えるのか。グループの2つ目の評価は、その摂動論的なマッチングの主張を認めるのか。
• 独立したチームが、Linuxでの隔離と外部のカーネルを使って、検査を再実行するか。
• クレイ数学研究所は、問題の存在の半分について何か述べるのか。

出典#

1. Validation of the OpenAI Yang–Mills construction: Assessment 1（ヤン–ミルズ・グループ、2026年11月10日、35ページ）、2026年11月11日確認 ↩ a b c d e f g
2. yang-mills-group/YM：README、提出物、検証の記録（GitHub）、2026年11月11日確認 ↩ a b c d
3. yang-mills-group/OpenAI-YM-20261028：OpenAIによる2026年10月28日のLeanの提出物とそのREADME（GitHub）、2026年11月11日確認 ↩ a b
4. What the formal checks cover（形式的な検査が扱う範囲。yang-mills-group/YM、submissions/openai-20261028/docs/checks.md）、2026年11月11日確認 ↩ a b c
5. Proof by OpenAI of the existence of Quantum Yang-Mills Theory: 3rd Statement by the Shepherding Committee（2026年11月9日）、2026年11月11日確認 ↩
6. Proof by OpenAI of the existence of Quantum Yang-Mills Theory: 2nd Statement by the Shepherding Committee（2026年11月3日）、2026年11月11日確認 ↩
7. Proof by OpenAI of the Existence of Quantum Yang-Mills theory: Statement by the shepherding committee（2026年10月付）、2026年11月11日確認 ↩
8. Rules and Procedures of the Yang Mills Group（KITP、日付なし）、2026年11月11日確認 ↩
9. Statement by the Yang-Mills Working Group（KITP。11月3日と11月9日の更新を含む）、2026年11月11日確認
10. ヤン–ミルズ・グループのメンバー（yang-mills-group/.github、2026年11月8日更新の記録）、2026年11月11日確認 ↩
11. Jaffe and Witten, Quantum Yang–Mills Theory（Clay Mathematics Institute）、2026年11月11日確認 ↩