OpenAI与Anthropic的内部AI系统独立得出了指数时间猜想（Exponential Time Hypothesis, ETH）不成立的证明。双方于10月26日相隔数小时公布结果，并将核心发现日期追溯至同一天：2026年10月16日。若这些证明通过独立严格审查，研究人员可能需重新审视超过800篇以ETH为基础假设的已发表论文。
指数时间猜想由Russell Impagliazzo和Ramamohan Paturi于1999年提出，2001年形式化。该猜想认为3-SAT问题无法在次指数时间内求解。过去二十五年间，图论、计算生物学、数据库优化等领域的大量研究均建立在此假设之上。
这两份由AI生成的证明均经过Lean 4验证，代码已公开在GitHub上。
OpenAI：十天内的三项突破
OpenAI宣布其未发布内部模型取得了三项成果。其中最重要的是论文《指数时间猜想是错误的》，描述了一种确定性算法，能在多项式空间内，以约 $2^{n/(\log n)^{1/2+o(1)}}$ 的时间精确计算k-CNF公式的解的数量。这直接驳斥了ETH。
该模型于10月16日生成自然语言证明，次日形式化为Lean代码。相关文档和代码已在GitHub公开。
此外，OpenAI的模型还证明了局部平滑猜想在所有维度下成立，从而解决了Kakeya猜想和Stein限制猜想；并严格证明了四维相互作用量子场论某些存在性，触及克雷数学研究所千禧年大奖难题之一。OpenAI表示，学术荣誉应归于解释和验证工作的研究人员，公司本身不申请奖项，并单独向西蒙斯基金会捐赠500万美元，支持AI生成数学相关的研讨会。
ETH创始人领衔独立审查
ETH提出者Impagliazzo、Paturi与麻省理工学院的Ryan Williams组成团队，独立检查该结果。三人发表公开信强调，参与审查不代表认可主张，重大结果需仔细独立验证。他们未签署保密协议且无报酬，要求OpenAI公开原始数据并资助社区会议，OpenAI已同意。
针对物理学结果，诺贝尔奖得主David Gross领导另一小组进行更谨慎的审查，拒绝直接发布AI材料，自行整理成果。
Anthropic：Claude同日完成发现
Anthropic随后发表论文《3-SAT的 $2^{o(n)}$ 时间算法》，作者署名为“Claude (Anthropic)”。其内部研究模型于10月16日在无人类介入下发现核心内容，使用1400万个输出token。研究人员随后与Claude合作改进表述。
两家实验室互不知晓对方进展。Anthropic的证明还驳斥了强指数时间猜想（SETH），意味着独立集、团等问题的理论算法可更快运行。数学家Jelani Nelson指出，两份证明的渐近运行时界限相近，约为 $\exp(O(n / \sqrt{\log n}))$。
Lean验证的局限与意义
Lean 4验证了证明的逻辑一致性，但无法保证形式化表达忠实于AI的自然语言论证。Anthropic额外使用Rust编写的nanoda内核进行二次确认，以排除Lean自身检查器可能遗漏的错误。然而，截至发表时，尚无人类手动逐行审查Claude的论证过程。
Impagliazzo等人的审查旨在填补这一空白：确认证明策略是否如声称般运作，以及Lean形式化是否正确代表该策略。
实际影响与荣誉归属
尽管ETH被驳斥，但新算法仅在变量规模达到 $10^{10,000}$ 时才优于暴力搜索，对现实问题无实际加速效果，也未解决P vs. NP问题。OpenAI总裁表示，P很可能仍不等于NP。
若证明属实，依赖ETH下界的800多篇论文需重新评估其形式化依据。关于荣誉归属，OpenAI和Anthropic均放弃学术认可，指向验证人员。这一事件加剧了关于AI生成成果归属规范的讨论，《莱顿宣言》及“人类数学协会”均呼吁建立新标准。
目前，西北大学数学家Ethan Sussman已设立公共GitHub仓库供独立检查。Impagliazzo、Paturi和Williams的判决将成为领域内的权威信号，确认这是否为计算复杂性理论的转折点。