OpenAI、自社モデルがカケヤ予想の全次元での証明・ETHの反証・ヤン–ミルズ理論の存在証明を出したと発表ETHと物理は外部の研究者グループが担当、公開方針は3件で別々

OpenAIは現地2026年10月26日、自社の内部モデルが数学・計算機科学・物理で3件の成果を出したと発表した。局所平滑化予想の全次元での証明（カケヤ予想の全次元での解決を含む）、指数時間仮説（ETH）の反証、そしてヤン–ミルズ理論とQCD（量子色力学）の数学的に厳密な存在証明である。あわせて、外部の研究者グループが結果を検証・解説する体制と、3件で別々の公開方針（AIの出力を公開／グループを作り公開／グループに公開を委ねる）を示した。証明を計算機で検査するLean（リーン）での形式化の日付も、OpenAIは書いている。

3行まとめ

1. OpenAIが2026年10月26日、自社モデルによる3件の成果（局所平滑化・カケヤ予想の全次元、ETHの反証、ヤン–ミルズ/QCDの存在証明）を発表。いずれもOpenAI側の主張で、外部の検証はこれから。
2. 外部で理解と解説を担うのは、ETHがImpagliazzo氏・Paturi氏・Williams氏、物理がDavid Gross氏ら5人のグループ。局所平滑化は研究者に任せる方針。
3. 局所平滑化とETHはAIの証明原稿とLean証明をGitHubで公開済み。物理はグループが公開を見送った。10月15日に発表済みのSimons Foundationへの500万ドルの拠出が、理解を進める資金として別に用意されている。

本記事の内容は、日本時間10月27日6時台に公式ページで確認したものです。

10月28日追記：この発表のうちETHを中心に、知識ゼロから順に解説した動画（約18分）を YouTube で公開しました。動画を作る中で、公開されたLeanの証明を手元のMacで照合ツールにかけた結果と、同じ日にAnthropicが出したETHの反証を、記事の後半「手元のMacでLeanを回した結果」の節にまとめています。

何が発表されたのか

OpenAIの公式ページ（Research Publication、日付は2026年10月26日）は、3件を「調和解析、計算複雑性理論、場の量子論についての新しい発見」と呼んでいる。同社はこれらの原稿を「生の研究データ」と位置づけ、学術コミュニティが理解に変換するために、外部の専門家に「shepherd（羊飼い）」役を頼んだと説明している。

最後の列について。今回取得した公式ページには、QCDそのもののLean形式化が済んだとは書かれておらず、完了と明記されているのはヤン–ミルズの存在証明だけだ。

3件はそれぞれ何を主張しているのか

局所平滑化予想とカケヤ予想

OpenAIの説明では、局所平滑化予想は1991年にSoggeが提案したもので、波が焦点を結ぶときの極端な集中は長続きしない、という内容だ。2019年にGuth・Wang・Zhangが空間2次元で局所平滑化予想を、2025年にWangとZahlが3次元でカケヤ予想を証明している。OpenAIは「自社のモデルが全次元での局所平滑化予想の証明を出し、したがってカケヤ予想とSteinの制限予想も全次元で解決した」と述べ、新しい証明は「新しい補助的な偏微分方程式」に基づくという。

GitHubのLean形式化の範囲を説明するページ（079.md）には、次元 n ≥ 2 と 2 ≤ p < ∞ について、ユークリッド空間の半波動方程式のL^pノルムを初期値のソボレフノルムで抑える評価がLeanで証明された、と書かれている。カケヤ集合のハウスドルフ次元がnになることも同じ範囲に含まれる。

指数時間仮説（ETH）の反証

ETHは、ブール式の充足可能性問題（SAT）の計算量についての長年の予想で、OpenAIは「数百本の論文で条件付きの計算困難性の導出に使われてきた」と書いている。OpenAIの主張は、自社のシステムがこれが偽であることを証明し、Leanで検証された、というものだ。一方で同社は「実際のアルゴリズムの改善につなげるには、さらに多くの研究が必要」とも書いている。

GitHubの形式化範囲のページ（378.md）によれば、固定の k ≥ 2 について、正規の符号化をした k-CNF の充足割当を数え上げる決定性機械が、準指数時間かつ多項式空間で動くことがLeanで証明されたとある。同ページには「10月25日付の原稿」でさらに鋭い時間の上界が示される、との記述もある。

ヤン–ミルズ理論とQCDの存在証明

物理の成果は、ゲージ場とフェルミオンを含む4次元の相互作用する場の量子論（QCDと、標準模型の統一的な完備化を含む）の、数学的に厳密な存在証明だという。OpenAIは、バラバン（Balaban）の構成的場の量子論の手法に基づくと説明している。部分問題として、純粋ヤン–ミルズ理論の存在証明を含み、これはClay数学研究所のミレニアム懸賞問題「量子ヤン–ミルズ理論」の一部だと書いている。ただし、今回取得したOpenAIのページは、懸賞問題が解決された、あるいは認定されたとまでは書いていない。

誰が、どう確かめるのか

OpenAIは、局所平滑化・ETH・物理で別々の公開戦略を採ったと説明している。外部の専門家の助言に従った結果だという。

ETHのグループの要望として、OpenAIは「生データはすべて公開する」「この仕事が分野全体に与える意味を理解する会議の資金をOpenAIが出す」の2点に同意したと書いている。物理のグループは、連絡窓口をYANGMILLS4D@gmail.comに一本化するよう求めている（OpenAIのページによる）。

協力の原則として、OpenAIは次の4つを挙げている。

• 透明性: 協力の存在を公にする。参加者に秘密保持契約は求めず、議論・中間成果の共有・結論の発表は自由
• 学術的な功績を求めない: 内部モデルが生んだ発見の功績をOpenAIは求めない。まとめ役を頼んだことは、その人や作業グループが最初の発見をしたことを意味しない
• 評価: 理解の形成、書き起こし、その他の資料づくりはグループの功績として認められる
• 独立性: 参加は自発的で無償。結論は各自のもので、OpenAIの代弁者ではない

OpenAI自身も、このやり方にはトレードオフがあると認めている。最初のまとめ役を選ぶことが誰が最初に関わるかを左右し、情報の非対称を生む、という趣旨だ。どの方式がもっとも役立つかはまだ分からない、とも書いている。

資金と、10月6日の発表との関係

公式ページによれば、今回の協力体制は、10月15日に追記された、Simons Foundationへの500万ドルの拠出を補完するものだ。この資金はSimons Foundationが管理・配分し、AIが出した成果を理解し発展させるためのワークショップ、会議、特別プログラムに使われる。10月6日付の「Sharing AI progress in mathematics」の追記には、Simons Foundation支援の研究者にモデルと計算資源も提供する、とある。

10月6日の発表は、内部の最先端モデルによる幅広い数学の結果をGitHubで公開するもので、Lean形式化と、推論の要約・計算量の見積もりも付いていた。同ページには、平均的な結果は「ChatGPT Proで約3時間の思考に相当する計算量」だったと書かれている。当サイトでは、この10月6日のリポジトリを調べた記事を OpenAIが社内AIの数学論文722本を公開 として出している。OpenAIは今回のページで、公開の進め方を学術コミュニティの意見に応じて変え続けていると書いており、今回は外部の専門家の助言で3件の公開方式を分けた形だ。

公式ページを見て気づいたこと

日本時間10月27日6時台にOpenAIの公式ページとGitHubの形式化範囲のページを続けて取得して読んだ。そこで目に留まったのは、日付の置き方だ。OpenAIのページはETHの自然言語の反証を「10月16日」に得たと書く一方、GitHubの378.mdは「10月25日付の原稿」でより鋭い時間の上界を示すとしている。少なくとも、AIが最初に反証を出した日より後の日付の原稿があることになるが、公開された原稿がどの版か、その間に何が変わったかは今回取得したページからは分からない。また、形式化の範囲を示すページはいずれも数式が中心で、一般向けの解説ではなかった。AIが書いた原稿の本体と、Lean本体のコードまでは、今回は読んでいない（Leanは翌28日に手元で実行した。下の追記）。

第三者の判断、QCDのLean、モデル名はまだ見えない

• 第三者の検証結果: 今回の発表は「これから外部のグループが理解・検証する」段階の説明で、確認済みの結論は書かれていない。今回確認した公式ページには、査読や外部専門家による「正しい」という判断は載っていない
• QCDのLean形式化: 公式ページが完了と書いているのはヤン–ミルズの存在証明（10月16日）だけ。QCDについては記載を確認できなかった
• 物理の原稿: 外部グループが公開を見送ったため、証明の中身は第三者がまだ読めない
• ミレニアム懸賞問題との関係: OpenAIは純粋ヤン–ミルズ理論の存在証明が懸賞問題の「一部」だと書くにとどまる。懸賞の審査や認定についての記載は、今回取得したページには見当たらなかった
• 証明を出したモデル: 公式ページは「our models」「our system」と書くのみ。今回取得したページでは、モデル名は確認できなかった。提供については、10月6日のページに「結果を出したモデルを責任ある形で公開すべく取り組んでいる」との記述があるのみで、時期は書かれていない
• 日本での扱い: 研究発表であり、今回取得したページに提供地域や料金に当たる記載はない

手元のMacでLeanを回した結果──Anthropicも同じ予想を崩していた

ここからは10月28日の追記だ。

Anthropicも同じ日にETHの反証を出した

OpenAIの発表から数時間後、Anthropicも自社のAIがETHを崩したとして、49ページの論文「A 2^o(n) Time Algorithm for 3-SAT」とLeanの証明をGitHub（anthropics/formal-math の eth）で公開した。論文の経緯の節によると、中心の解き方を見つけたのは10月16日で、モデルは人の入力なしに出力1,400万トークンを書いた。OpenAIが自然言語の反証を得たと書く日付も10月16日で、2社のAIが同じ日に別々の道具（OpenAIは多項式の補間、Anthropicはテンソルネットワーク）で同じ形の式にたどり着いた、という主張になる。

Anthropicの論文は、この結果の重さと限界を両方書いている。

• Claudeに文献を調べさせたところ、ETHか、それを含むもっと強い仮説だけを前提に自分の結果を出した論文が800本を超えた
• 論文が示した時間の上限が総当たり（2^n）を下回るのは、3-CNFで節の数が変数の5倍のとき、変数の数が10の1万乗を超えてから。論文自身が「Thus our result says nothing about solving formulas in practice.」（だからこの結果は、実際に式を解くことについては何も言っていない）と書いている

このMacで照合ツールにかけた3件

当サイトは動画を作る中で、公開されたLeanの証明を手元のMac（M5 Max・メモリ64GB）で組み立て、公式の照合ツール（comparator）にかけた。照合ツールは、証明が「書かれた問題文」どおりの定理を、許された公理だけで示しているかを確かめる。

Anthropicの定理 MainResults.ethIsFalse が使う公理は、Leanの標準の3つ（propext・Classical.choice・Quot.sound）だけだった。

試しに、OpenAIのETHの定理の文を写し、時間の上限から 2^(…) の項を消して「時間 ≤ 定数 ×（長さ＋1）^d」に書き換えたファイルを作り、本物の証明をそのまま当てた。結果は Type mismatch で止まった。言えるのは「同じ証明では、書き換えた問題文は通らない」までで、書き換えた主張が偽だと示したわけではない。

Leanが通っても、まだ決まっていないこと

• OpenAIのLeanが示しているのは、形式化範囲のページ（378.md）のとおり「この速さで数え上げる機械がある」までで、「だからETHは偽」という最後の一歩は人が読んで確かめる部分だ。Anthropicの方は「ETHは偽」という定理そのものがLeanにある
• どちらも、Leanの問題文が本物のETHと同じ意味かは、機械では確かめられない。AnthropicのREADMEも「Lean checks the proofs, but no machine checks that this file says what the paper says」（Leanは証明を検査するが、このファイルが論文と同じことを言っているかは、どの機械も確かめない）と書いている
• 照合ツールの隔離の仕組み（landrun）はLinux専用なので、Macでは素通しに差し替えて回した。Anthropicの公式の設定にある2つ目の検査器（nanoda）も外している
• ヤン–ミルズは証明が公開されていないので、検査していない

出典と確認時刻

• Working with academic communities to build scientific understanding — OpenAI（2026年10月26日）（日本時間2026年10月27日6時39分に確認）

• Sharing AI progress in mathematics — OpenAI（2026年10月6日、10月15日追記）（同6時40分に確認）

• The Exponential Time Hypothesis is False（Lean形式化の範囲）— openai/math（同6時40分に確認）

• Local smoothing for the Euclidean wave equation（Lean形式化の範囲）— openai/math（同6時40分に確認）

• anthropics/formal-math の eth（論文「A 2^o(n) Time Algorithm for 3-SAT」とLean）— Anthropic（日本時間2026年10月28日に取得し、手元で実行）

• 解説動画「計算機科学の根本が覆る｜ETHをOpenAIとAnthropicが同じ日に反証【これ1本で全てがわかる】」— AI時短ラボ（YouTube・2026年10月28日公開）

本記事は続報があり次第更新します（10月28日：Anthropicの反証と、手元のMacでのLeanの検査を追記）。