OpenAIは2026年10月26日、「指数時間仮説は偽である（The Exponential Time Hypothesis is False）」と題する未査読のプレプリントと、定理証明支援系「Lean」による形式証明をGitHubで公開した。同社の社内モデルが生成した成果で、計算量理論の重要な予想である指数時間仮説（Exponential Time Hypothesis、ETH）を反駁したと主張している。検証を率いるのは、ETHの提唱者であるRussell Impagliazzo氏、Ramamohan Paturi氏と、マサチューセッツ工科大学（MIT）のRyan Williams氏だ。ただし、専門家が検証に参加していることと、主張の正しさが確認されたことは区別する必要がある。

組み合わせをすべて試す探索では、問題の規模が大きくなるにつれて計算時間が急増する。ETHは、代表的な論理式の問題について、アルゴリズムをどれほど工夫しても指数時間を避けられないとする予想だ。これを覆せれば、長年にわたり計算の難しさを測る基準となってきた前提が変わる。一方、Leanで形式的な証明が検証されたという説明だけで、人間の研究者が意図するETHの反駁まで確定したと判断することはできない。

AD

指数時間仮説という「計算の壁」は何を主張してきたか

計算量理論で最も有名な未解決問題の一つが「P対NP問題」である。大まかに言えば、多項式時間で解ける判定問題のクラスPと、答えが「はい」であることの証拠を多項式時間で検証できる問題のクラスNPが等しいかを問う。一般には、両者は等しくないという予想、すなわちが支持されている。しかし、多項式時間で解けないと分かっても、それだけでは計算にどれほどの時間が必要なのかまでは決まらない。アルゴリズムの限界を詳しく論じるには、指数関数的な時間が不可避なのかという、さらに踏み込んだ問いが必要になる。

この問題を考えるため、1990年代末から2000年代初頭にかけてImpagliazzo氏、Paturi氏、Francis Zane氏らが提唱したのがETHだ。中心となるのは、代表的なNP完全問題である「3-SAT（3充足可能性問題）」である。3-SATでは、最大3つのリテラル、つまり変数またはその否定を「または」で結んだ節を、さらに「かつ」でつないだ論理式を扱う。その式全体を真にする真偽値の割り当てが存在するかを判定するのが、この問題だ。

変数の数を$n$とすると、真偽値の割り当ては$2^n$通りある。入力長に関する多項式因子を省いて述べれば、ETHは「ある正の定数$\delta > 0$について、3-SATを$O(2^{\delta n})$時間で解く決定性アルゴリズムは存在しない」とする予想だ。これが正しければ、指数部分の増え方が$n$よりも緩やかな$2^{o(n)}$時間、すなわち劣指数時間で解くこともできない。単に全探索の$2^n$より速くすることと、劣指数時間に到達することは異なる。指数部分の係数を小さな正の定数に変えても、計算時間は依然として指数的に増える。

ETHは証明済みの定理ではないが、この四半世紀にわたり、多くの研究がこの仮説を前提に計算時間の下限を示してきた。最大独立集合問題やクリーク問題などのグラフ問題をはじめ、計算幾何学、データベース、計算生物学にも関わる。そこで得られているのは、「ETHが正しければ、この問題を一定の計算量より速く解くことはできない」という条件付きの困難性証明である。ETHは、アルゴリズムをどこまで高速化できるかを考える際の標準的な物差しとして使われてきた。

プレプリントが主張するアルゴリズムと計算量

プレプリントの核心は、各節のリテラル数の上限$k$を固定した論理式「$k$-CNF」に対し、劣指数時間で動作する決定性アルゴリズムを構成したという主張にある。対象は、条件を満たす割り当ての有無を判定する問題だけではない。割り当ての総数を厳密に求める数え上げ問題にも対応し、使用する記憶領域は入力長に対して多項式の範囲に収まるとしている。$k=3$の場合には3-SATと、その数え上げ版である#3-SATが含まれるため、この主張が成立すればETHの反駁につながる。

公開リポジトリの概要にある計算時間を、入力長に関する多項式因子を省いて大まかに表すと、次の形になる。ここで$n$は変数の数である。

分母の対数項が増大するため、この式は$n$が十分大きくなると、どの固定された正の定数に対するよりも小さくなる。したがって、劣指数時間という条件を満たす。一方、この式の増え方は、任意の固定された次数$c$に対する多項式よりも大きく、準多項式時間の範囲にも収まらない。提示された計算時間の上界はなお超多項式的であり、多項式時間や準多項式時間で解けると示したわけではない。

ただし、論文が主張する上界と、Leanで形式化された上界には差がある。公開されている形式化範囲の説明では、多項式因子と定数を除いた指数部分について、Lean側は、10月25日版の論文はとしている。どちらも劣指数時間だが、後者の方が小さい上界を与える。これは単なる表記の揺れではなく、論文に記載された計算量と、形式化された計算量の違いとして捉える必要がある。

また、漸近的な計算量の改善だけでは、現実的な規模の入力で既存のSATソルバーを上回るかは判断できない。実際の処理時間は、計算量の表記では省略される定数係数や低次の項、実装方法にも左右される。OpenAIも、理論的な進歩を実用上の改善につなげるには、さらに多くの研究が必要だとしている。今回の主張と、その確認状況を整理すると次のようになる。

項目 プレプリントの主張 確認状況（2026年10月27日時点） この主張だけでは示されないこと
対象命題 指数時間仮説（ETH）の反駁 OpenAIはLeanで検証済みと説明し、外部の研究者が精査を進める P対NP問題の解決、$P=NP$の証明
アルゴリズム 固定幅のCNF式について、充足割り当てを劣指数時間・多項式領域で厳密に数える 論文とLeanコードが公開されている 実用的なSATソルバーや暗号解読の高速化
計算時間 概略で 論文とLeanでは、より詳細な上界に差がある 準多項式時間や多項式時間への到達
理論的影響 ETHに依存する困難性評価の前提が変わる 主張の正しさと、その帰結を独立に検討する段階 すべてのNP困難問題が容易に解けること

AD

Leanによる検証と、形式化で確認すべきこと

OpenAIの発表によれば、社内モデルが自然言語による反駁の証明を生成したのは2026年10月16日で、同社は翌17日に結果をLeanへ形式化した。Leanは、定義や公理、補題に基づき、形式的な命題が正しく導かれているかを検査するソフトウェアだ。人間の論文で「自明である」「同様に示される」と省略される部分も、検証対象となる証明では形式的に埋める必要がある。ただし、コードがエラーなく処理されたことだけで十分とは限らず、依存する補題に未証明の部分が残っていないか、追加の公理が何を仮定しているかも確認する必要がある。

こうした条件を確認したうえで、Leanが保証するのは、採用された定義と公理のもとで、コードに記述された命題が導かれることだ。その命題が、研究者の意図する数学的主張と一致しているかまでは、検証の通過だけで自動的に保証されない。例えば、用語の定義や条件の順序が意図と異なったり、本来の問題にはない仮定が加わったりしていれば、証明自体が正しくても別の命題を証明している可能性がある。今回であれば、入力の表現、計算モデル、計算時間の数え方などを含め、形式化された内容が本来のETHの反駁に対応するかが確認の対象となる。

この対応関係や論証を精査し、研究コミュニティが理解できる形に整理するのが、Impagliazzo氏、Paturi氏、Williams氏らの役割だ。3氏は公開書簡で、「私たちの関与を、この主張の正しさを保証するものと受け取るべきではない」と明記している。目指しているのは、他の研究者が論証を再構成し、疑問を提示し、その先の研究につなげられる理解である。機械による検証に加え、証明が何を意味し、どのような帰結を持つのかを明らかにする作業が求められている。

公開資料の位置づけについて、OpenAIは完成した学術論文というより「生の研究データ」と説明している。同社は社内モデルによる発見について学術的な功績を求めず、功績や優先関係の判断を研究コミュニティに委ねるとしている。現時点では、GitHubに資料が公開されたことをもって結論が確定したと扱わず、独立した専門家による精査の進展を確認する必要がある。

主張が成立した場合、何が変わるのか

仮に証明が正しく、ETHの反駁が成立しても、それだけでP対NP問題が解決するわけではない。今回の計算量評価は、3-SATを多項式時間で解けることを示していないためだ。RSA暗号や楕円曲線暗号についても、ETHそのものを安全性の前提としているわけではなく、素因数分解や離散対数などの問題に対する具体的な攻撃能力を別途評価する必要がある。今回の劣指数時間という主張だけから、実用的な暗号鍵を解読できるとはいえない。

理論面では、ETHを根拠に計算時間の下限を見積もってきた研究の再検討が必要になる。例えば、「ETHが正しければ$2^{o(n)}$時間では解けない」とされていた問題では、その下限を実際の計算の限界とみなす根拠が失われる。ただし、「ETHが正しければ下限が成立する」という条件付きの定理そのものが誤りになるわけではない。各問題について、本当により速いアルゴリズムが得られるか、どの程度の改善になるかは、個別に検討しなければならない。3氏の書簡も、研究の解釈が変わる可能性を指摘しつつ、これまで蓄積されたアイデアや問題間の還元、技法の価値は残るとしている。

一方、精査によって論証や形式化に不備が見つかり、今回の主張が成立しないと判断される可能性もある。アルゴリズムの正しさだけでなく、計算量の見積もりや、形式化された命題と本来の問題との対応も確認が必要だ。証明の一部が正しくても、結論に必要なすべての段階が確かめられるまでは、ETHを反駁したとは判断できない。また、今回の証明が成立しなかったとしても、それがETHの正しさを証明するわけではない。

AD

未査読の主張と、AI時代の証明の評価

ETHの反駁を主張するプレプリントが公開されたのは、今回が初めてではない。2021年にも、数え上げ版のETHの反駁を掲げた『The #ETH is False, #k-SAT is in Sub-Exponential Time』がarXivに投稿されている。こうした主張が公開リポジトリに掲載されることと、内容の正しさが研究コミュニティによって確認されることは別である。今回の特徴は、AIモデルが生成した論証に加え、機械的に検査できるLeanの形式証明も公開されている点にある。

この事例は、AIが未解決問題に取り組む能力だけでなく、研究の功績をどう評価するかという問題も提起している。AIが証明候補を出力したとして、それを読み解き、誤りを修正し、論証を簡潔にし、数学的な意味を説明する研究者の仕事をどう位置づけるのか。Impagliazzo氏らは公開書簡で、最初に発表した人や強力なツールを持つ人に評価が偏り、検証や解説、その先の研究が十分に評価されなくなることへの懸念を示した。成果への早期アクセスのあり方や、研究手法の変化に直面する学生・研究者への支援も、コミュニティ全体で議論すべき課題としている。

OpenAIは外部の研究者に秘密保持契約（NDA）を求めず、参加は任意かつ無報酬としている。研究者は独立した立場で作業し、途中経過や結論を自由に議論・公表できる。研究グループの要請を受け、独立検証のための生データの公開と、この成果が分野全体に及ぼす影響を議論する会議への資金拠出にも同意した。公開と検証、成果の理解をどう支えるかについても、今回の取り組みは一つの試みとなる。

現時点で公開されているのは、ETHの反駁を主張する論文と、その主張を検討するための形式証明である。今後の焦点は、形式化された定義や計算量の評価が本来のETHに対応しているか、そして論証を独立した研究者が確認し、説明できるかにある。ETHが覆ったと結論づけられるかどうかは、その精査を経て判断される。