10月26日，OpenAI公开了一篇标题毫不含糊的预印本：《The Exponential Time Hypothesis is False》，直译就是“指数时间假设是错的”。它声称给出固定宽度布尔可满足性问题的确定性次指数时间算法，连满足赋值的精确个数也能计算。如果证明经得起独立检查，复杂性理论中一条沿用多年的条件性下界，将失去原来的支点。此刻更准确的新闻表述仍是：OpenAI提出了反证，并公开论文与形式化材料；学界审查正在展开。[1][2][3]
这条假设到底说了什么
先看3-SAT。输入是一串用“且”连接的子句，每个子句至多涉及三个变量或其否定；任务是找出有没有一组真假赋值，让整串公式为真。设变量数为 n，穷举赋值有 2^n 种。几十年来，研究人员做出了各种改进，但“能否把最坏情形的运行时间压到 2^{o(n)}”一直是另一个问题。指数时间假设（ETH）认为，3-SAT不存在这样的确定性次指数时间算法。这里的 n 是变量数；条件性的下界正是按这个参数来讨论的。[2][4]
这个假设之所以重要，在于它能给“问题究竟难到什么程度”提供比 P≠NP 更细的尺子。证明某个问题是NP困难，通常只能说人们不期待多项式时间解法；如果从3-SAT做参数保持的归约，还能得到它在ETH成立前提下需要怎样的指数级时间。精确算法、图算法和参数化复杂性中，许多“几乎已经最快”的结论都按这条路线写成。假设若倒下，这些定理的推导前提就要重新检查；原问题未必自动有新算法。[2][4]
从模型的发现到公开审查
OpenAI在10月26日的说明中称，内部模型于10月16日形成自然语言反证，17日完成Lean形式化。论文首页标明10月17日、25日修订，仓库单篇说明的发布日期为10月25日，作者栏署“OpenAI”。公司将手稿、代码和形式化文件公开，并表示不为模型发现索取学术署名。[1][2][5]
这样的发布方式本身就引人注目。研究者可以直接下载论文，检查算法每一步的复杂度估算，也可以核对Lean中的命题与证明。OpenAI的仓库总说明把这些内容定位为供数学共同体理解、检验的原始研究材料；它没有把上传代码等同于完成同行评审。复杂性理论学者Ryan Williams称之为“声称的反证”，并表示将与ETH提出者Russell Impagliazzo、Ramamohan Paturi组织公开、独立的检验。截至本文发布时，未见他们宣布最终核验结论。[1][3][5]
论文声称做到了哪一步
论文的定理1.1针对每个固定的 k≥2，处理有 n 个变量、m 个子句的 k-CNF 公式。它给出的确定性算法可以精确计算满足赋值数，时间为 (n+m)^{O_k(1)}·2^{O_k(n log log n/√log n)}，所需空间是 (n+m)^{O_k(1)} 比特。若子句数满足 m≤Dn 且D固定，论文给出更强的 (n+m)^{O_{k,D}(1)}·2^{O_{k,D}(n/√log n)} 时间界。[2]
这串符号里最要紧的是 n/√log n 相对于 n 越来越小；前一个带 log log n 的式子同样是 o(n)。在把输入规模的多项式因子单独列明后，两个结果都给出次指数的参数依赖。计数比只判断“是否有解”信息更多：把计算结果与零比较，就能判定SAT。取 k=3，若定理正确，ETH要求的“3-SAT没有次指数时间算法”便与它直接冲突。[2]
论文还讨论了稀疏化、共享的线性摘要、低次数表达与插值，并在附录中给出改进时间界的张量收缩步骤。这不是把现有求解器参数调得更快几倍，而是针对最坏情形的渐近上界提出新算法。对于规模有限的工业实例，式子里隐藏的常数、实现代价以及既有SAT求解器的工程优化，仍决定实际运行速度；论文没有因此宣布现成软件会立刻提速。[2]
Lean证明能回答什么，暂时不能回答什么
形式化证明提高了检查的可重复性，但检查者仍要确认：机器证明的命题与公众理解的数学断言是不是同一件事，编码、渐近参数、空间模型和前提条件是否完整。项目的形式化范围说明明确写出，Lean覆盖了固定宽度公式的一个较弱但仍然次指数的时间界：(L+1)^{O_k(1)}·2^{O_k(n(log log n)^2/√log n)}，其中L是输入编码长度；它没有宣称已形式化PDF中的最强时间界。[2][6]
两种界的区别值得认真看。若较弱的形式化结论及其与3-SAT的对应关系经检查无误，单是“次指数”这一性质就足以触及ETH；PDF更强的定量界仍须按其自身证明核对。仓库有供比较器补全的挑战接口，看到某个接口文件中的待填证明标记，也不能直接判断整个项目的形式化成果无效。反过来，发布方说“已形式化”，也无法替代外部专家独立复核具体代码和数学陈述。[2][6]
如果成立，冲击会落在哪里
第一层是复杂性理论的条件性结果。固定k包含3，因此论文的主张直接针对ETH；论文还指出其精确计数算法会冲击#ETH，并连带触及SETH、Gap-ETH、NSETH等相关假设的相应表述。研究者接下来要逐篇检查：哪些下界只依赖这些假设，哪些仍有其他证明；涉及随机化、近似或不同参数的结论，也要分清适用范围。[2]
第二层是科研方法。OpenAI称模型在很短时间内提出自然语言论证，并给出可机读的形式化材料。它若通过审查，AI参与数学发现的案例会多一个分量很重、同时也极易被反复检查的实例。若审查发现错误，公开的论文、修订记录和形式化边界同样有研究价值：问题究竟出在算法、复杂度估算，还是自然语言结论与机器命题之间的接口。公开审查的价值就在于能把这些问题逐一落到具体证明上。[1][2][5][6]
第三层是技术产业的预期管理。SAT求解器用于芯片验证、排程、软件检查等任务，理论突破自然会引来应用想象。但次指数时间不是多项式时间，渐近上界不承诺现实输入下比现有求解器快。一般NP问题虽然可能通过多项式归约转成SAT，归约后的变量数也可能大幅增加，不能由此宣布“所有NP问题都有次指数算法”。这篇论文尤其没有证明 P=NP。[2][4]
眼下最值得盯的，是独立复核提出的具体问题：定理的输入编码与参数是否对应，稀疏化和计数步骤是否保留要求的界，Lean证明覆盖了哪一版结论，以及后续修订是否改变主张。10月25日的预印本把一个长期开放的问题摆到了可公开检验的位置；它可能成为复杂性理论的大事，前提是证明经得起这样的逐行审查。[2][3][6]
参考资料
[1] OpenAI，Building scientific understanding with academic communities，2026-10-26：原文
[2] OpenAI，The Exponential Time Hypothesis is False，预印本，2026-10-17，2026-10-25修订：PDF
[3] Ryan Williams，关于组织公开独立检验的声明，2026-10-26：原帖
[4] Impagliazzo、Paturi，On the Complexity of k-SAT，Journal of Computer and System Sciences 62(2)，2001：论文信息
[5] OpenAI Math 仓库及单篇说明：仓库 · 预印本说明
[6] OpenAI Math，Lean形式化范围说明：原文