AI捅了复杂性理论的马蜂窝

两个全球最烧钱的大模型实验室，最近交出的不是新模型，而是一份可能动摇理论计算机科学地基的作业。OpenAI与Anthropic相继公布：内部大模型推导出3-SAT的亚指数时间算法，并给出了Lean形式化证明，矛头直指支撑细粒度复杂性研究27年之久的指数时间假设（ETH）。

我的核心判断是：这件事真正的看点，不是AI又一次'考了高分'，而是数学发现第一次获得了机器可验证的信任底座——如果推导经得起考验，图论、数据库等领域百余项基于ETH的算法下界，都要重新排队体检。

🔥 一份Lean证明，两家实验室同时出手

在数学圈，把一句话变成机器检查过的证明，往往比想出这句话更难。

这事在圈子里的传播路径很典型：先是一批材料在小范围流传，随后OpenAI与Anthropic先后放出正式成果——各自的大模型推导出了3-SAT的亚指数时间算法，而且都附上了Lean形式化证明。两个互为最直接对手的公司，几乎在同一时间做同一件事，这在算法理论圈并不多见。

先补一下背景。3-SAT是NP完全问题最标准的'试金石'形态。2001年，Impagliazzo与Paturi提出指数时间假设（ETH）：3-SAT不存在亚指数时间算法。过去27年，它成了精细复杂性研究默认的地基——研究者用'假设ETH成立'的方式，证明了大量具体问题的难度下界。而这次两家公司的模型给出的，是反方向的构造：一个亚指数算法，加上一条机器可验证的推导链。

整件事的逻辑链条其实很清晰：

值得注意的是'形式化证明'这个细节。数学共同体几百年靠同行评议建立信任，人类证明藏错是常态；Lean这类证明助手把推导拆成机器逐条核验的形式化代码，'对不对'不再取决于审稿人有没有看漏。据多位接近人士的说法，学界的第一反应不是欢呼算法多妙，而是排队去读Lean文件——这本身就是一个信号：可机器验证，正在成为数学成果的新信任货币。

🧱 撑了27年的地基，塌一角意味着什么

下界是算法工程师的地图边界——地图错了，天不会塌，但原来标着'此路不通'的方向，突然可以走了。

很多做系统的工程师对ETH无感，这很正常，它听起来像纯理论。但换个说法：你在数据库里做的查询优化、在图计算里做的子图匹配调度，背后都有一批'已经被证明不可能更快'的结论撑腰，而这些结论大多是条件性的——'假设ETH成立，问题X至少需要f(n)时间'。换句话说，ETH不是一条定理，而是全行业共用的一条公理。

27年里，百余条这样的条件性下界挂在了ETH上，覆盖图论、数据库、调度、组合优化等方向。这次如果亚指数算法站住，这些下界不是全错，而是要逐条重估：有些结论随假设强度下降而松动，有些则需要换更强的假设重新证明。复杂度上的差距，用一张示意表感受最直观（取简化形态，仅作量级示意）：

再放一张行业内的定位图，看清各方的位置：

精细复杂性的价值在于'细颗粒'——它不停留在P≠NP这种粗判断，而是回答'到底多慢、慢多少'。这直接决定工程上值不值得再压榨常数。一旦地基动了，重估不是学术洁癖：对数据基础设施厂商来说，理论下界影响的是研发路线图——哪些优化方向被认定是'理论死路'，哪些值得继续投入。据业内私下流传的看法，已经有数据库方向的团队在盘点自己引用过哪些ETH条件性结果。

💼 对数据人来说，这不是茶余饭后

亚指数到多项式之间，隔着的不是一步，而是整个工程世界。

想象一个图数据库团队面对子图匹配的组合爆炸。过去的标准答案是：这是NP难问题，理论上就是指数的，我们只能做启发式剪枝。如果3-SAT真的存在亚指数算法，类似的参数化问题也可能松绑——'指数'两个字后面，藏着的优化空间比想象中大。受影响的方向可以拉出一张清单：

但这里要先泼一盆🧊冷水：亚指数不等于多项式。即便ETH被打破，新算法的复杂度大概率仍是2的（比n温和但依然爆炸的）函数。看上面那张示意表：n=100时，2^√n量级已经远小于2ⁿ，但仍显著高于多项式。对线上系统动辄百万级实体的数据场景，这不会立刻改变任何一条SQL的执行计划。

不过这不妨碍它成为数据产业值得盯的三个理由。其一，条件性下界的文献需要重审，理论上'死路'的方向可能复活，对数据库内核和求解器厂商是新的差异化机会；其二，'AI推导构造性对象+形式化验证'的范式一旦跑通3-SAT，下一个被海搜的可能是查询计划、调度方案、编码结构这些更贴近工程的对象；其三，复杂度理论一直影响硬件与系统设计的长期赌注，比如专用加速器该押哪些问题形态。

⚠️ 冷静看：从'推导出'到'学界接受'，隔着三条线

推翻一个27年的假设，需要的不是一次公告，而是一整个复核周期。

社区的反应目前很分裂：一半人在转发截图，另一半人在逐行读Lean代码。据多位接近人士描述，质疑的焦点非常具体——形式化证明覆盖的命题边界在哪里？算法是否真的绕开了已知的技术障碍？推导过程中有没有隐含依赖比ETH更强的前提？

客观地讲，有三条线必须跨过去。第一，Lean证明证明的是'这段推导逻辑成立'，而成果的分量还取决于它形式化了哪些命题——是完整冲击ETH级的结论，还是某个中间引理，意义完全不同；第二，27年来理论上逼近3-SAT指数边界的尝试从未成功过，社区有充分的怀疑惯性，这次也不会例外；第三，亚指数与多项式时间之间的鸿沟依然巨大，即便一切成立，也不改变NP难问题的工程本质。

把水面上下拆开看，这件事的显性成果和隐性根基是两回事：

我更愿意把这次事件看作一个范式的验收测试，而不是一次'科学被颠覆'。真正稀缺的资产是那条流水线：大模型负责在巨大的证明空间里做构造性搜索，Lean负责把'AI是不是在胡说'变成机器可判定的问题。这条流水线今天产出了一个理论算法，明天就可能产出更紧的界、更优的数据结构——对以算法为生的数据产业来说，这才是可持续的复利。

小结

ETH现在还谈不上'被推翻'，接下来数月的社区复核才是关键窗口：站住了，图论与数据库领域百余项条件性下界要排队重估，算法教科书得写勘误；站不住，'AI推导+形式化验证'的流水线也已经展示了另一种做研究的方式。对数据行业的务实姿态是：盯复核、盘引用、别急着改架构——但请把'机器可验证的数学发现'，写进你明年的技术雷达。