OpenAI 推翻指数时间假说：AI 生成的数学证明该信几分，又该怎么验证？
先说结论
OpenAI 在 2026 年 10 月 26 日公开了一份经过 Lean 形式化验证的证明，主张其内部模型推翻了计算复杂性理论中沿用 27 年的指数时间假说（ETH）——3-SAT 存在亚指数时间、多项式空间的确定性精确算法。这份主张目前仍处于独立审查阶段，审查组由 ETH 的两位提出者 Russell Impagliazzo、Ramamohan Paturi 和 Ryan Williams 领衔。
我的判断是：这条新闻真正的看点不是”ETH 是不是真的错了”——那要等数学社区审完才有答案——而是 OpenAI 这次展示的完整验证管线：AI 产出当原始数据发布、Lean 形式化做硬校验、原提出者组队独立审查、原始材料全部公开。对每天都要处理 AI 输出的工程团队来说，这套”生成便宜、验证昂贵”的分层验证设计，比结论本身更有直接借鉴价值。
发生了什么
主来源是 OpenAI 官方博客《Working with academic communities to build scientific understanding》，发布日期 2026 年 10 月 26 日，原始 URL：https://openai.com/index/building-scientific-understanding-with-academic-communities/。同日，配套材料全部进入公开 GitHub 仓库（https://github.com/openai/math，截至 10 月 27 日已有约 1.59 万 star）。
官方事实一：三项发现同日公布。 数学方向是欧氏波方程的 local smoothing 猜想证明（进而推出全维度的 Kakeya 猜想与 Stein 限制性估计），10 月 18 日获得 AI 输出、次日完成 Lean 形式化；计算机科学方向是 ETH 反证，10 月 16 日得到自然语言证明、10 月 17 日完成 Lean 形式化；物理方向是四维含规范场与费米子的相互作用量子场论（含 QCD 与标准模型的一个统一补全）的严格存在性证明，其中纯 Yang–Mills 存在性部分是千禧年大奖难题的子问题，10 月 16 日完成 Lean 形式化。
官方事实二：ETH 反证的算法主张。 仓库 history.md 描述该论文给出一个确定性算法，在亚指数时间内、多项式空间中精确计数固定宽度 CNF 公式的满足赋值；3-SAT 情形直接推翻 ETH。OpenAI 应审查工作组的要求立即公开了自然语言证明和 Lean 形式化，并承诺资助一场公开会议来审视这项工作对整个领域的影响。
官方事实三：仓库整体规模与自纠错记录。 openai/math 目前收录 721 份手稿、归入 373 个家族，约 42% 的主要结果已有 Lean 形式化。这些结果绝大多数由同一个未公开的内部模型产出，平均每个结果消耗约 3 小时的 ChatGPT Pro 推理算力，评估期间模型被投入约 4000 道问题。值得注意的是仓库的 history.md：10 月 7 日曾因一个符号错误撤回 3 份手稿（涉及 Weil 类代数性），同时修复 14 份，全部撤回与修订记录随版本保留、可公开追溯。
官方事实四：三种发布策略 + 四项原则。 这次 OpenAI 对三个学科刻意采用不同发布方式——数学结果直接放出 AI 原始输出，让研究者自行组织解读；计算机科学结果由外部协作组解释、AI 原始材料同步公开；物理结果则由外部组自行撰写、暂不放出 AI 产物。官方博客明说这是实验，三种方式哪种最有效尚无答案。四项协作原则为透明（参与者不签保密协议）、不署学术荣誉（不把发现归于任何人）、承认理解者的贡献、独立且无薪。
官方边界声明必须完整转述： 论文自身注明，形如 2^o(n) 的运行时间界不能通过一般多项式时间归约传递，因此该结果不意味着一般 NP 问题都有亚指数算法。第三方解读页（gravitypersists.github.io，2026 年 10 月 27 日上线）将当前状态标注为”claim · under review”，并强调 Lean 校验覆盖的是主定理的一个版本。
来源汇总：OpenAI 官方博客（2026-10-26）、openai/math 仓库 history.md（2026-10-26 更新）、ETH 论文页 README（2026-10-25）、第三方解读（2026-10-27）、Hacker News 讨论（两帖合计约 1700 分、800 评论，2026-10-26 至 10-27）。下文的技术分析与工程解读是我的判断，与官方无关。
技术细节
1. ETH 是什么，倒下会晃动什么
指数时间假说由 Impagliazzo、Paturi（与 Francis Zane）在 1999 年前后提出，内容大致是——3-SAT 在变量数 n 上的最坏情形运行时间必须呈 2^(Ω(n)) 增长，不存在 2^o(n) 的算法。它比”P=NP 吗”更精细：即使 NP 问题都有多项式算法之外的世界被排除，复杂度学者仍需要一把更锋利的尺子来区分”多项式但太慢”与”指数且不可救药”。27 年来，图论、计算生物学、数据库、计算几何等领域的数百篇论文用”假设 ETH 成立”推出条件下界——某问题不可能在某某时间内解决。ETH 一旦倒了，这批条件结果全部失去支点，需要重新审视。
2. 为什么 Lean 形式化是这条管线的关键一环
Lean 是交互式定理证明器，逐条检查证明的每一步推理，只有全部通过才接受。对 AI 生成的证明，它的价值在于把”看起来对”变成”机器验证过对”。但覆盖率是诚实的边界——官方数字是约 42% 的主要结果有 Lean 形式化，本次 ETH 论文是”主定理的一个版本”被形式化。也就是说，机器验证是硬闸门而不是全覆盖保险；未形式化的过半结果仍处在”未验证”状态，官方 README 也直说部分未形式化结果可能有问题。
3. 分层验证管线的设计
把这次发布拆开看，是一张四层过滤网。第一层是产出筛选——4000 道问题筛出 721 份手稿，按重要性聚合；第二层是 Lean 硬校验——主定理版本级验证；第三层是独立专家审查——由假说提出者本人领衔，官方明确”参与不代表认可”；第四层是社区公开审查——原始数据、撤稿记录、版本历史全部公开，任何人可复核。撤稿机制是这张网自我修正的证据：10 月 7 日那批撤稿不是丑闻，而是管线在正常工作。
4. 与 10 月 6 日首次发布相比的进化
10 月 6 日 OpenAI 首次公开这批数学材料时，采用的是”全部直接放出”的单一策略；三周后这次发布进化为按学科分流的三策略实验，并配套四项协作原则。这说明发布协议本身在快速迭代——官方博客坦言，选定初始审稿人必然造成信息不对称，他们公开征集更好的方案。
对 Agent/工程的影响
其一，生成与验证的剪刀差是 Agent 工程的核心约束。 一个结果 3 小时算力生成，而人类审查以周月计。这套不对称在 Agent 系统里同样成立——Agent 批量产出代码、报告、决策建议，而验证带宽才是系统吞吐的真瓶颈。openai/math 的四层管线给出一个可抄的模板：产出筛选、机器硬校验（对应我们工程里的 schema 校验、静态检查、测试套件）、独立评审、公开可追溯。
其二，形式化验证正在成为 AI 输出的最高级过滤器。 大多数团队止步于 schema 验证和单测，而这次事件把”机器可检验的规约 + 证明检查”推到了台前。对关键路径逻辑（账务、并发、安全边界），把自然语言需求提升为可形式化检验的规约，可能是 Agent 时代最值得投入的工程基建之一。
其三，文献依赖要标注”条件假设”的时效。 不少算法选型的依据来自”假设 ETH/SETH 成立则无更快算法”的条件下界文献。这批结果短期内不会被推翻性改写——审查尚未完成——但在技术报告和论文引用里加一条”该假设正被挑战”的脚注，是低成本的风控。
其四，worst-case 与工程实践的距离没有变。 HN 讨论里最热的技术评论恰恰在提醒——即使 ETH 被推翻，工业界 SAT 求解器（基于 CDCL 等技术）的实践性能与最坏情形理论算法是两个世界。这项工作改写的是复杂度图景，不是下个季度就能落地的加速器。工程师不必调整任何现有选型。
我的判断
第一，对”ETH 被推翻”这个主张本身，我做分级置信：Lean 校验过的主定理版本可信度显著高于自然语言版本，但它是”一个版本”，而且这条管线三周前刚撤过稿。我押”核心算法主张大概率站得住，但会以修补和限定范围的方式站住”。撤稿史不但不减分，反而是这套管线可信的证据——敢公开认错、版本可追溯，比”永远正确”的宣传可信得多。
第二，这套发布协议会被各家 AI 实验室抄。三个学科三种发布策略本质是一次 A/B 测试，四项原则（透明、不署名、承认理解者、独立无薪）精准回应了此前学术界对 AI 产出冲击荣誉体系的担忧。可以预期，”AI 产出 + 外部 shepherd + 形式化验证 + 原始数据公开”会成为 AI 生成科学主张的标准交付格式。
第三，验证带宽是下一个稀缺资源。4000 道题、721 份手稿、42% 形式化率、3 位领衔审查人——每往管线深处走一层，可处理的对象数量骤减。当生成成本趋近于零，整个科学共同体和工程界的瓶颈都会向验证侧转移。”验证即服务”可能成为一个真实赛道。
第四，对 Agent 工程师最实用的一课是诚实分层。openai/math 把”Lean 已验证”、”未形式化”、”已撤回”标得清清楚楚，而不是把 721 份手稿包装成一个光鲜的数字。我们构建 Agent 系统时同样应该让每个输出的验证等级可见——哪份是机器验证过的，哪份只是模型说的。这个习惯在证据链上的价值，这次被官方示范了一遍。
Q&A
Q：ETH 被推翻等于 P=NP 吗？
A：不等于。论文明确注明 2^o(n) 型运行时间界不能经一般多项式时间归约传递，该结果不暗示一般 NP 问题存在亚指数算法。ETH 只约束固定宽度 CNF（如 3-SAT）的精确求解复杂度，与 P 与 NP 是否相等是不同层面的问题。
Q：SAT 求解工具会因此变快吗？
A：短期内不会。论文算法的意义在复杂度图景层面，最坏情形理论算法与工业求解器的实践性能之间隔着巨大的工程鸿沟。现有求解器选型无需调整。
Q：这份证明到底验证了没有？
A：分三层回答——Lean 已验证主定理的一个版本；由 Impagliazzo、Paturi、Williams 领衔的独立工作组正在审查，且官方强调参与不等于认可；OpenAI 承诺资助公开会议供社区审视。在审查完成前，把它当作”待确认的重大主张”是准确的姿势。
Q：之前撤稿是怎么回事？
A：10 月 7 日，仓库因一个符号错误撤回 3 份手稿并修复 14 份，全部记录随版本公开保留。这是管线自纠错机制在工作，不是掩饰——被撤手稿的 README 会说明缺口并链接存档版本。
Q：工程团队现在需要做什么？
A：不需要改任何算法选型或架构。值得做的是两件小事——引用 ETH/SETH 条件下界的文档加时效脚注；更重要的，借鉴这套四层验证管线，为自己系统里 AI 产出的验证等级建立可见的标注。