2026年10月16日、OpenAIの内部モデルが67ページの数学的証明を生成し、指数時間仮説（ETH）が偽であると主張した。同日、AnthropicのClaudeは人間の介入を一切受けることなく、1400万の出力トークンを費やして独立に同一の結論に達した。両文書はその後Lean形式言語に翻訳されて機械検証が行われ、いずれも通過した。
複雑性理論ブログComputational Complexityの著者であるジョージア工科大学のLance Fortnow教授の評価によれば、両機関が提示したアルゴリズムはk-SAT問題を $(n+m)^{O(1)} \cdot 2^{O(n \log\log n / \sqrt{\log n})}$ 時間で解くことができる——この量級は準指数時間（2^o(n)）と呼ばれ、理論上「指数時間より本質的に速い3-SATアルゴリズムは存在しない」というETHの核心的主張を直接反駁するものである。Fortnowは「私自身がこの証明を検証したわけではないが、今や指数時間仮説は終焉を迎えたと安全に見なせる」と記している。
ETHとは何か、なぜ重要なのか
指数時間仮説は、Russell Impagliazzo、Ramamohan Paturi、Francis Zaneによって2001年に共同提唱された。その核心的命題は「3-SAT問題は最悪ケースにおいて指数時間を要し、本質的に速いアルゴリズムは存在しない」というものである。この仮説はP≠NPとは等価ではないが、その後25年間にわたって数百本のアルゴリズム複雑性論文の前提として使用され、理論計算機科学における事実上の礎石の一つとなっている。
だからこそ、OpenAIが10月26日にGitHubリポジトリを公開し、自然言語による証明とLean形式化版を同時に公開した際、アルゴリズム理論界の反応は喜びではなく慎重さであった。ETHの原著者であるImpagliazzoとPaturi、そしてマサチューセッツ工科大学のRyan Williamsは直ちに公開声明を発し、「これほど重大な結果は厳密な独立審査を必要とする」と述べた。三者は独立審査グループを組織し、Williamsは「守秘義務契約への署名も報酬の受領もない」と明言した。
Lean通過：これは何を検証したのか
Leanは数学的定理証明支援システムであり、すべての論理推論ステップの形式的妥当性を逐次検証することができる。OpenAIは自然言語による証明を生成した翌日にLean形式化を完了した。
Leanが検証したのは「このLeanコードがその前提から論理的に整合している」ということであり、「これらの前提がETHの完全な数学的記述と数学的に等価である」ということではない。公開されたLeanリポジトリの説明によれば、この形式化版が検証したアルゴリズムの界は「主要な数学的主張よりわずかに弱いバージョン」である——すなわち、Leanが証明した命題と論文本文の命題との間には技術的な乖離が存在し、その乖離の等価性自体はいまだ形式化されていない。
独立研究者のRyan O'DonnellとShiva Kintaliはその後それぞれ簡略化版のフォローアップ証明を公開し、最適な界を犠牲にして明瞭さを優先するという意図的な選択をした——専門コミュニティは、機械支援による高度に圧縮されたこの証明を、人間が追跡可能な形式に再翻訳しようと努力している最中である。
両社が同日独立して同一の結論に到達
Anthropicが開示した一つの詳細：Claudeは問題解決の過程で「人間の入力を一切受けず」、1400万の出力トークンを使用した。この規模は、Claudeが生成した推論の連鎖がいかなる人間数学者の単回の作業量をも大幅に超えることを意味する——それはおよそ3万ページ分の草稿に相当する。
両社が同日独立して同一の準指数界 $2^{n/\sqrt{\log n}}$ に到達したことは、むしろ次のことを示唆している。現在のAI能力水準において、この数学的経路はすでにモデルの「到達可能領域」に入っており、ただこれまで誰も意図的に試みていなかっただけである。これは突破と言うよりも、能力の境界を測定する試みである——人間のロードマップなしに、AIはどこまでの探索空間で有効な数学的構造を見つけられるか、という問いへの答えである。
暗号学的パニックに根拠はあるか
現行の主流な公開鍵暗号システム（RSA、楕円曲線暗号）のセキュリティは、整数因数分解と離散対数問題の困難性に基づいており、ETHに直接依存しているわけではない。ETHの反駁は特定のアルゴリズム的界の仮定が失効することを意味するが、整数因数分解が容易になることを直接意味するわけではない。
より直接的な定量的評価はAnthropicの論文自身から得られる。変数ごとに5つの節を持つ3-SATインスタンスにおいて、そのアルゴリズムが実際の効果において全数探索を上回るには、問題の規模が $10^{10000}$ 変数に達する必要がある。この数字が意味することは、仮に証明が成立しても、このアルゴリズムは地球上のいかなる予見可能な計算装置においても実際のSAT求解効率の向上をもたらさないということである。既存の暗号インフラに対する直接的な脅威は現時点では存在しない。
AI支援数学：信頼メカニズムの欠陥
この出来事は、単一事件の欠陥ではなく、AI科学的発見の領域における構造的問題を明らかにした。
伝統的な数学コミュニティにおける信頼構築のメカニズムは、専門家が証明を読み理解し、欠陥を発見し、査読を経て、時間をかけて定着させるというものである。このメカニズムは、AI生成の高密度な証明に直面して圧力にさらされている。証明が67ページに及び、機械によって逐次構築され、形式化検証を通過したものの、大多数の専門家のリアルタイム読解速度を超えている場合、「証明済み」という合意はいかにして形成されるのか。
Leanシステムは新たな経路を提供する。すなわち、信頼を「専門家が読み理解できるか」から「形式システムが論理的に整合しているか」へと移行させる経路である。しかしこの経路には二つの前提が同時に成立している必要がある。第一に、Lean内の形式的声明が元の数学的命題を忠実に再現していること。第二に、Leanシステム自体の信頼性が十分に確立されていること。前者は現時点でいまだ未解決の問題であり、後者は理論計算機科学界においてすでに比較的強固な合意があるものの、絶対的なものではない。
ETH原著者のImpagliazzo、Paturi、Williamsが現在行っていることは、本質的にこの欠陥を修復することである。すなわち、「形式的声明が元の命題と等価か」を最も的確に判断できる者たちが、人手による検証の層を補完している。この層は事後的な補修であるべきではなく、AI支援数学的発見の標準的なプロセスとして組み込まれるべきものである。
独立した判断
現時点で確認可能な証拠から、以下の判断を示す。
成立する可能性が極めて高い部分：AIモデルは理論的複雑性のある技術的経路において実質的な数学的進展を達成した。Lean検証の通過、そしてトップクラスの複雑性研究者が無報酬で独立審査に時間を投じていること、この二点は肯定的なシグナルである。Lance Fortnowの慎重な楽観主義は、理論界における現在の主流的な受け止め方を代表している。
いまだ閉じられていない欠陥：Lean形式的声明とETHの完全な数学的記述との等価性は、いまだ形式化されていない。これは些細な欠陥ではなく、現在の独立審査全体の核心的作業である。それが確認されるまで、「ETHが反駁された」は確認済みの結論ではなく、高い確信度を持った予測に留まる。
より大きな図式：今回の出来事は、数学的発見におけるAIの真の能力の境界を示した——AIは人間のロードマップなしに、高度に技術的な数学的構造を極めて速く完成させることができる。しかし同時に、既存の知識検証体制の脆弱性も露わにした。AIの出力速度が人間の検証速度を超えるとき、科学コミュニティが基準を下げることなくこれらの成果を適時に消化するにはどうすればよいか——これは今後数年間の核心的な制度的課題であり、数学そのものの難しさと同等に重要である。
© 2026 Winzheng.com 赢政天下 | 转载请注明来源并附原文链接