指数時間仮説（ETH）の否定は検証されたのか：これまでに確認されたことと、確認に必要なこと

OpenAIとAnthropicがそれぞれ指数時間仮説（ETH）を否定したと主張してから4日が経ちましたが、2社の外では、どちらの主張についても判定を公表した人はいません。Russell Impagliazzo、Ramamohan Paturi、Ryan Williamsが取りまとめを引き受けた精査は、公開の場で始まっています。議論のためのブログ、ノートを共有するフォルダ、意見を募るフォームがあり、2026年末までのオンライン会議も提案されています。有志はLeanの証明を組み立て直し、解説を書き、小さな実験を行いました。この結果の上に立つ最初の後続論文も、すでに出ています。

これまでに確認されたことは、活動の多さから受ける印象よりも限られています。OpenAIの論文に対する公開の検査のうち最も具体的なものは、10月29日に有志のリポジトリにマージされたコミュニティのノートです。論文の構成を変数が最大14個の論理式で実行し、すべての結果を総当たり（ブルートフォース）と比べるものです。著者は、このノートは「定理の正しさには関わらない」と書いています。¹³

10月27日、私たちはOpenAIの掛谷予想・ETH・ヤン–ミルズの主張で、2つの主張を並べて比べました。この記事では、その後に起きたことを扱います。精査チームがOpenAIに何を求めたのか、公開の精査は実際にどう進んでいるのか、何が確認され、何が確認されていないのか、最初の後続論文、そして何があれば確認されたと言えるのかです。出典はすべて2026年10月30日に確認しました。

精査チームはOpenAIに何を求めたのか#

2つです。生データと、会議です。Williamsは10月26日（UTC）の夜、XとBlueskyで、4つの投稿からなるスレッドで精査を発表しました。2つ目の投稿¹にはこうあります。「私たちは秘密保持契約（NDA）に署名しておらず、報酬も受け取らないので、進行中の知見を自由にコミュニティと共有できる。全過程を通じてそうするつもりだ。私たちはOpenAIに、PDFとLeanのソースを含め、ETHに関するすべての生データをできるだけ早く公開するよう求めた」。3つ目¹はこうです。「また、この研究の影響を受けるコミュニティ全体のために、会議の開催を支援すると約束するようOpenAIに求めた。OpenAIは両方に同意した」。

OpenAIの発表⁴も、自らの言葉で同じことを述べています。「コミュニティによる独立した検証を助けるために結果のすべての生データを公開すること、そしてこの研究が分野全体に与える影響を理解するための会議に資金を出すとOpenAIが約束することという、グループの要請に同意した」。記者名のある報道も、同じように伝えました。Ana Maria Constantinは10月26日、The Next Web⁵にこう書いています。「グループはOpenAIに、ETHの結果に関するすべての生データを公開し、研究コミュニティのための会議に資金を出すよう求めた。WilliamsとOpenAIによれば、OpenAIは両方に同意した」。Scientific American⁶は10月27日、会議について「Williamsによれば」として報じました。

精査チームに特別なアクセス権が与えられたわけではありません。モデルにさらに質問できるのかとBlueskyで尋ねられたWilliamsは、こう答えています²。「私たちは彼らの社内モデルにアクセスできない。受け取ったのはPDFだけで、それはここに投稿した」。

現在公開されているものは次のとおりです。

• GitHub：openai/math⁷のETHのフォルダには、論文、そのTeXソース、引用情報のファイルがあり、Leanの形式化はリポジトリのLeanライブラリに置かれています。10月26日以降のリポジトリの更新は10月29日付の1回だけで、別の結果（虚数乗法を持つアーベル多様体についてのホッジ予想）に関するものです。OpenAIはほかの10件の結果について短縮した推論の要約を公開していますが、ETHはその中に入っていません。
• 主催者のフォルダ：精査チームの共有フォルダ（後述）にはOpenAIのサブフォルダがあり、公開された論文と、OpenAIの2本目の原稿が入っています。17ページで、題は「Exactly Counting 3-SAT Solutions in Subexponential Time」（3-SATの解を準指数時間で正確に数える）、10月17日付です。¹¹この原稿は、log n のべきが小さい、より弱い指数を主張しており、公開された論文を自らの「姉妹原稿（companion manuscript）」と呼んでいます。OpenAIのGitHubリポジトリにあるプレプリントの中には入っていません。

私たちが読んだ出典は、「すべての生データ」に何が含まれるのかを明記していません。

公開の精査は実際にどう進んでいるのか#

小さな研究コミュニティが、主に共有ファイルを通じて自らを組織しているように見えます。ethdiscussion.blogに載った主催者の最初の投稿⁹は3人全員の署名入りで、彼らの書簡を繰り返しています。「私たちの関与を、主張へのお墨付きと受け取らないでほしい」。投稿は、なすべき仕事をこう定めています。「当面の課題は、議論を精査し、その正しさを確立するか限界を特定し、その帰結を理解することだ」。そして、研究者が「疑問、欠落、訂正、検証済みのステップを共有しながら、独立に貢献する」方法についての案を求めています。

投稿は4つの仕組みを挙げています。

• 公開元のURL：「元のPDF、付随するソースや形式化、その後の訂正の正式な置き場所」です。⁹
• ETH_Repository：3人の主催者が管理する閲覧専用のGoogleドライブのフォルダで、「研究者のノート、説明、コメント、訂正、後続の結果を広めやすくする」ためのものです。ReadMeによれば、投稿したい人はPaturiにメールを送り、自分の名前のフォルダを受け取ります。¹¹
• Googleフォーム：意見と、「2026年末までに提案されているオンライン会議の是非、形式、時期」について尋ねています。
• ブログ自体：お知らせと公開のコメントのためのものです。ReadMeは、Holger Dellが立ち上げたZulipのチャットも案内しています。

10月29日、ブログはFrancis Zaneによる2本目の投稿「Links To Other Work」¹⁰（ほかの研究へのリンク）を載せ、Mark Sellke、Ryan O'Donnell、Shiva Kintaliの解説とLance Fortnowのブログを紹介しました。10月30日の時点で、共有フォルダには次のものがありました。

種類	フォルダの中身
主張	OpenAI：公開された論文と17ページの原稿。Anthropic：その論文
主催者	ImpagliazzoとPaturiによる5ページのノート（10月28日付）。ETHの弱い形について
解説	Ryan O'Donnell：10月26日から29日までの解説の草稿13版（番号付き）、ほかのノート、講義へのリンク。Mark Sellke：スライド。Shiva Kintali：簡略化した証明。Eitan Porat：スライドと動画。Jesper Nederlof：Anthropicの論文についての「Claude ETH refutation working note」（「work in progress」〔作業中〕と記載）。Amit Sahaiのフォルダ：「An Elementary Route to Subexponential 3-SAT」
さらなる研究	Isaac Rudich：計数アルゴリズムの上に立つ素因数分解の論文。Tony Newton：OpenAIの構成の中の構造についてのノート。「ETHの独立した否定」は主張しないとしている

主催者自身のノートは、仮説の弱い形である弱ETH（Weak ETH）が3-SATについて成り立つのは、k-SATについて成り立つときであり、かつそのときに限ることを証明しています。どちらの主張も評価してはいません。10月30日の時点で、ブログにも、共有フォルダにも、WilliamsのXとBlueskyの投稿にも、主張そのものについての精査チームの知見は見つかりませんでした。

PR #60のコミュニティノートは何を確認したのか#

確認しているのはアルゴリズムの簡易モデル（トイモデル）で、定理ではありません。ノートはoai-math-revised¹²にあります。OpenAIの原稿についての訂正、参考文献、読書会を集める有志のリポジトリです。READMEによれば、この取り組みは「完全に独立しており、OpenAIの認可も支援も受けていない」。Chelsea A. McElveenが10月28日にプルリクエスト#60¹³を作成し、Soledad Villarが10月29日にマージしました。ETHの論文のフォルダに3つのファイルを加えるもので、NOTES.md¹³、Pythonのスクリプト、そのスクリプトの短いREADMEです。

スクリプトは、PRの言葉では「2.3節から2.7節の実行可能なモデルで、n ≤ 14 で総当たりと照合したもの」です。¹³小さな論理式について、論文の多項式、「測定設計（measurement designs）」、補間の段階を組み立て、厳密な算術を使い、各段階を 2^n 通りのすべての割り当ての数え上げと比べます。ノートが「何も圧縮しない」とする単純な「直接」設計では、再構成された数は、変数が10、12、14個の論理式で総当たりと一致します。充足割り当ての数は、それぞれ259、736、3,108です。論文自身の2.7節の構成を最小のパラメータ（r = 2, Q = 2, R = 2）で使うと、変数6個の論理式で処理全体が最後まで動いて正しい数34が得られ、変数12個の論理式で鍵となる恒等式が確かめられます。

ノートは2.7節について、構造に関する2つの指摘を加えています。1つは、論理式が大きくなるにつれて変数がどのようにグループにまとまるかの記述です。もう1つは、それが「指数を変えない」ことを確かめたもので、ノートはこの現象を「アルゴリズム上ではなく、構造上のもの」と呼んでいます。説明を分かりやすくするための提案も2つあります。PRは自らの限界を明記しています。「TeXのソースも原稿の主張も変更しない。原稿に誤りがあるとは主張していない」。ノート自体にはこうあります。「このノートは定理の正しさには関わらない。定理の形式的な検証は、Leanの形式化が担っている」。

簡易モデルで決着がつかない理由：ETHは、変数の数が無限大に向かうとき、実行時間がどう増えるかについての命題です。変数が14個なら、総当たりで確かめる割り当ては16,384通りです。小さな実行で示せるのは、各段階が正しい数を計算することです。その方法が 2^o(n) 時間で動くことは示せません。Anthropicの論文は自らの手法について、「n > 10^7 でない限り、一般的な改善をもたらす見込みは低そうだ」とし、「総当たりの列挙は n = 100 ですでに現実的でない」と付け加えています。¹⁶ノートはスクリプトを、ありのままに、「Leanの形式化を補う」理解の助けとして示しています。

どう作られたか：PRにはこう書かれています。「Chelsea A. McElveenによる投稿。実装と草稿の作成はClaude（Anthropic）が支援した」。ノートは「内容の責任は著者にある」と付け加えており、2つのコミットのどちらにも「Claude Opus 5.5」を共著者（co-author）とする行が付いています。

Leanの証明を確かめ直した人はいるのか#

ビルドについては、確かめ直されています。命題が何を意味するかは別の問題です。独立した再確認が2つ公開されています。

• Carlos Toledoの監査：10月28日に主催者のブログへのコメント⁹で告知されたToledoの報告¹⁵は、両社のLeanの形式化を、Comparator、Lean自身のカーネル、そして「Leanのものとは独立に書かれたカーネル」であるnanodaで再実行しています。「どちらも両方の証明を受理し、使っているのは propext、Classical.choice、Quot.sound だけ」で、これは3つの標準的な公理です。OpenAIのLeanにはETHの定義がないので、ToledoはLeanで教科書どおりのETHを書き、各社の命題が、その社自身の計算モデルでそのETHを否定することのLeanによる証明を報告しています。未解決のまま残る点は、彼の言葉では次のとおりです。「どのカーネルにも確かめられないことが2つある。各社のマシンと入力の符号化が教科書のものと一致すること…、そして私たちのLeanのETHが教科書のETHであることだ。後者は読解であり、これからもずっとそうである」。彼の結論は「これはETHが偽であることを保証するものではない」です。Toledoは、自分のツールが「AnthropicのモデルであるClaudeを使って書かれており、2つの主張の1つはAnthropicのものだ」と開示しており、どちらの社とも所属関係はないとしています。
• プルリクエスト#62：10月29日に作成され、まだオープンのままのこのPRは、OpenAIのLeanの形式化を独立に再ビルドした結果を報告しています。3,977のモジュールすべて、公理の確認、そして課題（challenge）と解答（solution）の命題の比較です。¹⁴PRは「これはComparatorによる実行ではない」とはっきり書いています。10月30日、リポジトリの側から返信したJohannes Schmittは、再ビルドを歓迎し、「このリポジトリには、ファミリー378についてのComparatorの実行はまだない」と指摘しました。そして、命題が何を意味するかについてのPRの読解は除くよう求めました。「読み手が2人とも言語モデルだったので、論文のノートには入れるべきではない」。

この返信は、今回の精査が何度も立ち返る線を引いています。証明が形式的な命題に合っているかは、機械が確かめられます。その形式的な命題がETHと同じことを言っているかは読解の問題で、あのリポジトリでは、言語モデルだけによる読解は数に入りません。

論文とそのLeanの証明の間にも隔たりがあります。OpenAIのLeanの範囲に関する注記（scope note）⁸によれば、形式的な証明が与える時間の上界の指数は n(log log n)²/√log n です。論文のより鋭い指数 n·log log n/√log n は、自然言語による証明だけに支えられています。

最初の後続論文は何か#

2日のうちに、数理科学のプレプリントのリポジトリであるHexagonに、主張の上に立つ投稿がいくつも登録されました。どれにも、文章のどれだけがAIで生成されたか、人間がどれだけを理解しているかを示すHexagonのラベルが付いています。

投稿	投稿者、日付	何をするとしているか	Hexagonのラベル
2610.00574v118	Scott Kominers、10月27日	「主結果の定性的な形についての予備的な解説」	人間とAIの文章の混合。人間の理解：一部
2610.00594v119	Deep Bhattacharjee、10月28日	OpenAIの計数アルゴリズムを再現し、数え上げから重み付き和に広げる	人間とAIの文章の混合。一部
2610.00600v120	Isaac Rudich、Louis-Martin Rousseau、10月28日	時間 N^o(1) での決定的な素因数分解を主張。Leanの証明つき	人間とAIの文章の混合。一部
2610.00613v117	Xiaoyu Li、10月28日	否定が学習理論に何をもたらすかを問う	主にAIが生成した文章。一部

申告は率直です。Kominersは自分の草稿を「きわめて予備的で、大いにLLMで数学したもの（heavily LLMathed）」と呼び、こう書いています。「各部分は個別に読んで理解したが、議論全体を完全に『腑に落とす』にはまだほど遠い」。¹⁸RudichとRousseauは、アイデアとLeanの証明はClaude Opus 5.5が生成したと書いています。2人は形式的な命題を指定して監査しましたが、「証明は読んでいない。証明はLeanが確認している」。²⁰

学習理論の論文：Hexagon 2610.00613v1「What Does the Refutation of the Exponential Time Hypothesis Mean for Learning Theory?」¹⁷（指数時間仮説の否定は学習理論にとって何を意味するのか）は、10月28日にXiaoyu Liが登録しました（ページの見出しでは、第1版は10月29日となっています）。ページには「Primarily AI-generated text」（主にAIが生成した文章）と「Human understanding: some parts」（人間の理解：一部）のラベルが付いています。来歴に関する記述（provenance statement）はこう始まります。「この研究は2026年10月28〜29日に、Claude Codeの中でエージェントとして動くClaude Opus 5.5（Anthropic）とともに作られた」。続けてこうあります。「投稿者は、指数時間仮説の否定が学習理論にとって何を意味するかという問いを立て、提示の仕方を指示し、題を選んだ。Claudeは結果を選び、それらを証明し、文章を書き、図を描いた」。別のClaudeのエージェントが引用を確認し、「証明を監査し、査読者として論文を査読した」。PDF自体のAI利用の開示は「この論文は、Claude Codeの中でエージェントとして動くClaude Opus 5.5（Anthropic）とともに書かれた」で始まり、「内容の責任は著者にある」で終わります。

論文の要旨は「OpenAIとAnthropicによる最近の2つの研究が、指数時間仮説（ETH）を否定した」で始まります。¹⁷続いて、新しいアルゴリズムが学習を速めるのはどんなときかについての「局所性原理」と、「AlmanとVassilevska Williamsの疎Max-SAT仮説は偽である」ことを主張しています。来歴に関する記述は、2つの否定をどう使っているかを説明しています。「ブラックボックスとして、Imported Theorems（取り込んだ定理）として引用する」。つまり、この論文の結果は、取り込んだ主張とともに成り立ちもし、崩れもします。ラベルと来歴に関する記述は、誰が何をしたかを伝えます。取り込んだ主張が成り立つかどうかは伝えられません。それが精査の問いです。

その後、名前の分かる研究者は何を言っているのか#

意見は出ていますが、その限界も明記されています。Lance Fortnowは10月28日、自身のブログにこう書きました²¹。「自分で証明を検証してはいないが、指数時間仮説はもう終わりだと考えて差し支えないだろう」。

Fortnowがまず読むよう勧める解説を書いたRyan O'Donnellは、「免責事項：正しいかどうかは分からない」という一文を添えてそれを投稿しました²²。解説の脚注には、「odonnell@cs.cmu.eduがLLMとのやり取りを通じて作成した」とあります。主張への最初の反応を尋ねられたWilliamsは、10月27日にこう答えています³。「『確かなのか』と聞いた。Leanで検証したという返事だった。私は『分かった、でも確かなのか』と言った」。

何があれば確認されたと言えるのか#

1つの確認では足りません。「ETHの否定は検証されたのか」という問いは別々の問いに分かれ、それぞれに違う人が違う証拠で答えます。

問い	誰が、または何が答えられるか	10月30日の状況
Leanの証明は、それ自身の命題に対して通るか	Leanのカーネル、Comparator、独立したカーネル	OpenAIの公開資料はそうだとしている。Toledoが両社の証明を再実行した。15OpenAIの証明を再ビルドしたPR #62はオープンのまま14
Leanの命題は、ETHが偽だと言っているか	計算モデル、入力の符号化、定義を読む人	Toledoは、各命題がその社自身のモデルで教科書どおりのETHを否定することのLeanによる証明を報告。モデル間をつなぐ一歩は「非形式的なまま」としている。15精査チームの読解は投稿されていない
論文のより鋭い上界は成り立つか	自然言語による証明を読む専門家	OpenAIの範囲に関する注記によれば形式化されていない。8公表された読解はない
人々は証明を理解しているか	解説、講義、セミナー	草稿、スライド、動画、録画された講義。正しさを保証すると主張するものはない
主催者は何を見いだすか	Impagliazzo、Paturi、Williamsとコミュニティ	私たちが見つけた限り、投稿はない。2026年末までのオンライン会議が提案されている9

同じ問いは、Anthropicの主張にも別個に当てはまります。それ自身のLeanの形式化を持つ、別の論文だからです。

主催者の書簡は、これほど重要な結果には「慎重で独立した精査と、他の人が再構成し、疑問を投げかけ、その上に積み上げられる理解」が必要だとしています。その物差しで測れば、作業はまだ初期の段階です。有志が示したのは、構成の簡易版が小さな論理式で正しい数を計算すること、そして形式的な証明がビルドできることです。人が必要な部分、つまり命題とより鋭い上界を読む作業こそ、公開された結果がまだ欠けているところです。

Papexで何が変わったのか#

ETHのページ（英語）には、OpenAIとAnthropicの両方の主張が、出典の記述どおりに載っています。状態は「Claimed」（主張あり）です。Papexが示すのは出典が示す状態で、Papex自身の判定ではありません。この記事に合わせて、私たちはPR #60のコミュニティノートを、OpenAIの主張への応答としてこのページに加えました。両方の主張は、未解決問題についてのAI支援の主張を集めた私たちの一覧/ai-claims（英語）にも載っています。

出典#

1. Ryan Williamsによる精査の発表のスレッド（Bluesky、2026年10月26日）、投稿2/4と3/4を含む。同じ文面はXにもある。2026年10月30日確認 ↩ a b
2. モデルへのアクセスについてのRyan Williamsの返信（Bluesky、2026年10月26日）、2026年10月30日確認 ↩
3. Ryan Williamsの返信「OK but are you sure?」（X、2026年10月27日）、2026年10月30日に公開の閲覧専用ミラーで確認（Xにはログインしていない） ↩
4. Working with academic communities to build scientific understanding（OpenAI、2026年10月26日）、2026年10月30日確認（2026年10月26日のインターネットアーカイブの保存版。公式ページは自動アクセスを遮断） ↩
5. OpenAI says its AI model has disproved the Exponential Time Hypothesis（Ana Maria Constantin、The Next Web、2026年10月26日）、2026年10月30日確認 ↩
6. Dueling proofs from OpenAI and Anthropic astound scientists（Joseph Howlett、Peter Hall、Scientific American、2026年10月27日）、2026年10月30日確認 ↩
7. openai/math、ETHのフォルダ、コミット履歴と推論の要約（GitHub）、2026年10月30日確認 ↩
8. Lean scope note 378, ETH（openai/math、GitHub）、2026年10月30日確認 ↩ a b
9. ETH Refutation: Examination and Discussion（Impagliazzo、Paturi、Williams、ethdiscussion.blog、2026年10月26日）、コメントを含む、2026年10月30日確認 ↩ a b c d
10. Links To Other Work（Francis Zane、ethdiscussion.blog、2026年10月29日）、2026年10月30日確認 ↩
11. ETH_Repository、主催者の共有フォルダとそのReadMe、サブフォルダ（Googleドライブ）、2026年10月30日確認 ↩ a b
12. oai-math-revised、README（GitHub）、2026年10月30日確認 ↩
13. Family 378: executable toy model, structural notes, expository suggestions（Chelsea A. McElveen、oai-math-revised PR #60、2026年10月28〜29日）とNOTES.md、2026年10月30日確認 ↩ a b c d
14. NOTES (ETH is False): independent build and statement check of family 378（oai-math-revised PR #62、2026年10月29日作成）、10月30日の返信を含む、2026年10月30日確認 ↩ a b
15. Two claimed refutations of the Exponential Time Hypothesis: what was decided, and what was only read（Carlos Toledo）、2026年10月30日確認 ↩ a b c
16. A 2^o(n) Time Algorithm for 3-SAT（Claude, Anthropic。anthropics/formal-math、コミット16a5ce41）、2026年10月30日確認 ↩
17. What Does the Refutation of the Exponential Time Hypothesis Mean for Learning Theory?, hexagon:2610.00613v1（投稿者Xiaoyu Li、Hexagon、2026年10月28日）、ページとPDF、2026年10月30日確認 ↩ a b c
18. On counting satisfying assignments via polynomial separation, hexagon:2610.00574v1（投稿者Scott Kominers、Hexagon、2026年10月27日）、2026年10月30日確認 ↩ a b
19. Subexponential Weighted Counting and Exact Optimisation, hexagon:2610.00594v1（投稿者Deep Bhattacharjee、Hexagon、2026年10月28日）、2026年10月30日確認 ↩
20. Deterministic Factoring in Time N^o(1), hexagon:2610.00600v1（投稿者Isaac Rudich、Louis-Martin Rousseau、Hexagon、2026年10月28日）、2026年10月30日確認 ↩ a b
21. The Exponential Time Refutation（Lance Fortnow、Computational Complexity blog、2026年10月28日）、2026年10月30日確認 ↩
22. 解説を共有するRyan O'Donnellの投稿（X、2026年10月27日）とSome exposition of "The Exponential Time Hypothesis Is False"、2026年10月30日確認 ↩