读懂｜Claude 也称推翻指数时间假设，用了 1400 万词元

Anthropic 公开 Claude 写出的 3-SAT 次指数算法与 Lean 证明，称与 OpenAI 同日得出。论文自己算过，规模到天文数字前它不比穷举快。

指数时间假设的反例，现在有了第二个独立来源：Anthropic 公开的论文写明，它的内部研究模型在 10 月 16 日得到核心算法，和 OpenAI 公告里写的日期是同一天。

据 Anthropic 在 GitHub 上公开的 formal-math 仓库，这份结果包括一篇署名「Claude」的论文和一套 Lean 4 形式化证明，提交时间是北京时间 10 月 27 日上午。

我们的判断是：两家各自拿出反例，这个假设被推翻的可信度比昨天高了一截；但对写代码、买算力和用加密的人，眼下什么都没变。

两份结果同一天得出

OpenAI 10 月 26 日的公告写明，它的系统 10 月 16 日找到否证，次日完成 Lean 形式化。我们昨天那篇稿件写的就是这一份。

Anthropic 论文的「来源说明」一节写着，核心算法由内部 Claude 研究模型在 10 月 16 日找到，输出约 1400 万词元，过程中没有人类输入；研究人员随后和 Claude 一起改写了论文的表述。

论文还写了一句：OpenAI 的内部模型独立且同时地声称证明了类似结果。两家都没有说看过对方的材料。

论文给出的是一个确定性算法，能在次指数时间内数出 3-SAT 公式有多少组满足赋值。此前最好的确定性算法是 1.328 的 n 次方量级，仍是指数时间。

但论文自己算过账，结论写得很直白：

所以 Anthropic 在仓库首页写明，这个结果纯粹是渐近意义上的，对实际求解公式没有任何说明意义。

据 TechCrunch 报道，MIT 的 Ryan Williams 问过 OpenAI 是否检查了对加密系统的影响，得到的答复是对方有相当把握不会造成破解。

真正要改写的是理论文献。论文称，Claude 做的文献检索找到 800 多篇论文，至少有一项结论只在指数时间假设或更强的假设成立时才成立。

推翻指数时间假设，也就推翻了更强的版本 SETH；论文同时写明，它没有推翻正交向量假设，细粒度复杂性里很多下界靠的是后者。

Williams 对 TechCrunch 说，每个计算机科学家都该给 P=NP 的可能性多加一点权重，但他不认为 OpenAI 的算法就是能得到的最好算法。

两家都附了 Lean 证明，这是这次比以往更容易检验的地方。Anthropic 的说明写明，证明只依赖 Lean 的三条标准公理，并用另一套独立编写的内核复查过一遍。

同一份说明也写清了边界：没有任何机器能检查定理陈述文件是否说的就是论文里那句话，这一步只能靠人读。这也是 OpenAI 请 Impagliazzo、Paturi 和 Williams 三人小组来做的事。

有人会说，两家同日得出结果，本身就值得怀疑。据 TechCrunch 报道，Anthropic 的数学家 Levent Alpöge 曾暗示 OpenAI 的解法建立在已有工作之上，几小时后 Anthropic 发布了自己的反例。

我们接受这里有竞争的成分。但两份材料都公开了 Lean 证明，可信与否最终要看外部研究者的核对，与谁先发布无关。

两家独立得出同一个方向的结论，比任何一家单独宣布都更难被一句「模型出错」带过。这是分析推断，依据是两份证明来自不同的模型、各自完成形式化。等复杂性理论学界给出第一份对照两份证明的意见，这个判断才算落地。