Claudeも指数時間仮説を否定する論文を出した。OpenAIと同じ日、同じ結論という出来過ぎた一致

まず初めに

AIが数学の難問を解いた、というニュースはもう珍しくない。だが今回は、ライバル同士が同じ日に、同じ予想を、ほぼ同じ結論で否定しに来た。偶然と言うには出来過ぎていて、出来レースと言うには両社の面子が邪魔をする。数学の世界では、道具がそろった瞬間に複数の人間が同じ山に同時に登り切ることは昔から起きてきた。登山者が人間ではなくモデルになっただけ、と見るのが一番しっくりくる。問題は、頂上に旗が立ったかどうかを、まだ誰も確認していないことだ。

※個人の感想です

何が起きたのか

Anthropicは、自社の形式数学リポジトリ「formal-math」に「eth」というフォルダを追加し、論文PDFとLean 4の形式化コードを公開しました。論文の日付は2026年10月26日、著者は「Claude（Anthropic）」です。

指数時間仮説（ETH）は、ImpagliazzoとPaturiらが提唱した計算量理論の予想で、論理式の充足可能性を判定する問題「3-SAT」は、変数の数に対して指数時間より本質的に速くは解けない、とするものです。グラフ理論、計算生物学、データベース、計算幾何学など多くの分野の論文が、この予想を前提に「速くは解けない」という条件付きの結果を積み上げてきました。Claudeの文献調査では、ETHまたはETHを含意する仮説の下でしか証明されていない結果を持つ論文が800本を超えた、と論文は述べています。

論文の主張

論文の主張は、決定性アルゴリズムによって、n個の変数を持つ3-SATを2の o(n) 乗時間——つまり指数よりも遅い伸び方の時間——で解ける、というものです。さらに、より難しい数え上げ版の「#3-SAT」（満たす割り当てが何通りあるかを数える問題）まで同じ枠組みで解けるとしています。

手法の核は、式をテンソルネットワークとして扱い、格子状に並べた節点の縮約を安い方向へ寄せていく発想だと、リポジトリの要約は説明しています。ただし論文自身が強調するとおり、この結果は漸近的なもので、式の規模が天文学的に大きくならないと、従来の総当たりより速くなる場面は現れません。現実のSATソルバーが速くなる話では決してない、という留保が冒頭から付いています。

また、この結果はP対NP問題そのものには直接触れません。論文もその点を明記しています。「3-SATが多項式時間で解ける」わけではなく、「指数時間が必要だという強い予想は外れた」という主張です。

来歴と形式化

論文の「Provenance（来歴）」の節によると、中核のアルゴリズムは2026年10月16日に内部の研究用Claudeモデルが発見しました。使用した出力トークンは1400万、人間の入力はなかったとされています。その後、Anthropicの研究者がClaudeと協力して記述を整え、今回の論文になりました。

証明の検証可能性については、Lean 4による形式化が同時に公開されています。主要な定理を述べた「MainResults.lean」はMathlibだけに依存する短いファイルで、リポジトリのCIは、独立に書かれた第二のカーネルで証明を再検証する仕組み（Comparator）まで含んでいます。一方で、リポジトリのREADMEは限界も率直に書いています。「Leanは証明を検査するが、このファイルが論文の主張どおりの内容を述べているかは、機械は検査しない」。形式化の正しさと、形式化された文が人間の意図した定理と一致するかは、別の問題だということです。

OpenAIの発表との関係

OpenAIは2026年10月26日（日本時間では27日未明）に、自社の内部モデルがETHを反証したことなど3つの科学的成果を発表しています。OpenAI側の説明では、自然言語の反証は10月16日、Lean形式化は10月17日に得られたとされています。Claudeの論文も、脚注で「OpenAIの内部モデルが同様の結果を主張している」ことに触れ、独立かつ同時並行の成果だと位置付けています。

つまり、2社のモデルが同じ10月16日に、同じ予想の反証に到達した、というのが両社の主張を並べた姿です。IT Postは2026年10月27日の記事でOpenAI側の3成果を報じましたが、その時点ではAnthropic側の論文はまだ公開されていませんでした。本記事は、その「もう一社」の側を扱います。検証体制にも違いがあり、OpenAI側は予想の提唱者を含む外部グループが検証と解説を担う形を公表していますが、Anthropic側の論文については、現時点で人間による査読結果は公表されていません。

私たちへの影響

一般の利用者への直接の影響は、現時点ではありません。パスワードが速く破られる、暗号が危なくなる、といった話とは無関係です。今回のアルゴリズムが従来手法を上回るのは、現実には到達しない規模の入力においてだけだからです。

影響があるとすれば、研究の進め方の方です。「AIモデルが予想の反証らしきものを出した。形式化も付いている。では誰が、どうやって正しさを確かめるのか」という、検証側の手順と人員がボトルネックになる時代の到来を、この一件は象徴しています。成果を出す速度に、確かめる速度が追いつかない。その差が開くほど、「発表」の重みは下がり、「検証済み」の重みが上がります。

初心者が知っておくべきこと

Q. 3-SATとは何ですか。

A. 「はい／いいえ」で答えられる変数の組み合わせについて、与えられた条件式を全て満たす組み合わせがあるかどうかを問う問題です。組み合わせの総数は変数が1つ増えるごとに2倍になるため、しらみつぶし（総当たりそうあたり）では変数が増えるとすぐに手に負えなくなります。配送ルートの最適化や回路設計など、多くの実問題がこの形に帰着します。

Q. 指数時間仮説が否定されると、P対NP問題が解けたことになりますか。

A. なりません。P対NPは「多項式時間で解けるか」という一段強い問いです。今回の主張は「指数時間よりは速く解ける」というもので、多項式時間には程遠く、P対NPの決着とは別物です。論文もその点を明記しています。

Q. Leanによる形式化があれば、証明は正しいと言えますか。

A. Leanは、形式化された文に対する証明の論理が正しいかを機械的に検査します。ただし「形式化された文が、論文が主張したい定理と本当に同じ意味か」は人間が目で確かめる部分として残ります。今回のリポジトリも、その留保を自分で書いています。

IT Postの見方——勝負は「解いたか」から「誰が確かめるか」へ移った

IT Postでは、この一件の本質は「AIが難問を解いた」ことではなく、数学の成果発表の作法そのものが変わり始めたことだと考えます。著者はモデル名義、発見の来歴はトークン数付きで開示、証明は形式化して公開、ただし意味の一致は人間待ち。査読誌に載る前のプレプリントですら、ここまで「検証可能な形」で出すのが新しい標準になりつつある。

そして同じ日に同じ結論へ2社が到達した事実は、フロンティアモデルの研究能力が、特定の1社の飛び道具ではなく、業界全体の水準として上がってきたことを示している。差がつくのは、モデルの賢さそのものより、検証を引き受けてくれる人間のコミュニティをどれだけ味方に付けられるかだ。OpenAIが提唱者本人を検証側に招いたのは、その意味で一番賢い一手だった。Anthropicの論文に、人間の側からの応答がいつ、どんな形で返ってくるか。そこがこの話の本当の続報である。

※個人の感想です

今後どうなりそうか

焦点は2つあります。第一に、計算量理論の研究者コミュニティが両社の証明をどう評価するか。第二に、ETHを前提に積み上げられてきた800本超の論文の条件付き結果を、分野としてどう扱い直すかです。いずれも、結論が出るまでには時間がかかると見られます。

IT Postでは、検証側の動きや両社の続報が出た場合は、本記事を更新して追います。