ETH 被证伪了几百篇论文的「条件性下界」地基突然没了2026 年 10 月 26 日OpenAI 公布了三项由内部模型产出的结果。数学那项局部光滑猜想 / Kakeya很炸物理那项被合作组压着没放但真正会让做算法的人后背发凉的是中间那项指数时间假设ETH被推翻了而且已经在 Lean 里形式化通过。先说结论避免误读ETH 为假 ≠ P NP。这两件事差得很远。但它足以让过去二十年里一大批在 ETH 成立的前提下这个问题不可能更快的结论失去前提。这次和以往AI 说自己证了个定理最大的区别是Lean 证明是公开的可以自己跑。一、时间线从自然语言证明到 Lean 只隔了一天按 OpenAI 公告里的说法10 月 16 日模型产出 ETH 为假的自然语言证明。10 月 17 日形式化到 Lean通过。10 月 25 日自然语言 writeup 与 Lean 证明一起公开在openai/math仓库。合作组由Russell Impagliazzo、Ramamohan PaturiUCSD和 Ryan WilliamsMIT牵头。这三个人不是随便找的审稿人。Impagliazzo 和 Paturi 就是 ETH 的提出者连同 Francis Zane2001 年那篇 JCSSWilliams 这些年一直在做 ETH 的强版本、以及用 ETH 推下界。让假设的提出者来主持对假设的推翻这个安排本身就是这次公告里最值得学的一点。有一句容易被忽略但很关键合作组要求 OpenAI公开全部原始数据并出资办一场会议来讨论这件事对整个领域的意义。也就是说他们自己也没打算让这件事停在一篇 PDF 上。二、ETH 到底是什么凭什么是地基形式化地说ETH 断言3-SAT 不存在 $2^{o(n)}$ 时间的算法。其中 $n$ 是变量个数。换句话说最坏情况下你不可能做到比每个变量指数级更好——注意它说的不是多项式是次指数都不行。它之所以是地基不是因为大家关心 3-SAT 本身而是因为它是条件性下界conditional lower bound的通用货币。逻辑长这样若 ETH 成立 ⇒ 3-SAT 需要 2^Ω(n) ⇒ 通过归约问题 X 需要 n^(2-ε) 时间 ⇒ X 不存在真正亚二次的算法除非 ETH 假这条流水线支撑了几百篇论文覆盖图论、计算生物、数据库、计算几何。你在工程里听到的那些这个问题理论上做不到更快很多都是这么来的——它们从来不是被证明的是被条件出来的。细粒度复杂度fine-grained complexity这一整片领域基本就是靠这条流水线吃饭。三、地震震在哪不是算法立刻变快是不可能失效这里必须把两件事分开第一层理论上的不可能没了。那些写着assuming ETH, no $O(n^{2-\epsilon})$ algorithm exists的结论前提被抽掉了。它们不会自动变成存在快速算法但它们不再能阻止别人去找。学术上这叫结论变空vacuous。第二层工程上的别费劲了没了。这才是对做业务的人有影响的。过去你说这个 join 顺序优化理论上没戏、这个近似算法不可能再快一个量级背后可能挂着一篇 2015 年的 ETH-based 下界。现在那句话的效力降级为在旧假设下成立。但请注意——没有任何现成算法因此变快。ETH 被推翻意味着存在次指数算法可那个算法没有被构造出来也不知道常数多大、能不能落地。公告自己也写了把这些理论进展变成实际改进需要大量后续研究。四、它不意味着什么这一段比前面都重要写这类文章最容易犯的错是把ETH 假讲成P NP或者NP 难题都能解了。都不是。1. ETH 为假只说明 3-SAT 可以亚指数。$2^{o(n)}$ 依然是指数级的敌人。$2^{n/\log n}$ 也是 $2^{o(n)}$。它离多项式还隔着一条鸿沟。P vs NP 一点没动。2. SETH 也跟着倒了但跟着倒不等于变简单。强指数时间假设SETH蕴含 ETH所以 ETH 假 ⇒ SETH 假。逻辑上没毛病但同样地这不构成任何构造性收获。3. 已经证明的无条件下界不受影响。凡是真·无条件证明的比如时间层级定理、某些电路下界该成立还成立。倒的只是条件那部分。4. 已经跑得很快的工程实践不受影响。你的 B 树不会因为 ETH 挂了就变慢也不会变快。五、Lean 那一步才是这次真正的分水岭如果只有自然语言证明这件事最多是一条争议新闻领域外的人没法判断领域内的人要花几个月吵。但 Lean 证明公开在openai/math的lean/docs/378.md这意味着验证从相信权威变成了跑一遍。这是过去两年 AI 数学公告里最重要的模式转变自然语言 writeup给人读的可能有 gap。Lean 形式化给机器检查的gap 会被编译器抓住。两者一起放读得懂的人读 writeup读不懂的人验 Lean。对工程师的启示其实很直接AI 产出的东西如何被信任这个问题答案正在从审查文本变成审查可执行的证明对象。这个模式会溢出到数学之外——配置、协议、调度策略凡是能形式化的东西未来都会有Lean 等价物。我甚至觉得这条流程比 ETH 本身更值得抄进团队规范产出一个结论 → 用机器可检验的形式重述 → 再交给人判断有没有意义。三层分离每层都能被不同的人独立检查。六、实操建议接下来该做什么给三类人三种动作。如果你是做算法/数据库/图计算的去翻你依赖的那些下界论文看看有几条挂着assuming ETH。把它们列出来标注前提待重估。不用删但别再拿它们当这条路走不通的挡箭牌。这周就值得做一次因为这是你手上少有的、成本极低的信息更新。如果你是写基础设施/做性能优化的短期内什么都别改。中期值得盯的是那场会议和后续论文——如果真有人把次指数 SAT 算法压到能跑的常数SAT 求解器、约束求解、程序验证工具链会先被冲一遍。如果你是关注 AI for Science 的重点看的不是AI 又证了一个定理而是三个流程细节原始数据是否公开、形式化是否独立、提出假设的人是否参与了验证。这次的答案分别是是、是、是。这三个是以后判断同类新闻真假的筛子。七、最后一句实话这件事最反直觉的地方在于一个被信了二十五年的假设可能是错的而推翻它的东西只花了一天做形式化。这不代表数学变简单了也不代表人类专家多余了——Impagliazzo 他们的角色不是盖章是决定这个结果该怎么被社会消化。真正稀缺的从来不是证明是判断哪个证明值得被认真对待。而这一次判断权还在人手里。这大概是目前最让人安心的一点。参考OpenAI: Working with academic communities to build scientific understanding2026-10-26openai/math仓库ETH writeup PDF 与lean/docs/378.mdImpagliazzo, Paturi, Zane,Which Problems Have Strongly Exponential Complexity?, JCSS 2001注本文基于 OpenAI 公告与合作组公开材料整理。Lean 证明虽已公开但完整独立复核仍在进行中涉及具体技术细节的结论请以原始 writeup 为准。 
长河君 · 2026/10/29 2:17:39 · 阅读 1.2k ETH 被证伪了：几百篇论文的「条件性下界」，地基突然没了
ETH 被证伪了几百篇论文的「条件性下界」地基突然没了2026 年 10 月 26 日OpenAI 公布了三项由内部模型产出的结果。数学那项局部光滑猜想 / Kakeya很炸物理那项被合作组压着没放但真正会让做算法的人后背发凉的是中间那项指数时间假设ETH被推翻了而且已经在 Lean 里形式化通过。先说结论避免误读ETH 为假 ≠ P NP。这两件事差得很远。但它足以让过去二十年里一大批在 ETH 成立的前提下这个问题不可能更快的结论失去前提。这次和以往AI 说自己证了个定理最大的区别是Lean 证明是公开的可以自己跑。一、时间线从自然语言证明到 Lean 只隔了一天按 OpenAI 公告里的说法10 月 16 日模型产出 ETH 为假的自然语言证明。10 月 17 日形式化到 Lean通过。10 月 25 日自然语言 writeup 与 Lean 证明一起公开在openai/math仓库。合作组由Russell Impagliazzo、Ramamohan PaturiUCSD和 Ryan WilliamsMIT牵头。这三个人不是随便找的审稿人。Impagliazzo 和 Paturi 就是 ETH 的提出者连同 Francis Zane2001 年那篇 JCSSWilliams 这些年一直在做 ETH 的强版本、以及用 ETH 推下界。让假设的提出者来主持对假设的推翻这个安排本身就是这次公告里最值得学的一点。有一句容易被忽略但很关键合作组要求 OpenAI公开全部原始数据并出资办一场会议来讨论这件事对整个领域的意义。也就是说他们自己也没打算让这件事停在一篇 PDF 上。二、ETH 到底是什么凭什么是地基形式化地说ETH 断言3-SAT 不存在 $2^{o(n)}$ 时间的算法。其中 $n$ 是变量个数。换句话说最坏情况下你不可能做到比每个变量指数级更好——注意它说的不是多项式是次指数都不行。它之所以是地基不是因为大家关心 3-SAT 本身而是因为它是条件性下界conditional lower bound的通用货币。逻辑长这样若 ETH 成立 ⇒ 3-SAT 需要 2^Ω(n) ⇒ 通过归约问题 X 需要 n^(2-ε) 时间 ⇒ X 不存在真正亚二次的算法除非 ETH 假这条流水线支撑了几百篇论文覆盖图论、计算生物、数据库、计算几何。你在工程里听到的那些这个问题理论上做不到更快很多都是这么来的——它们从来不是被证明的是被条件出来的。细粒度复杂度fine-grained complexity这一整片领域基本就是靠这条流水线吃饭。三、地震震在哪不是算法立刻变快是不可能失效这里必须把两件事分开第一层理论上的不可能没了。那些写着assuming ETH, no $O(n^{2-\epsilon})$ algorithm exists的结论前提被抽掉了。它们不会自动变成存在快速算法但它们不再能阻止别人去找。学术上这叫结论变空vacuous。第二层工程上的别费劲了没了。这才是对做业务的人有影响的。过去你说这个 join 顺序优化理论上没戏、这个近似算法不可能再快一个量级背后可能挂着一篇 2015 年的 ETH-based 下界。现在那句话的效力降级为在旧假设下成立。但请注意——没有任何现成算法因此变快。ETH 被推翻意味着存在次指数算法可那个算法没有被构造出来也不知道常数多大、能不能落地。公告自己也写了把这些理论进展变成实际改进需要大量后续研究。四、它不意味着什么这一段比前面都重要写这类文章最容易犯的错是把ETH 假讲成P NP或者NP 难题都能解了。都不是。1. ETH 为假只说明 3-SAT 可以亚指数。$2^{o(n)}$ 依然是指数级的敌人。$2^{n/\log n}$ 也是 $2^{o(n)}$。它离多项式还隔着一条鸿沟。P vs NP 一点没动。2. SETH 也跟着倒了但跟着倒不等于变简单。强指数时间假设SETH蕴含 ETH所以 ETH 假 ⇒ SETH 假。逻辑上没毛病但同样地这不构成任何构造性收获。3. 已经证明的无条件下界不受影响。凡是真·无条件证明的比如时间层级定理、某些电路下界该成立还成立。倒的只是条件那部分。4. 已经跑得很快的工程实践不受影响。你的 B 树不会因为 ETH 挂了就变慢也不会变快。五、Lean 那一步才是这次真正的分水岭如果只有自然语言证明这件事最多是一条争议新闻领域外的人没法判断领域内的人要花几个月吵。但 Lean 证明公开在openai/math的lean/docs/378.md这意味着验证从相信权威变成了跑一遍。这是过去两年 AI 数学公告里最重要的模式转变自然语言 writeup给人读的可能有 gap。Lean 形式化给机器检查的gap 会被编译器抓住。两者一起放读得懂的人读 writeup读不懂的人验 Lean。对工程师的启示其实很直接AI 产出的东西如何被信任这个问题答案正在从审查文本变成审查可执行的证明对象。这个模式会溢出到数学之外——配置、协议、调度策略凡是能形式化的东西未来都会有Lean 等价物。我甚至觉得这条流程比 ETH 本身更值得抄进团队规范产出一个结论 → 用机器可检验的形式重述 → 再交给人判断有没有意义。三层分离每层都能被不同的人独立检查。六、实操建议接下来该做什么给三类人三种动作。如果你是做算法/数据库/图计算的去翻你依赖的那些下界论文看看有几条挂着assuming ETH。把它们列出来标注前提待重估。不用删但别再拿它们当这条路走不通的挡箭牌。这周就值得做一次因为这是你手上少有的、成本极低的信息更新。如果你是写基础设施/做性能优化的短期内什么都别改。中期值得盯的是那场会议和后续论文——如果真有人把次指数 SAT 算法压到能跑的常数SAT 求解器、约束求解、程序验证工具链会先被冲一遍。如果你是关注 AI for Science 的重点看的不是AI 又证了一个定理而是三个流程细节原始数据是否公开、形式化是否独立、提出假设的人是否参与了验证。这次的答案分别是是、是、是。这三个是以后判断同类新闻真假的筛子。七、最后一句实话这件事最反直觉的地方在于一个被信了二十五年的假设可能是错的而推翻它的东西只花了一天做形式化。这不代表数学变简单了也不代表人类专家多余了——Impagliazzo 他们的角色不是盖章是决定这个结果该怎么被社会消化。真正稀缺的从来不是证明是判断哪个证明值得被认真对待。而这一次判断权还在人手里。这大概是目前最让人安心的一点。参考OpenAI: Working with academic communities to build scientific understanding2026-10-26openai/math仓库ETH writeup PDF 与lean/docs/378.mdImpagliazzo, Paturi, Zane,Which Problems Have Strongly Exponential Complexity?, JCSS 2001注本文基于 OpenAI 公告与合作组公开材料整理。Lean 证明虽已公开但完整独立复核仍在进行中涉及具体技术细节的结论请以原始 writeup 为准。