ETH 死了。OpenAI 一夜之间证伪了三十年共识，顺手摸到了千禧年难题

10 月 26 日，OpenAI 发了一篇公告。我花了一整天把它挂出来的两篇论文、两套 Lean 形式化、外加千禧年难题的官方陈述全部读完，现在可以负责任地说：这是 AI 科学史上目前分量最重的一次发布，没有之一。

公告标题起得很克制，叫《与学术社区合作构建科学理解》。内容一点不克制，一口气宣布三个结果：

· 调和分析：证明了 Sogge 1991 年提出的局部光滑化猜想，全部维度。顺手收割 Kakeya 猜想、Bochner–Riesz 猜想、Stein 限制猜想；
· 计算机科学：证明了指数时间假设（ETH）为假。注意，不是解决 P vs NP，是把整个细粒度复杂性领域当作地基用了三十年的那条假设证伪了；
· 理论物理：给出了包含规范场和费米子的四维相互作用量子场论（包括 QCD）的严格存在性证明，其中纯 Yang–Mills 的存在性是千禧年难题的组成部分。

三个结果，两个已经完整公开（论文＋Lean 机器证明），一个被物理学家小组按住不发。这篇把三条线全部扒开，包括那些 OpenAI 自己没说出口的东西。

一、先看时间线，节奏比结果更吓人

把公告里散落各处的日期拼起来，会得到一条非常诡异的流水线：

· 9 月 9 日：模型产出 Yang–Mills 存在性的自然语言证明；
· 9 月 18 日：产出 QCD 存在性证明；
· 10 月 16 日：Yang–Mills 的 Lean 形式化完成；同一天，ETH 的反例算法拿到自然语言证明；
· 10 月 17 日：ETH 结果 Lean 形式化完成（论文页脚写的日期就是这一天，10 月 25 日修订）；
· 10 月 18 日：局部光滑化猜想证明产出；
· 10 月 19 日：局部光滑化 Lean 形式化完成；
· 10 月 26 日：公告发布。

也就是说，两个公开结果的"猜想被证明"到"机器逐行检查通过"只隔一天；连最重的 Yang–Mills，从自然语言证明到形式化完成也只用了五周——这个量级的工作，人类团队形式化往往以年计。以前数学界对 Lean 的抱怨是形式化成本太高，一个非平凡定理要几个博士生干一年。现在是：AI 证明，AI 第二天形式化，人类只负责读。

还有个背景数字。承载这一切的 GitHub 仓库 openai/math 是 10 月 6 日才建的，README 里写着：目前目录里有 721 份手稿、373 个结果家族，约 42% 的主要结果已完成 Lean 形式化，Lean 文件五万多个。这次公告的三个结果，只是这个仓库浮出水面的冰山尖。

二、局部光滑化：波不能永远聚着

▲ 59 页论文《Local smoothing for the Euclidean wave equation》，OpenAI 署名，2026 年 10 月 25 日（图源：openai/math 仓库）

先解释这个猜想到底在说什么。一列从四面八方汇聚的波，在焦点处可以聚出一个比初始能量大得多的尖峰——想象放大镜聚光。Sogge 在 1991 年问：这种极端聚焦能持续多久？他的猜想说：很短。在时间上平均之后，聚焦带来的损失可以被初始数据的少量导数完全控制，需要的导数阶数是精确的 s+(p) = max(0, (n−1)/2 − n/p)，一步都不能少。

这个问题四十年间养活了调和分析的半壁江山。Bourgain、Wolff、Tao、Guth、Demeter……一串如雷贯耳的名字都在它边上留过迹。二维情形是 Guth–Wang–Zhang 2019 年拿下的；2025 年 Wang–Zahl 证明了三维 Kakeya 猜想，当时被算作菲尔兹奖级工作。而这篇论文直接宣布：所有维度 n≥2，全部解决。

更狠的是推论链。论文摘要列出的收割名单：Bochner–Riesz 猜想（全部 p 和 α 的猜测范围）、Stein 平方函数尖锐界、球面/抛物面/截锥的 Fourier 限制估计（整个内部区域）、Schrödinger 方程局部光滑化、Kakeya 与 Nikodym 极大猜想——最后这条意味着每个欧氏 Kakeya 集的 Hausdorff 维数都等于 n，所有维度。2025 年人类数学家的巅峰结果，在这篇论文里只是一行推论。

方法呢？公告里只有一句"基于一个新颖的辅助偏微分方程"，论文里才看得全：把波沿光线方向做虚平移，让不同方向的模态被高斯权重筛开；用对称双曲系统的通量造出一个正半定的守恒张量；然后在每条纤维上解一个四元数 Hermitian 行列式方程（Monge–Ampère 型），借 Aubin–Mabuchi 能量做修正项；最后靠"两个圆"的调和分析把信息从观测时刻传回初始时刻——每传一次损失一个对数，一共损失两次，所以临界频率环带上的估计里出现 log² 因子。

说实话，这套组合拳里每一件兵器都是别的领域的经典（补偿紧性、Monge–Ampère、Aubin–Mabuchi），把它们焊成一台能打通任意维度的机器，这个"缝合"本身就是创新。人类数学家在这个方向上试了三十多年的路线是解耦、波包分解、归纳尺度——没有人试过从虚平移加行列式方程这个方向进攻。

三、ETH 死了：证伪一条假设，比证明一条定理更炸

▲ 67 页论文《THE EXPONENTIAL TIME HYPOTHESIS IS FALSE》，标题就是结论（图源：openai/math 仓库）

ETH 是什么？2001 年，Impagliazzo、Paturi 和 Zane 提出：3-SAT 这种问题，n 个变量的布尔公式，最坏情况下任何确定性算法都得花 2^Ω(n) 时间——指数级，一个变量都省不掉。它比 P≠NP 弱得多，所以安全得多，三十年来成了算法复杂性研究的通用地基：几百篇论文的结构都是"假设 ETH，则问题 X 不存在更快的算法"。你熟悉的很多"这个问题已经最优了"，底下垫的都是它。

论文的定理 1.1 说：对每个固定的 k≥2，存在确定性算法，精确数出 k-CNF 的满足赋值个数，时间只要

(n+m)^O(1) · 2^{O(n·log log n/√log n)}

空间只要多项式。这个指数是 2^o(n)——比任何 2^cn 都小，不管 c 多小。ETH 当场死亡。而且死的不止它一个：论文 1.1 节明确列出，同一个定理顺手带走了 SETH（更强的版本）、Gap-ETH（近似版本）、NSETH（非确定版本）、#ETH（计数版本），连它们的随机化变体一起埋了。

算法思路有趣在哪？它不是枚举，是插值。把每个子句的多项式里的变量偷偷替换成"共享线性摘要"的组合——固定住少数几个测量值之后，整个 2ⁿ 的巨大和式分解成小组独立求和；然后在参数 T=0,1,…,Q 上做多项式插值，从一堆"容易算的变形版本"里把原始计数 H(0) 反解出来。变形用的低次多项式怎么构造？靠一个秩受限的辅助矩阵 M₀，而 M₀ 的性质又是通过在短区间上插值 (−1)ʲ 得到的。中间还塞了 Tanner 码奇偶检验、稀疏化引理、条件期望去随机化。代数方法在 SAT 上轰出 2^o(n)，这个组合的想象力浓度相当高。

但必须泼的冷水，论文自己都写了，我逐条搬过来：

· 这不等于 P=NP。2^o(n) 仍然是超多项式时间，2^√n 级别的算法照样打不开RSA；
· 理论速度 ≠ 实际速度。公告原话："把理论进展变成实际改进，需要大量后续研究。"前置常数 (n+m)^O_k(1) 里的指数天知道多大；
· 下游塌了一部分，没全塌。很多基于 SETH 的下界其实只依赖更弱的假设（比如正交向量猜想 OVC），那些还活着。论文 1.1.3 节自己盘点了哪些结论失去地基、哪些只是搬家；
· 2^o(n) 不向一般归约传递——论文脚注明确警告，别急着给别的下界判死刑。

顺带一提，论文推论 1.4 还白送了一个无条件电路下界：存在 ENP 中的语言，其电路规模在无穷多个 n 上超过 c·n/√log n。Williams 2016 年用 MA-SETH 被否（MA-SETH 是他自己否的）换来的那类"算法→下界"结果，这次是同一枚硬币的另一面。

四、Yang–Mills：最大的结果，最克制的发布

▲ Jaffe–Witten 撰写的千禧年问题官方陈述第 3 页，质量间隙、夸克禁闭、手征对称性破缺三大要求（图源：Clay 数学研究所）

这条线的措辞需要逐字读，因为它是三者中最容易被写错的。公告的原话：给出了"四维中包含规范场与费米子的若干相互作用量子场论——包括 QCD 和标准模型的一个统一完备化——的严格存在性证明"，并且"作为一个子问题，这项工作还包括纯 Yang–Mills 理论存在性的证明，它是千禧年难题 Quantum Yang–Mills Theory 的组成部分"。

注意"组成部分"四个字。对照 Jaffe–Witten 的官方陈述，千禧年难题要求两件事：一是按 Wightman 公理严格构造量子 Yang–Mills 理论，二是证明质量间隙（谱从 0 以上某个 Δ 才开始）。这次宣布的是存在性。质量间隙有没有一起解决？公告没说，论文也没放出来。所以"OpenAI 拿下千禧年难题"这个标题现在还不能写，能写的是：人类第一次有了四维非阿贝尔规范场论的严格存在性证明——这本身就够物理学家和数学家开十年研讨会了。

技术上这条路不是横空出世：公告明说工作建立在 Balaban 的方案之上。Thomas Balaban 从 1980 年代起用十几篇长文死磕格点规范场的紫外问题，是constructive QFT 几十年里最硬的一条路，但从未走完。如果 AI 真把 Balaban 程序推到终点，那等于人类数学家长期积累的一条"未竟路线"被接管完成了——这个模式（在巨人没走完的地方走完）和局部光滑化那条全新路线正好是两种极端。

最有意思的是发布策略。物理这条线，OpenAI 说：材料不给。交给 David Gross 牵头的小组（成员 Douglas、Jaffe、Klebanov、Nekrasov——清一色这个领域的顶级人物，Gross 因 1973 年渐近自由工作拿过 2004 年诺贝尔奖，Jaffe 本人就是千禧年难题的出题人），由他们自己组织写作和发布。出题人来审这道题，这个安排本身就说明 OpenAI 知道这个结果有多容易被误读。

五、别信 AI，让机器先过一遍

▲ Lean 挑战文件里的定理陈述（节选）：注意结尾的 sorry——这是留给解题者的靶子（图源：openai/math 仓库 ComparatorChallenges/LocalSmoothing.lean）

两个公开结果都带 Lean 形式化，而这套东西的设计比结果本身还讲究。仓库里有个 ComparatorChallenges 目录，玩法是：先放出一份"挑战文件"，把定理逐字写成 Lean 陈述，结尾挂 sorry——比如局部光滑化的那份，六个目标一次列出：欧氏局部光滑、Bochner–Riesz 一致界、球面限制、Kakeya 极大、Kakeya 集满维数、Stein 平方函数，全是独立陈述、不借任何自定义漏洞；然后解题方（这里是 OpenAI 的模型）交上完整证明。任何人 clone 仓库跑一遍编译，机器就告诉你证没证对。

审计口径也干净：两个形式化的 JSON 元数据里，允许使用的公理只有 Lean 的标准三件套（propext、Quot.sound、Classical.choice），没有塞任何新公理。ETH 那份形式化甚至把"图灵机"写进了定理——声明存在一台确定性机器，在亚指数时间、且每一步累计访问的纸带格子只有多项式个的条件下，精确数出满足赋值。把"空间多项式"翻译成"访问格子数有界"，这是把复杂性论断钉死到最机械的定义上。

当然，"Lean 验证通过"≠"没有争议"。机器只保证证明在形式系统里成立，定理陈述是不是数学家想问的那个问题，机器管不了——这正是 Comparator 把陈述和证明分开放的原因：陈述是公开标靶，谁觉得 OpenAI 偷换了定义，可以直接对着挑战文件抬杠。

六、让提出 ETH 的人，审判 ETH 的死

公告里最见情商的一笔在这：ETH 验证小组的负责人是 Impagliazzo、Paturi 和 Ryan Williams。前两位就是 2001 年提出 ETH 的人——亲手写下假设的人来审判假设的死亡。Williams 则是三十年来最会"否假设"的复杂性理论家，他 2016 年证伪过 MA-SETH，还建立了算法与下界之间的桥梁。让最懂这条假设、也最会拆这条假设的人来拆，这个安排很难挑出毛病。

小组提了两个条件，OpenAI 全答应：原始数据全部公开供社区独立检验；OpenAI 出资办一场会议，专门讨论这件事对整个领域的影响。再加上 10 月 6 日那批结果发布时已经宣布过的向 Simons 基金会捐赠 500 万美元，专门支持学者研究 AI 产出的成果。

发布策略本身也被当成实验做。三个结果三种打法：数学直接放，让研究者自己组织消化；CS 放原始数据＋外部小组讲解；物理按住，全权交给专家小组。公告承认"我们还不知道哪种方式最有用"，并列出四条原则：透明（不签保密协议）、不占学术署名、给解释者以荣誉、参与者独立且无薪。

README 里还有一句话值得单独摘出来："在我们看来，这些手稿最好被理解为一种原始研究数据，而不是打磨过的学术论文。关于署名、优先权和并行工作，我们完全听从数学界。"——一家公司把"我们可能抢了别人正在做的题"写进仓库首页，姿态是新的。

七、我的几点想法

1. 三个结果不是三场胜利，是一条流水线。9 月 9 日到 10 月 19 日，四十天里横跨三个领域，自然语言证明到机器验证最短只隔一天。单点突破可以归功灵感，这种吞吐率只能归功系统。真正该被讨论的是：当一个系统能同时在调和分析、复杂性、量子场论里产出可验证结果时，"AI 辅助数学"这个词已经不准确了，这是 AI 在做数学，人类在做验收。

2. 证伪比证明更危险，也更诚实。ETH 之死提醒所有人：我们有多少"已知最优"是建在一条没人验证过的假设上的。好消息是这次有 Lean——形式化第一次成了对抗"AI 幻觉质疑"的硬通货。坏消息是质量间隙这种"陈述是否切题"的问题，机器依然帮不上忙。

3. 物理那条线请按暂停键看。存在性≠千禧年难题攻克，这是全文我写得最大声的一句。等 Gross 小组的材料放出来之前，任何"AI 解决黎曼之后的下一个千年难题"的标题都是抢跑。

4. 学术界的反应才是真正的实验。Impagliazzo 小组、Gross 小组、500 万美元、三种发布策略——OpenAI 实际上在公开测试"科学共同体如何消化非人类产出的知识"。这个测试没有标准答案，但它一定会被写进科学社会学的教科书。

5. 对我们这种靠读论文为生的人，最直接的冲击是那个 721 份手稿的仓库：42% 已形式化，剩下 58% 连 Lean 都还没过。今天公告的三个结果，可能只是它家底里最不经挑的那几件。

最后说点丧的：局部光滑化论文 59 页，ETH 论文 67 页，我确认自己只真正读懂了其中一小部分。机器验证给了"对"的保证，但"理解"这件事，接下来几年还得靠人类数学家一行一行往回啃。OpenAI 在公告里用的词就很准——这些是原始研究数据。从数据到理解，中间隔着的那段路，才是接下来所有论文、研讨会和职业生涯的所在地。

参考来源：
1. OpenAI, Working with academic communities to build scientific understanding, 2026-10-26
2. OpenAI, Local smoothing for the Euclidean wave equation (preprint, 59pp), 2026-10-25
3. OpenAI, The Exponential Time Hypothesis is False (preprint, 67pp), 2026-10-17/25
4. openai/math 仓库：README、lean/docs/079.md、lean/docs/378.md、ComparatorChallenges、formalization.yaml
5. Jaffe & Witten, Quantum Yang–Mills Theory（Clay 数学研究所千禧年问题官方陈述）