【标题】OpenAI 预印本声称证伪计算复杂性基石 ETH：数学研究正在进入“形式化验证”的信任博弈
【摘要】OpenAI 发布预印本挑战计算复杂性基石指数时间假设，但这一依赖 Lean 形式化验证的结论目前仍包含占位符，其学术权威性正处于未闭环的特殊阶段。
【正文】
2026 年 10 月 25 日，OpenAI 在其 GitHub openai/math 仓库发布了一篇标题为《The Exponential Time Hypothesis Is False》的预印本。论文声称找到了一种确定性的子指数时间算法，能够解决固定子句长度的 k-SAT 问题。如果这一结论成立，意味着计算复杂性理论中极其重要的指数时间假设（ETH）将正式被证伪。
对于长期依赖 ETH 作为下界证明前提的复杂性理论研究员而言，这是一次突如其来的震动。ETH 由 Russell Impagliazzo 和 Ramamohan Paturi 提出，长期以来被视为确定许多算法求解难度下界的地基。OpenAI 此次提出的算法运行时间为 $(n+m)^{O_k(1)} \cdot 2^{O_k(n \log\log n / \sqrt{\log n})}$，在 $n$ 趋于无穷时属于 $2^{o(n)}$。这意味着，求解这些问题的难度并非传统认为的纯指数级。
复杂性理论的基石为何动摇
在计算复杂性理论中，ETH 假设 3-SAT 问题不存在 $2^{o(n)}$ 的算法，即求解难度至少是指数级的。它是现代密码学和算法分析中许多证明的逻辑起点。一旦 ETH 失效，基于该假设导出的成百上千个算法复杂度下界将瞬间失去支撑，研究人员必须重新审视这些问题的理论难度。
然而，需要厘清的一个核心认知是：ETH 被证伪并不等同于 P=NP。
即使该算法被证实有效，它仅仅证明了某些 NP 完全问题的求解难度低于单纯的指数级，并不代表这些问题可以在多项式时间内解决（即 P=NP）。这就像是在原本坚固的指数级高墙上钻开了一个洞，但这堵墙依然远未倒塌到多项式的平原上。
信任危机的遗留与形式化验证的悖论
OpenAI 在数学项目上的信誉，目前正处于一个微妙的信用修复期。就在 2026 年 10 月 7 日，该仓库曾批量撤回了 3 篇预印本论文，理由是代数符号处理中的错误。这一次，为了避免重蹈覆辙，OpenAI 采取了 Lean 形式化验证与专家背书的组合策略。
然而，这种做法引入了新的信任悖论。虽然 Lean 作为形式化证明工具，理论上可以消除逻辑漏洞，但该仓库 ComparatorChallenges 目录下的 Lean 代码中依然残留着 sorry 占位符。在形式化社区中，sorry 意味着该部分逻辑尚未通过机器验证，是一个显性的待办标记。
这意味着，虽然这篇论文在形式逻辑的框架下发布，但其核心逻辑闭环尚未完全由机器签署。这种未完成的发布方式，与传统学术期刊严格的审稿流程形成了鲜明对比。
- 风险.目前的 Lean 验证版本与手稿本身在运行时间界限上存在细微差异，这表明机器验证并非简单的复刻原文，而是可能暴露原文中的逻辑鸿沟。
从同行评审到机器证明的范式阵痛
此次验证由 Russell Impagliazzo、Ramamohan Paturi 和 Ryan Williams 组成的外部专家小组负责，这实际上是 OpenAI 在尝试建立一套全新的学术评审范式：AI 生成证明、机器形式化验证与顶级专家二次确认。
对于算法工程师和科研人员来说，最现实的问题不在于 ETH 是否真被证伪，而在于这套范式本身是否可靠。传统数学依靠社区的长期阅读与复现，而 OpenAI 正在试图将这一过程压缩并数字化。
在最终确认结果之前，外界保持怀疑是合理的常态。OpenAI 并非在试图单方面宣布真理，而是在测试这个数学共同体对机器辅助数学的容忍度边界。如果 ETH 的证伪在这些代码的 sorry 被填补后依然成立，这不仅是理论的一大进步，也将标志着数学论文的生产力工具正式跨入了机器验证时代。
- 提醒.该算法在实践中是否真能达到理论上的子指数效率，目前仍需等待更多基准测试与代码逻辑的完善，不要将其直接视为工程可用的算法跃迁。
【锐评】数学终究是逻辑的严丝合缝，而非算力的暴力试错。在机器证明的边界完全闭合前，学术界的审慎质疑本身就是同行评审的一部分。