复杂度理论里被引用最多的「垫脚石」之一,被一个还没发布的模型动了。10 月 26 日,OpenAI 向开源仓库 openai/math 提交了预印本《The Exponential Time Hypothesis is False》和配套 Lean 证明:其内部模型构造出确定性算法,能在亚指数时间和多项式空间里精确计数固定宽度 CNF 公式的满足赋值,其中 3-SAT 情形直接反驳指数时间假设(ETH)。预印本尚未经过同行评审,也还没有第三方确认。
这个假设撑起无数下界
ETH 是 1999 年提出的复杂性猜想,刻画布尔可满足性问题的求解难度:它断言 3-SAT 这类问题不存在亚指数时间算法,是大量计算复杂性下界的推理起点。用媒体的话说,数百篇计算机科学论文直接建立在它之上。ETH 若倒下,一整批「在 ETH 假设下」导出的下界结论都得重新排队。
手稿全部出自内部模型
openai/math 不是普通的论文集。README 写明:全部手稿与证明构件出自一个未公开的 OpenAI 内部模型——既有数学评测饱和后,公司开始拿开放研究问题当考题,平均每个结果消耗约 3 小时的 ChatGPT Pro 档思考算力,整个评估累计抛出约 4,000 道题。目录现有 721 篇手稿、归入 373 个族,约 42%(300/719)的顶层结论已配 Lean 形式化;仓库以 Apache-2.0 协议开源,已收获约 1.59 万 star。OpenAI 对定位很克制:这些手稿是「原始研究数据」而非打磨过的论文,未形式化的结果可能有问题,部分成果建立在此前模型输出之上。这次与 ETH 同批新增的,还有证明 Sogge 局部平滑估计的手稿,它顺带导出 Kakeya 极大函数与维度猜想、Stein 球面限制估计等结论;仓库同时放出 10 个结果族的模型推理摘要,包括 π 的无理性指数、Mahler 猜想等。
谁来验,怎么验
验证安排是这个事件最有意思的部分。更新日志写明:由 Russell Impagliazzo、Ramamohan Paturi、Ryan Williams 领衔的独立计算机科学家工作组将审查并解读这份证明,材料是应工作组要求立即公开的。这个仓库自己也带着纠错记录:10 月 7 日,一处符号错误让 3 篇手稿被撤回、14 篇被修订——流程会出错,但在公开版本历史里纠错。另一边,陶哲轩本月早些时候在 UCLA 研讨会上公开批评 OpenAI 急于发布数学成果的做法,认为这暴露了真实意图,双方已经没有建设性合作的可能。
所以呢
比起「AI 证伪大猜想」的标题,更值得注意的是验证流程的重构:Lean 让「机器写、机器查」成为可能,但一条战略级结论的最终成立,仍然要 Impagliazzo 这个量级的工作组来背书。当发现的产能变成算力问题,数学的瓶颈整体移向验证侧——这比任何单一结论都更像范式信号。下次再刷到「某猜想被 AI 推翻」,先问一句:证明,谁验的?