
OpenAIが数学・計算機科学・物理で3つの成果を発表
OpenAIは社内のAIによる新しい発見として、数学・計算機科学・物理学という3分野の成果を発表しました。ただし、どれも専門家による検証はこれからで、OpenAIはAIが出力した原稿を「研究の生データ」と呼んでいます。
OpenAIが発表した3つの成果
| 分野 | AIが出したとする成果 | AI出力の公開 |
|---|---|---|
| 数学(調和解析) | 局所平滑化予想をすべての次元で証明 | 公開 |
| 計算機科学(計算量理論) | 指数時間仮説(ETH)を反証 | 公開(検証グループも結成) |
| 物理学(場の量子論) | QCDを含む場の量子論が4次元で存在することを証明 | 外部グループの判断で見送り |
数学と計算機科学はAIの出力を公開、物理は外部グループが判断
OpenAIがAIの出力を公開したのは数学と計算機科学の2分野で、物理学では公開するかどうかを外部の研究者グループに任せました。OpenAIは成果を理解するためのグループ作りを外部の専門家に要請し、公開の進め方も専門家の助言に沿って成果ごとに分けています。
- 数学:AIの出力をそのまま公開し、研究者が自由に集まって解明に取り組めるようにする
- 計算機科学:外部の研究者でグループを作り、成果の意味を解き明かす。AIの出力も公開し、誰でも検討できるようにする
- 物理学:外部の研究者でグループを作り、資料を公開するかどうかもその研究者たちに任せる
計算機科学のグループは自然言語の証明とLeanによる形式化をすぐに公開すると決め、OpenAIが両方をGitHubで公開しました。Leanは数学の証明が正しいかを機械が1行ずつチェックするプログラミング言語のことで、人の言葉で書いた証明をLeanでチェックできる書き方へ書き換える作業を形式化と呼びます。
物理学のグループはAIが作った成果物を公開せず、解説を独自に書く方針です。どの進め方が最もうまくいくかはまだ分からないと、OpenAIは認めています。
学術的な功績は求めず、外部の研究者に検証を任せる
OpenAIは社内のAIが出した発見について、学術的な功績を求めないとしています。OpenAIが外部の研究者と共同研究を進めるうえでの原則は、次の4つです。
外部の研究者と進める共同研究の4原則
OpenAIはこの進め方の弱点も認めています。最初に取りまとめを担当する専門家を選んだ時点で、先に関われる研究者が限られ、その研究者だけが先に情報を持つことになるとのこと。一方でOpenAIは研究者がAIの成果を検討するワークショップや会議の費用として、サイモンズ財団の新しい取り組みへ500万ドル(約7億9,000万円)を拠出しています。

We are announcing three new discoveries in mathematics, computer science, and physics about harmonic analysis, complexity theory, and quantum field theory. / In our view, these manuscripts are best understood as a form of raw research data. / For the math result, release the AI output, leaving researchers free to organize their own efforts to explain the result. / For the computer science result, form an external group of collaborators to explain the result, while making the AI output publicly available for anyone to examine and build on. / For the physics result, form an external group of collaborators and defer to them on the release of materials. / We do not seek academic credit for the discoveries produced by our internal models. / Participation is voluntary and unpaid. / On the other hand, choosing initial shepherds necessarily shapes who gets involved first and creates asymmetry of information. — 3つの成果、公開の進め方、共同研究の原則と弱点に関する記述より公式情報を見る →
指数時間仮説は「SATを解くには指数時間かかる」という予想
指数時間仮説(ETH)は、論理式を満たす真偽の割り当てを探す問題にはどう工夫しても指数時間がかかるという計算量理論の予想です。OpenAIのプレプリント(査読前の論文)は、この予想が成り立たないと主張しています。
指数時間仮説は数百本の論文で計算の難しさを論じる根拠
ETHは多くの研究者が正しいと考えてきた予想で、数百本の論文で「この問題は速く解けない」と論じる根拠として使われてきました。ETHの対象はSAT(充足可能性問題)です。
SATは「AとBのどちらかは真」のような条件をいくつも並べ、すべてを同時に満たす真偽の割り当てがあるかを判定する問題で、代表例に3-SATがあります。ETHは、3-SATで変数がn個なら最悪の場合に指数時間がかかるとする予想です。指数時間とは、変数が1つ増加するごとに計算時間が一定の倍率で伸びていくことを指し、変数が多いほど計算は手に負えなくなります。
予想を最初に唱えたのはRussell Impagliazzo氏・Ramamohan Paturi氏・Francis Zane氏の3人で、Impagliazzo氏とPaturi氏は今回の検証グループにも加わっています。グラフ理論・計算生物学・データベース・計算幾何学などでは、他の問題が難しいことを「ETHが正しければ」という条件付きで証明した研究が多く、ETHが偽ならこれらの結論は根拠を失います。
OpenAIの論文では解の個数を準指数時間でカウント可能
OpenAIの論文によると、条件を満たす割り当ての個数は指数時間より短い準指数時間で正確にカウントできるとのこと。準指数時間とは、指数時間よりは緩やかだが多項式時間よりは急速に増加する計算時間のことです。論文は、計算に使うメモリも多項式で表せる量に収まるとしています。
個数をカウントできれば、1個以上あるかどうかで「条件を満たす割り当てがあるか」も判定できます。したがって3-SATも準指数時間で解けることになり、ETHは成り立たないと論文は主張しています。
論文の題名は「The Exponential Time Hypothesis is False」(指数時間仮説は偽である)で、著者名はOpenAIです。10月17日付で、25日に改訂されています。
論文は同じ方法を、グラフの彩色と完全マッチングのカウントにも使うことができるとしています。彩色は隣り合う頂点同士が同じ色にならない塗り分け、完全マッチングはすべての頂点を重複なく組にする組み合わせのことで、どちらも準指数時間でカウントできるとのこと。

The computer science collaboration will understand and explain a result concerning the Exponential Time Hypothesis (ETH), a longstanding conjecture about the computational complexity of Boolean formula satisfiability, a problem deeply related to the P vs. NP problem. The ETH has been widely believed to be true, and has been used in hundreds of papers to derive conditional computational hardness results across a wide variety of fields including graph theory, computational biology, databases, computational geometry, and more. / Impagliazzo and Paturi, along with Francis Zane, are the original proposers of the Exponential Time Hypothesis — ETHの位置づけと提唱者に関する記述より公式情報を見る →
We give a deterministic algorithm for exactly counting the satisfying assignments of an arbitrary k-CNF formula. / Testing #F > 0 also decides satisfiability. / However we do obtain subexponential time algorithms for counting graph colorings and perfect matchings. — 要旨と序論の記述より公式情報を見る →
反証は未確定、提唱者らが検証中
ETHの反証はOpenAIが主張している段階で、査読はまだ終わっていません。OpenAIによると、社内のAIが10月16日に自然言語で反証を見つけ、翌17日にOpenAIがLeanで形式化したとのこと。検証は、ETHを最初に唱えた研究者を含むグループが進めます。
ETHの検証グループ
Leanで証明したのは論文の主定理より弱い結果
OpenAIがLeanでチェックを終えたのは、論文の主定理よりも緩い計算時間の上限です。OpenAIが公開したLeanの範囲説明によると、Leanで証明した上限は、10月25日版の論文が導いた上限よりも大きな値とのこと。どちらの上限も準指数時間に収まるため、OpenAIはETHが偽であることをLeanで検証したとしています。
論文における主定理そのものは、まだLeanでチェックされていません。主定理の正しさは、検証グループなど人の専門家が論文を読んで判断することになります。
Anthropicも同じ仮説の反証を公開したのか
Anthropicも、社内の研究用Claudeモデルが見つけたとする3-SATのアルゴリズムを、論文とLean 4の形式化付きで公開しています。公開先のGitHubリポジトリ「formal-math」にあるREADMEは、このアルゴリズムでETHが否定されると説明しました。
機械でチェックできる範囲には限界もあります。Leanは証明をチェックしますが、形式化した定理が論文と同じ内容を述べているかどうかは機械では判定できません。
指数時間仮説の反証で実務の計算がすぐ速くなるわけではない
ETHの反証が正しくても、分かるのは変数が限りなく増加したときに計算時間がどう伸びるかだけです。この結果は実際に論理式を解くときの計算時間については何も述べていません。実際の計算が速くなるまでにはかなりの研究が必要になります。
OpenAIの論文も、一般のNP問題が準指数時間で解けるとまではいえないと認めています。数学の成果をめぐっても、OpenAIは10月7日に社内のAIが生成した数学論文3本を撤回しており、AIの証明は人の検証を経るまで確定しません。
あわせて読みたい:OpenAIの数学論文3本が撤回、符号ミス1つで連鎖的に崩れた理由


Surprisingly, our system has recently proved that the ETH is false, a result that was subsequently verified in Lean. / Finding such algorithms, and turning theoretical advances into practical improvements, will require significant further research. / This work will be verified and shepherded by a group led by Russell Impagliazzo (UC San Diego), Ramamohan Paturi (UC San Diego), and Ryan Williams (MIT). / Our AI found its natural language disproof for the ETH on October 16th, 2026 and then subsequently we formalized the result in Lean on October 17th, 2026 — ETHの反証と検証グループに関する記述より公式情報を見る →
The following describes the scope of the Lean formalization related to the following accompanying paper(s): / Lean proves that a deterministic machine exactly counts satisfying assignments / the October 25 manuscript gives the sharper time bound — Leanで証明した範囲に関する記述より公式情報を見る →
The result is purely asymptotic and says nothing about solving formulas in practice. / The result was discovered by an internal research Claude model. This folder holds the paper and its Lean 4 formalization, which was written by AI models. / Lean checks the proofs, but no machine checks that this file says what the paper says — 結果の位置づけとLeanの限界に関する記述より公式情報を見る →
our result does not imply that general NP problems admit subexponential time algorithms — 序論の記述より公式情報を見る →
掛谷予想とヤン–ミルズ理論の成果も同時に公表
OpenAIは同日に、数学と物理学の成果も公表しました。数学では掛谷予想を導く予想の証明を、物理学では素粒子の強い力を記述する理論の存在証明を、AIが出力したとしています。どちらも専門家による検証はこれからです。
数学の成果は局所平滑化予想の全次元証明
OpenAIによると、AIはSogge氏が1991年に唱えた局所平滑化予想を、すべての次元で証明したとする出力を得たとのこと。局所平滑化予想は、波が1か所に集中しても極端な集中は長く続かないという予想です。AIの証明が正しければ、掛谷予想とスタインの制限予想もすべての次元で解けることになります。
これまでに証明されていたのは一部の次元だけでした。2019年にGuth氏・Wang氏・Zhang氏が空間2次元で局所平滑化予想を証明し、2025年にはWang氏とZahl氏が3次元で掛谷予想を証明しています。
OpenAIがAIの出力を得たのは10月18日で、Leanでの形式化はその翌日に完了しました。OpenAIは専門家の助言を受け、10月6日に数学の論文をまとめて公開したときと同じく、AIの出力をそのまま公開しています。
物理のグループはAI成果物の公開を見送り
物理学では、QCD(量子色力学)を含む場の量子論が4次元で数学的に存在することを証明した、とOpenAIは主張しています。QCDは、クォークやグルーオンのあいだに働く強い力を記述する理論です。
主張には純粋ヤン–ミルズ理論の存在証明も含まれています。この理論の存在は、クレイ数学研究所が懸賞金をかけたミレニアム懸賞問題の一部です。
AIは9月9日にヤン–ミルズ理論が存在する証明を、9月18日にQCDの証明を出力しました。証明が長く複雑なため、OpenAIはLeanでの形式化を待ってから発表しており、ヤン–ミルズ理論の形式化は10月16日に完了しています。
検証は、2004年にノーベル物理学賞を共同受賞したDavid Gross氏が率いるグループが進めます。グループには、Michael Douglas氏・Arthur Jaffe氏・Igor Klebanov氏・Nikita Nekrasov氏が加わっています。
In 1991, Sogge proposed the local smoothing conjecture, which concerns the behavior of waves as they become focused. In particular, the conjecture states that the most extreme focusing must be short-lived. / Our models produced a proof of the local smoothing conjecture in every dimension and therefore also resolve the Kakeya conjecture and Stein’s restriction conjecture in all dimensions. / We obtained our AI output on October 18th, 2026, which was formalized in Lean the following day / As a subproblem, this work also includes a proof of the existence of pure Yang–Mills theory / Our models produced a natural language proof for Yang–Mills existence on September 9th, 2026, and then subsequently produced a proof for QCD on September 18th, 2026. / David Gross will lead a group including Michael Douglas, Arthur Jaffe, Igor Klebanov, and Nikita Nekrasov that will shepherd this work. / For the physics collaboration, the group has decided to hold off on releasing the AI-produced artifacts and instead work on writing it up themselves. — 数学と物理学の成果に関する記述より公式情報を見る →
まとめ:指数時間仮説の反証は検証グループの判断待ち
Leanで形式化されていても、ETHの反証は検証グループが論文の中身を最後まで確認するまで確定しません。Leanがチェックしたのは論文より緩い上限で、形式化した定理が論文と同じ内容かどうかは人が読んで判断するしかないからです。OpenAIとAnthropicが同じ仮説の反証をそれぞれ公開したため、検証グループや研究者は両社の論文を比較しながら確認できます。
3成果のうち、誰でもAIの出力を確認できる分野は数学と計算機科学の2つです。物理学はヤン–ミルズ理論のLeanでの形式化を終えていても、Gross氏らのグループが解説を出すまで、外から中身を検討する手立てはありません。同じ発表の中でも、外部の研究者が中身に触れられる時期は成果ごとに異なります。
FAQ
- 指数時間仮説(ETH)とは何ですか?
- 論理式の条件をすべて同時に満たす真偽の割り当てがあるかを判定する問題(3-SAT)について、変数が増加すると最悪の場合に指数時間がかかるとする計算量理論の予想です。Impagliazzo氏・Paturi氏・Zane氏が唱え、グラフ理論やデータベースなどの数百本の論文で、計算の難しさを論じる根拠として使われてきました。
- OpenAIによるETHの反証は正しいと確定しましたか?
- 確定していません。OpenAIは反証をLeanで検証したとしていますが、Leanでチェックした対象は論文の主定理より緩い計算時間上限で、論文は査読前です。ETHを唱えたImpagliazzo氏・Paturi氏と、MITのWilliams氏を合わせた3人が率いるグループが検証を進めています。
- ETHが反証されると、実際の計算は速くなりますか?
- すぐには速くなりません。この結果は変数が限りなく増加したときに計算時間がどう伸びるかについての話で、実際に論理式を解くときの計算時間については何も述べていません。実際の計算が速くなるまでにはかなりの研究が必要です。



