AREX Feed Article
Anthropic 论文称：内部 Claude 模型独立反驳指数时间假设，1400 万 token、无人工输入
2026 年 10 月 27 日（UTC 04:20），AI 评论作者 Andrew Curran 在 X 上发帖：「这非常令人困惑：一个内部 Claude 研究模型也于 10 月 16 日独立反驳了指数时间假设（ETH），输出 1400 万 token，无人工输入」，并附上一张论文截图（）。一分钟后他跟发链接，指向 Anthropic 在 GitHub 的 formal-math 仓库中的论文 PDF（）。这篇题为《A 2^o(n) Time Algorithm for 3-SAT》的论文署名 CLAUDE（ANTHROPIC），标注日期为 2026 年 10 月 26 日。
关键段落写在公开的论文里，可以逐字核对。第 2 页的「Provenance」一节写明：「核心算法由一个内部 Claude 研究模型于 10 月 16 日发现，产生 1400 万输出 token，无人工输入。Anthropic 研究者与 Claude 合作改进了表述，形成了这篇论文。」紧随其后还有一句：「独立且同期，OpenAI 的一个内部模型声称证明了类似的结果。」也就是说，这是 Anthropic 出自自家论文的单方声明，反驳是否成立目前没有任何独立判定；OpenAI 那边就同一断言发布的预印本，同样只是其自己的宣称。
一份署名 Claude 的论文自称反驳了 ETH
按论文摘要的说法，它给出一个确定性算法，在 n 个变量的 3-SAT 上以 2^o(n) 时间运行，从而反驳 ETH——Impagliazzo 与 Paturi 在 2001 年提出的猜想。该猜想断言存在固定的 δ>0，使 3-SAT 无法在 O(2^δn) 时间内解决，是比广被接受的 P≠NP 更强的猜想。论文称其算法还解决了更难的计数版本 #3-SAT：定理 1 称，对 m 个子句、n 个变量的 k-CNF（子句至多含 k 个文字的合取范式），算法可在 2^O(min{k²n·log log n/√log n, km/√log m}) 时间内算出可满足赋值的个数，其中 O(·) 隐藏一个绝对常数。
论文同时给出了几条边界内的推论：由于强指数时间假设 SETH 蕴含 ETH，反驳 ETH 也就反驳了 SETH（推论 5），但不触及 SETH 所蕴含、许多细粒度复杂性下界所依赖的 Orthogonal Vectors 假设。作为参照，论文列出的此前纪录是：确定性 3-SAT 算法 O(1.328^n)，随机算法 O(1.308^n)——都是对穷举 2^n 的常数因子级改进；新算法若成立，则是把运行时间压到次指数级。论文明确写道，这一结果「不直接触及 P vs NP 问题」，也不给出任何实用的 NP 完全问题算法。
机器检查了什么，机器查不了什么
论文的 Lean 4 形式化托管在同一仓库的 。该目录 README 顶部自称「研究产物。不维护，不接受贡献」，并写明「结果由一个内部研究 Claude 模型发现」，形式化由 AI 模型编写。文件 MainResults.lean 只陈述两个命题——ETHIsFalse 与主定理——除 Mathlib 外不依赖任何库，工具链钉在 Lean 4.33.1 与 Mathlib 4.33.1。
论文附录 E 写明机器已检查的部分：两个命题仅依赖 Lean 的三个标准公理（propext、Classical.choice、Quot.sound）；证明被 Lean 内核接受，又被重放检查器 leanchecker 逐模块复核，再经 Comparator 用一个独立实现的内核 nanoda 复检；整个开发的 1,050 个 Lean 模块从零共同构建过。eth 目录 README 补充了构建成本：24 个 vCPU 上约 8 分钟，最大进程约占 7 GB 内存；构建会打印两条 sorry 警告，均来自只陈述定理、留作更完整检查对照用的 Challenge.lean。
附录 E 同时写明机器查不了的部分：「这两个定义是否说了它们想说的话——即 ETH 为假与主定理——没有机器能检查；这要由这份清单的读者判断。」据论文，Lean 开发由 AI 模型编写、由同一模型的其他实例复核，「截至写作时，没有已知的人检查过它」，且其常数不是显式的。formal-math 仓库整体按 Palomar 提交模板组织， 说明 CI 会在相关文件变动时运行 comparator 检查，用 nanoda 内核与 landrun 沙箱复核。eth README 还给出一段「可被 AI 模型解读的浓缩版关键思想」，并称 Claude Opus 5.5 high effort 能据此重新推导出 ETH 反驳——不过只能得到对每个 δ>0 的 O(2^δn) 这一较弱形式，拿不到论文的更强界。
论文自己划出的边界：纯渐近，不改变实践
就在 Provenance 段上方，论文先用一段话压低了这个结果的实用含义：它是纯渐近的。对子句数 m = 5n/8 的一般 3-CNF 公式，除非 n > 10^10,000，所证明的界并不优于穷举的 2^n；只按变量数 n 计、对任意子句数都成立的那个界，要 n > 10^(10^8) 才不劣于穷举；论文估计其总体思路要 n > 10^7 才可能带来普遍改进。而 n = 100 时穷举早已不实用——「所以我们的结果所带来的改进不会出现在实际场景中」，「我们的结果对求解公式的实践没有任何说明」。
论文仍列出了若成立则可用的后果：Independent Set、Clique、Vertex Cover、Dominating Set 将都能在任意 δ>0 的 O(2^δn) 时间内解决；复杂度类 E^NP 不具有线性大小的布尔电路。论文还提到，一次由 Claude 完成的文献检索找到 800 多篇「仅在 ETH 或蕴含它的假设（如 SETH、Gap-ETH）下证明至少一个结果本身」的论文——这个数字说明的是这一假设在复杂性文献中承担的分量。
同一窗口里的另一份声明：OpenAI 的预印本
Anthropic 论文引用的 [Ope26]，指向 OpenAI 预印本《The Exponential Time Hypothesis is False》，标注日期 2026 年 10 月 25 日，存放于 OpenAI 的 。该的 README 称，其中收录一个内部 OpenAI 模型产出的数学手稿与证明材料：共 719 份手稿、归入 372 个 family（相关论文的归组）；绝大多数结果出自同一个未发布的内部模型，平均每个结果花费 3 小时 ChatGPT Pro 思考算力，评估中模型总共被问了约 4,000 道题；约 42% 的顶级结果已有 Lean 形式化，并且「部分未形式化的结果可能有问题」。
需要分开的是：这是两家实验室各自独立的声明，共享的只是同一个数学问题和同一时间窗口；现有材料并未把二者确立为同一事件或其不同阶段，两条声明也都没有独立判定。Curran 推文里的「也（also）」，正是相对 OpenAI 已经公开的预印本而言。
回复区最先出现的问题
Curran 的推文在发出后数小时内被浏览约 4 万次（截至本文检索时）。回复里最先浮现的是可核验性问题：用户 Marius du Preez 问：「问个小问题，Anthropic 之外的人能读到那 1400 万 token 吗？还是只有润色过的论文？」（）whb0821 用中文写道：「最值得关注的不是 1400 万个 token，而是 AI 能否独立挑战自己曾经依赖的假设。不过，长时间自主运行不等于结论正确，关键还要看推理过程能否复现、结果能否被独立验证。」（）
目前外部能独立核验的，是仓库公开的部分：论文 PDF、Lean 代码、构建与检查说明，均在 Apache-2.0 许可下可复现。而 10 月 16 日那次运行的过程本身如何被记录、能否复核，公开材料没有给出说明。截至发稿，这份证明的有效性仍停在论文附录 E 写下的那句判断上——论文写作时「没有已知的人检查过它」；两个实验室的反驳声明是否成立，也没有出现独立判定。