OpenAIとAnthropicが、AIの見つけた「指数時間仮説は誤り」の証明を公開｜何が示され、研究者がどう確かめるのか

2026年11月7日

OpenAIとAnthropicが、AIの見つけた「指数時間仮説は誤り」の証明を相次いで公開した

OpenAIは2026年10月26日（米国時間）、社内のAIモデルが計算機科学の有名な予想「指数時間仮説（ETH）」が誤りであることを証明したと公式ブログで発表しました。証明の論文と、証明をコンピューターで点検するためのLeanのファイルもGitHubで公開しています。

その約6時間後には、Anthropicも社内の研究用Claudeモデルが見つけた別の証明を、論文とLeanのファイルとともにGitHubで公開しました。どちらの会社も、社内のAIモデルが証明を見つけ、Leanでの形式化まで済ませたと説明しています。

指数時間仮説は、30年近く多くの研究の前提として使われてきた予想です。この記事では、この予想が何を言っているのか、両社の証明が何を示したと主張しているのかを整理します。そのうえで、公開されたLeanの定理文と、Anthropicが公開している自動検査の記録を読み、機械が確かめた範囲と、研究者がこれから確かめる範囲を分けて紹介します。

発表の要点

両社はLeanでの点検を済ませたと説明し、正しさと意味の確認は研究者がこれから進める

発表

2社が別々の証明を公開

OpenAIが10月26日（米国時間）に発表し、Anthropicも約6時間後に、論文とLeanのファイルをGitHubに置いた。

主張

変数1個あたりに増える時間の倍率が、1へ近づいていく解き方

変数が増えたときの計算時間の伸び方が、指数時間仮説の想定より小さくなるとする。

機械による点検

AnthropicのLeanは公開の自動検査に合格

2種類の検査プログラムが証明を受け入れた記録を、GitHubで誰でも読める。

人による確認

提唱者を含む3人がOpenAIの証明の検証を主導

3人は、自分たちの関与を「主張の認定」と受け取らないよう呼びかけている。

出典: OpenAI公式ブログ（2026年10月26日）、openai/math、anthropics/formal-math、Impagliazzo・Paturi・Williams各氏の書簡。自動検査の欄は、2026年10月28日に筆者が公開ログを読んで確認した内容

指数時間仮説は、3-SATを解く時間が変数とともに指数的に増えるという予想

指数時間仮説の対象は「3-SAT（スリーサット）」という問題です。オンかオフにできるスイッチがn個あり、「スイッチ1がオン、またはスイッチ5がオフ、またはスイッチ7がオン」のような、3つまでの項目を「または」でつないだ条件がたくさん与えられます。すべての条件を同時に満たすスイッチの組み合わせがあるかどうかを答えるのが3-SATです。

組み合わせを全部試す総当たりでは、スイッチが1個増えるたびに調べる組み合わせが2倍になり、n個なら2のn乗通りになります。スイッチ100個で約10の30乗通りです。これまでに総当たりより速い方法はいくつも見つかっていますが、どれも「スイッチが1個増えるたびに、計算時間が一定の倍率で増える」形にとどまっていました。

指数時間仮説は、Russell Impagliazzo氏とRamamohan Paturi氏が提唱した予想で、この形は避けられないとします。どれだけ工夫しても、スイッチが1個増えるごとに時間が一定の倍率以上で増えると考えます。正しいと広く信じられてきたため、グラフ理論、計算生物学、データベースなどの数百の論文が「この予想が正しければ、この問題はこれ以上速く解けない」という結論を導く前提として使ってきたと、OpenAIは説明しています。

総当たり

1個増えるごとに2倍

2のn乗通りを全部試す。

指数時間仮説の想定

1個増えるごとに一定の倍率以上

倍率は2より小さくできても、1より大きい一定の値を下回らない。

両社の主張

増える倍率がしだいに1へ近づく

スイッチが多いほど、1個あたりに増える時間の割合が小さくなる方法がある。

数式では、指数時間仮説は「ある正の数δについて、3-SATを2の(δ×n)乗より短い時間で解く方法はない」と書ける。両社は、どんな正の数δでも2の(δ×n)乗より短い時間で解ける、という形でこれを否定したと主張している

両社は、組み合わせの数を数える新しい方法で3-SATを解けると主張している

両社の証明はどちらも、条件を満たす組み合わせがあるかどうかだけでなく、条件を満たす組み合わせが何通りあるかを正確に数える方法を示したとしています。数えられれば「1通り以上あるか」も分かるので、3-SATも同じ時間で解けます。乱数を使わない決まった手順（決定的アルゴリズム）である点も共通です。

ここで出てくる log n は、nを2進法で書いたときの桁数にあたる量で、nが増えてもごくゆっくりしか増えません。log log n は、その桁数の桁数にあたり、さらにゆっくり増えます。計算時間の上限は、OpenAIが2の「n÷√log n」程度の乗、Anthropicが2の「n×log log n÷√log n」に比例する数の乗です。どちらも指数の部分がnよりゆっくり増えるので、変数が1個増えるごとに増える時間の倍率が、nが大きくなるほど1に近づきます。この性質が、指数時間仮説の否定にあたります。

暗号の多くは、ある種の計算問題を速く解けないことを安全性の土台にしているため、計算の速さに関する予想が崩れると、暗号への影響が気になります。米国のテック系ニュースサイトTechCrunchによると、Williams氏が暗号への影響を尋ねたところ、OpenAIのチームは確認済みで、影響はないとかなり確信していると答えたそうです。OpenAI自身も、より速いアルゴリズムを見つけて実用上の改善につなげるには、さらに多くの研究が必要だとブログに書いています。

速さの差が大きくなるのは、変数がけた外れに多い場合

指数時間仮説を否定するには、変数の数nを限りなく大きくしたときの伸び方だけが問題になります。そのため、両社の上限が実際の計算をどのくらい速くするかは、上限の式に含まれる定数の大きさしだいです。Anthropicの説明文も、この結果は変数が限りなく増えたときの振る舞いについてのもので、実際の問題を解く速さについては何も述べていない、と明記しています。

上限の式で、指数を総当たりより小さくしているのは「√log n で割る」部分です。この割る数は、変数が2の100乗個あってもようやく10、2の1万乗個でも100にしかなりません。しかもAnthropicの上限の式には、この効果を弱める log log n の掛け算や、条件1つあたりの項目数の2乗（3-SATでは9）を掛ける係数が入り、両社の式には値が示されていない定数も入っています。そのため、上限の式から「すでに知られている速い方法より有利」「総当たりとの差がはっきり開く」と言えるのは、変数がけた外れに多い場合だけです。

実際の業務でSATを解くソフト（SATソルバー）は、問題の構造を利用する工夫で、数百万個の変数を含む問題を解くこともあります。今回の証明が関わるのは、最悪の場合にどこまで速く解けるかという理論上の見通しです。

Leanの定理文と公開された検査記録で、機械が確かめた範囲が分かる

Leanは、数学の証明を一歩ずつ書き下し、各ステップが論理的に正しいかをコンピューターに機械的に点検させるためのソフトです。Leanが受け入れた証明には、人が読み落とす計算ミスや論理の飛躍が残りにくくなります。

ただし、Leanが保証するのは「Leanで書かれた定理文が証明された」ことまでです。その定理文が、論文や指数時間仮説が言いたいことを正しく表しているかは、人が読んで確かめます。Anthropicは、主張をまとめたMainResults.leanを、Mathlib（Leanの標準的な数学ライブラリ）だけを読み込む短いファイルにし、人が読んで確かめやすくしたと説明しています。論文との違いも付録に列挙しています。

筆者が2026年10月28日にこのファイルを読んだところ、指数時間仮説は「3-SATを2の(δ×n)乗に定数を掛けた時間以内で解くチューリングマシン（計算の手順を表す理論上の機械）について、δをどこまで小さくできるかの限界が0より大きい」という形で定義され、その否定が「ETHIsFalse」として書かれていました。数え上げの主定理には、変数が4個以上、条件が2個以上、どの変数も条件に現れる、同じ条件を2回書かない、という前提が付いています。

Anthropicのリポジトリでは、変更を加えるたびにGitHub Actions（GitHub上で自動検査を走らせる仕組み）が証明を組み立て直し、Comparatorという道具で検査します。Comparatorは、証明された定理が定理文と同じ形をしているか、Leanで標準的に使われる3つの公理以外に頼っていないかを確かめ、さらに独立に作られた別の検査プログラム（nanoda）でも証明を点検します。

同じ実行の記録（ログ）の終盤には、次の行が残っています（時刻を除いた抜粋）。sorryは「この部分の証明を省略する」というLeanの書き方で、定理文だけを置いたファイル（Challenge.lean）の2か所に出ています。証明の本体を読み込んだあとの検査では、2つの検査プログラムがどちらも証明を受け入れました。

warning: Challenge.lean:12:8: declaration uses `sorry`
warning: Challenge.lean:16:8: declaration uses `sorry`
Building Solution
Build completed successfully (9516 jobs).
Running nanoda kernel on solution
nanoda kernel accepts the solution
Running Lean default kernel on solution.
Lean default kernel accepts the solution
Your solution is okay!
All 1 comparator configuration(s) accepted.

OpenAIも、検証用の定理文（SubexponentialSAT.lean）と、許可する公理を標準の3つに限った検査設定を公開しています。OpenAIのリポジトリには、Leanの検査を自動で走らせる仕組みが置かれていないため、検査は各自が手元で走らせる形です。筆者が10月28日に、証明本体にあたるLeanのファイル3977個（約71万行）を取得して検索したところ、証明を省略するsorryも、独自の公理を追加する宣言も、1件も見つかりませんでした。

研究者の検証グループは、正しさと影響をこれから確かめる

機械の点検が済んでも、研究者が証明を理解し、定理文が本当に指数時間仮説を否定しているかを確かめるまで、計算機科学の分野で結論として扱われるには時間がかかります。OpenAIの発表によると、OpenAIの証明の検証と研究は、指数時間仮説を提唱したImpagliazzo氏とPaturi氏（ともにカリフォルニア大学サンディエゴ校）と、MITのRyan Williams氏の3人が率いる独立したグループが担います。

3人は計算機科学の研究者に向けた公開書簡で、「私たちの関与を、主張の認定と受け取らないでほしい」と書いています。そのうえで、証明の正しさを確かめるか限界を見つけること、分かりやすい解説や簡単な証明を作ること、影響を受ける研究を整理することを、研究者のコミュニティ全体で進めようと呼びかけています。

OpenAIは検証グループの求めに応じて、この成果の生データをすべて公開することと、分野への影響を話し合う会議の費用を出すことに合意しました。グループの参加者は秘密保持契約を結ばず、報酬も受け取りません。OpenAIは、AIが生んだ発見について学術的な功績を主張しないとも述べています。

10月6日の公開から翌日に3本が取り下げられたように、AIの書いた証明は公開後に誤りが見つかることもあります。今回、Anthropicの証明は公開の自動検査に合格していて、OpenAIもLeanでの形式化を済ませたと説明しています。それでも、定理文が意図どおりの内容か、OpenAIの論文が示す、Leanで確かめた上限より厳しい上限まで正しいか、証明の考え方を人が理解できるかは、研究者がこれから確かめる段階です。

続報は、両社のリポジトリと検証グループの書簡で追える

今回の発表は、研究者による検証の入り口にあたります。続きを追うなら、次の3か所を見ると、訂正や検証の進み具合を一次情報で確かめられます。

今回の発表で目を引いたのは、証明そのものより、2社がLeanのファイルまで添えて公開し、予想を提唱した本人たちが検証の取りまとめを引き受けた進め方でした。AIが書いた証明を、機械の点検と人の理解の両方でどう確かめていくのか、検証グループの会合の告知を待ちながら追いかけたいと思います。