FRONTIER · 落到现实

ETH 倒了：十天里两家实验室的模型各自推翻了 3-SAT 的指数下界——而这个算法要等 n 超过 10 的一万次方，才真的比暴力枚举快

The Exponential Time Hypothesis is False / A 2^{o(n)} Time Algorithm for 3-SAT

OpenAI 与 Claude（Anthropic） OpenAI 那份《指数时间假说是假的》10 月 17 日首发、10 月 25 日改定，给出确定性的 #k-SAT 计数算法，只用多项式空间，一次推翻 ETH、SETH、Gap-ETH、NSETH 与计数版 #ETH · Anthropic 那份的署名栏直接写着「CLAUDE」，论文自述核心算法是 10 月 16 日由一个内部研究模型在一次 1400 万输出 token、无人类输入的会话里做出的 · 两份的主结果都已在 Lean 4 中形式化 · ETH 的两位提出者 Russell Impagliazzo、Ramamohan Paturi 与 MIT 的 Ryan Williams 出面组织社区核查，并公开声明「我们的参与不构成对这项主张的认证」

2026 年 10 月

为什么选它ETH 是过去二十多年细粒度复杂性的承重墙，八百多篇论文的下界只在它成立时才成立。这一篇让你一次看清三件事：倒掉的到底是什么、为什么这个算法在现实里永远跑不赢暴力枚举、以及一个学科在十天内怎么组织人手去检查一份机器写出来的证明。最后一件别处看不到。

10 月 17 日，OpenAI 挂出一份预印本，标题就是一句陈述句：《指数时间假说是假的》。九天后，Anthropic 挂出另一份，《一个 2^o(n) 时间的 3-SAT 算法》，署名栏里写的是「CLAUDE，ANTHROPIC」。两份互相独立的工作给出了同一件事：判定一个 3-SAT 公式能不能被满足——甚至数清它到底有多少组解——可以在 2^o(n) 时间内做完，这推翻了 1999 年提出、此后被整个细粒度复杂性领域当作地基的指数时间假说（ETH）。10 月 28 日，Lance Fortnow 在他那个开了二十多年的复杂性博客上写：我自己没验证，但现在可以安全地认为，指数时间假说已经凉了。

值得读的理由不是「AI 又解了一道难题」。本栏今年写过 Claude 把费马大定理写成 1300 万行 Lean（第 57 篇）、一万个 agent 证出纳维-斯托克斯会爆破（第 66 篇）、矩阵乘法指数被往下推（第 51 篇），那些都是在一道已经摆好的题目上往前拱一格。这次不一样的地方在于：倒掉的是一个从没被证明过、却被所有人拿来当前提用的假设——Claude 自己做的那次文献检索数出八百多篇论文，它们的某个下界只在 ETH（或者蕴含 ETH 的更强假设）成立时才成立。而同样该一起读的是第二层：这个算法在可预见的宇宙里永远不会比暴力枚举快，这句话是 Anthropic 自己写在论文第 2 页上的。

ETH 是什么：一个没证明过、却被八百篇论文当地基的前提

3-SAT 是这样一道题：给 n 个布尔变量和一串「三选一」的子句，每个子句要求其中至少一个文字为真，问有没有一组赋值能让所有子句同时成立。它是 NP 完全问题的原型，最笨的做法是把 2^n 种赋值全试一遍。四十年里算法界一直在往下压这个指数，到去年为止，确定性算法的最好纪录是 O(1.328^n)，随机算法 O(1.308^n)——全是常数因子上的让利。1999 年 Impagliazzo 和 Paturi 把「这种让利不可能无限做下去」写成了一条假设：存在某个 c>0，任何算法解 3-SAT 都需要 2^cn 时间。这就是 ETH。它从没被证明过，但它能把「这个问题很难」变成可以在问题之间传递的结论，于是整个细粒度复杂性就建在它和它的加强版 SETH 上面：k-团的 n^o(k) 下界、树宽动态规划的最优性、编辑距离的二次方下界，背后都是它。两份新论文一次把 ETH、SETH、Gap-ETH、NSETH 和计数版的 #ETH 全部掀掉。

两份证明，十天，以及 1400 万 token

两条技术路线不同，形状却像：都不直接判定可满足性，而是去数满足赋值的个数（更难的 #3-SAT），再看这个数是不是零；都是确定性算法，都只用多项式空间。OpenAI 那份的时间是 (n+m)^O(1)·2^{O(n·loglog n/√log n)}，Anthropic 那份在子句数 m 上给到 2^{O(km/√log m)}。Ryan O'Donnell 把 OpenAI 的证明重写成了一个好懂得多的形式：核心其实是精确计算一个每行每列只有常数个非零元的稀疏矩阵的积和式，再靠经典归约把 3-SAT 计数搬过去——他在脚注里注明，这份讲义本身也是「通过与大模型交互产出的」。更该注意的是产地。Anthropic 在论文里写明：核心算法是 10 月 16 日由一个内部研究模型做出来的，那次会话用掉 1400 万输出 token，没有人类输入；研究员做的是把它改写成一篇能读的论文。这不是孤例——10 月初 Alman 与 Vassilevska Williams 那篇把 3SUM 压到 O(n^1.9992)、APSP 压到 O(n^2.9995) 的论文，算法同样来自 Claude：当时 Anthropic 的员工让它去查密码学里 Zero-k-Clique 平均情况难度的构造，它没去查，自己做出了这个算法，1600 万 token，也没有人类输入。这几件事的主结果都已经过 Lean 4 的机器检查（OpenAI 那份机器证到的界比论文正文略弱）。

先别高兴：n 要大过 10 的一万次方，它才比暴力枚举快

Anthropic 的论文自己交了底：对 m=5n 的一般 3-CNF，他们证出来的界在 n 超过 10^10000 之前都不优于暴力枚举的 2^n；只按变量数算的那个界，要 n>10^8 才开始生效。原话是：「暴力枚举在 n=100 时就已经不现实了，所以我们的改进不会出现在实际场景里。我们的结果对实际求解只字未说。」维也纳工业大学的 Stefan Szeider 照 OpenAI 自己设定的参数又算了一遍：正文那套构造在 n 超过 2^(10^10) 之前全程等同于穷举，支撑主定理的附录 D 算法至少要等到 n+m 超过 2^131071。10 月 30 日 Ruhollah Majdoddin 的一篇 arXiv 论文专门做「把门槛往下压」这件事：在子句密度为 1 时，交叉点从 2^33858 个子句降到约 2^420 个——仍然是这个宇宙装不下的数字，而他顺带证明了这道距离是结构性的：在他定义的那一类算法里，低于约 2^6000 个变量不可能有任何收益。所以正确的读法是：ETH 作为一个渐近命题是假的，而它想描述的那件事——3-SAT 在人类够得着的规模上很难——一个字都没变。

废墟里剩下什么，以及一个学科连夜搭出来的检查流程

下界会倒一片，但不是全倒。Fortnow 提醒：这个算法只管 k-SAT，对子集和、旅行商毫无改善，因为从它们归约到 3-SAT 会把变量数撑爆；要让整个 NP 都变成次指数，得把 3-SAT 做到 2^{n^o(1)}，离得还远。正交向量猜想没有被推翻，靠它撑着的那批二次方下界还活着。Szeider 另有一份笔记做了最实用的事：他把教科书里 29 条基于 ETH 的下界逐条过了一遍，20 条在几个没被推翻的更弱假设下原样成立，另外 9 条以削弱的形式成立，他还顺手提了个替代品——k×k 团假设。而这十天里最该被外行看见的，是 Impagliazzo、Paturi 和 Ryan Williams 的动作：10 月 26 日三人开了一个公开博客来组织核查，开篇就写「我们的名字可能会随这次发布一起出现，但我们的参与不构成对这项主张的认证」。随后那里长出了一整套东西：三份互相独立的简化讲义；一个「Lean 复现」专帖——有人在本地重跑两家的形式化并报告编译通过，组织者说这在理论计算机科学里是个新习惯，过去只有实验科学才讲复现；还有一个征集后续结果的帖子，几天里就堆进了新的电路下界、NTIME 对 DTIME 的新包含关系、以及一批参数化算法的显式速率。

这件事的新信息不是「AI 会做数学」，是它第一次拆掉了一面承重墙。解一道难题和推翻一个前提，分量完全不同：前者给学科添一块砖，后者要求八百多篇论文的作者重新去看自己的第一段写了什么。更值得留意的是节奏——9 月 Claude 在一次查密码学构造的会话里顺手做掉了 3SUM 和 APSP，10 月 16 日另一次会话做掉了 ETH，两次都是「没有人类输入」，而人类合作者的角色统一变成了理解、简化、改写、担责。Alman 和 Vassilevska Williams 在论文里专门写了一句「作者对本文承担全部责任」，这句话以前不需要写。但「ETH 是假的」和「3-SAT 变好算了」之间，隔着整个宇宙。交叉点要到 n 超过 10^10000、或者 n+m 超过 2^131071，这不是「暂时还不实用」，是永远不会实用——而且这件事是作者自己先说的，不是批评者挖出来的。我认为这正是这篇最有教育意义的地方：当机器开始大量产出数学上为真的命题，读者唯一的防线是学会问「它从多大规模开始成立」。接下来几年一定会有人拿着「ETH 已被推翻」去论证密码学不安全、去论证某个 NP 难问题现在可解了——这类话一句都不要信。要警惕的第二条，是 Szeider 对 Lean 的那句提醒。他指出 OpenAI 的 Lean 语句先固定了机器模型和常数，才对所有公式做全称量化，而语句里并不含这些常数的值；有人在复现帖里也说，「这台机器上的定理」和「教科书意义上的 ETH」之间那一步，两家都还是非形式的。形式化保证的是推导无误，不保证你问对了问题——这和第 57 篇是同一个调子：被自动化掉的首先是审稿，不是判断。最该抄作业的其实是 Impagliazzo 他们那套十天搭起来的流程。三位当事人先声明「参与不等于认证」，再把工作拆成四摊公开认领：重写讲义、本地复现形式化、清点哪些下界还活着、征集新推论。这是一个学科被机器的产出速度压过来之后，给出的第一个像样的接口，而它对任何要把 AI 产出接进自己流水线的团队都适用——把机器可验证的部分和必须由人判断的部分分开标注，然后把检查这件事本身当成值得署名的工作。

计算复杂性AI 做数学形式化验证渐近与现实科研范式

去读原文 本文是原创导读，不是原文翻译——真正的细节、证据和微妙之处都在原文里。原文OpenAI《指数时间假说是假的》：确定性 #k-SAT 计数算法，以及附录 C 列出的一连串后果 → 原文Anthropic / Claude《一个 2^o(n) 时间的 3-SAT 算法》：第 2 页的 Provenance 与「本结果对实际求解只字未说」就在这里 → 原文Impagliazzo、Paturi、Ryan Williams 致 TCS 社区：为什么要核查，以及关于 AI 产出成果的三个规范问题 → 原文后续结果征集帖：Szeider 的两份笔记（交叉点与「哪 20 条下界还活着」）和各家新推论都在这条评论线里 → 延伸Lance Fortnow 的技术向解读：ETH 倒了之后，哪些下界跟着倒、哪些一点没动 → 延伸Majdoddin：把交叉点从 2^33858 个子句压到约 2^420，并证明这道距离是结构性的 →

上一篇六个最强模型进了一间真实验室：92 个任务只过了 45.3%，而它们的错是拿冻着的样品去移液、给开着盖的孔板涡旋、一个枪头用到底下一篇你没法确认对面是哪个模型——4000 亿参数的一次推理被压成 19 MB 收据，CPU 上 17 秒验完，代价是 70 到 95 倍算力

本文为 AKL AI Club 原创撰写的导读，不是原文翻译；著作权归原文作者所有。篇目由编辑独立选取，来源均经人工核实。