2026年10月16日，OpenAI的一个内部模型生成了一份67页的数学证明，声称指数时间假说（ETH）为假。同一天，Anthropic的Claude在未经任何人类干预、耗费1400万个输出token的情况下，独立得出了相同的结论。这两份文件随后被翻译成Lean形式语言进行机器验证，均通过。
据复杂度理论博客Computational Complexity的作者、佐治亚理工学院教授Lance Fortnow的评估，两家机构给出的算法能在 $(n+m)^{O(1)} \cdot 2^{O(n \log\log n / \sqrt{\log n})}$ 时间内求解k-SAT问题——这个量级被称为次指数时间（2^o(n)），理论上直接反驳了ETH关于“不存在比指数时间更快的3-SAT算法”的核心断言。Fortnow写道：“我没有亲自验证这份证明，但现在可以安全地认为，指数时间假说已经终结。”
什么是ETH，它为何重要
指数时间假说由Russell Impagliazzo、Ramamohan Paturi与Francis Zane于2001年共同提出。其核心命题是：3-SAT问题在最坏情况下需要指数时间求解，不存在本质上更快的算法。这个假说虽然不等同于P≠NP，但在此后25年间被用作数百篇算法复杂度论文的前提基础，成为理论计算机科学中事实上的基石之一。
正因如此，当OpenAI在10月26日公开发布其GitHub仓库、同时公布自然语言证明与Lean形式化版本时，算法理论界的反应不是喜悦，而是谨慎。ETH原作者Impagliazzo和Paturi，以及麻省理工学院的Ryan Williams，随即发出公开声明：“如此重大的结果，需要严格的独立审查。” 三人组织了一个独立评审小组，Williams明确表示“未签任何保密协议，也未接受任何报酬”。
Lean通过：这究竟核验了什么
Lean是一个数学定理证明助手，能够逐步检验每一个逻辑推导步骤的形式有效性。OpenAI在生成自然语言证明后的次日即完成了Lean形式化。
Lean验证的是“这份Lean代码从其前提出发逻辑自洽”，而不是“这些前提在数学上等价于ETH的完整表述”。据公开Lean仓库的说明，该形式化版本核验的算法界是“略弱于主要数学声明的版本”——也就是说，Lean证明的命题和论文正文的命题之间存在技术差距，而这个差距的等价性本身尚未被形式化证明。
独立研究者Ryan O'Donnell和Shiva Kintali随后各自发布了简化版的跟进证明，刻意选择牺牲最优界换取清晰度——专业社区正在努力将这份机器辅助的高度压缩证明重新翻译成人类可追踪的形式。
两家公司同日独立得出相同结论
Anthropic披露的一个细节：Claude在求解过程中“未经任何人类输入”，使用了1400万个输出token。这个规模意味着Claude生成的推理链条远超任何人类数学家的单次工作量——它相当于一份约3万页的草稿。
两家公司在同一天独立达到相同的次指数界 $2^{n/\sqrt{\log n}}$。这更可能说明：在当前的AI能力水平下，这个数学路径已经进入了模型的“可到达区域”，只是此前没有人针对性地尝试。这与其说是突破，不如说是一次能力边界的测量——AI在不需要人类路线图的情况下，能在多大的搜索空间里找到有效的数学构造？
密码学的恐慌是否有据可依
当前的主流公钥密码体系（RSA、椭圆曲线加密）的安全性建立在整数分解和离散对数问题的困难性上，而非直接依赖于ETH。ETH被推翻意味着一类特定的算法界假设失效，但并不直接意味着整数分解变得容易。
更直接的量化来自Anthropic自己的论文：在每变量5条子句的3-SAT实例中，其算法要在实际效果上超越暴力搜索，问题规模需要达到 $10^{10000}$ 个变量。这个数字的含义是：即便证明成立，这个算法在地球上任何可预见的计算设备上都不会产生实际的SAT求解效率提升。对现有加密基础设施，当前不存在直接威胁。
AI辅助数学：信任机制的缺口
这起事件揭示出一个AI科学发现领域的系统性问题，而非单一事件的瑕疵。
传统数学社区的信任建立机制是：专家读懂证明、发现漏洞、同行评审、时间沉淀。这个机制在面对AI生成的高密度证明时正在承压。当一份证明长达67页、由机器逐步构造、通过了形式化核验但超出了多数专家的实时阅读速度，“已证明”的共识如何形成？
Lean系统提供了一条新路径：将信任从“专家能否读懂”转移到“形式系统是否自洽”。但这条路径有两个前提必须同时成立：第一，Lean中的形式声明必须忠实还原原始数学命题；第二，Lean系统本身的可靠性必须得到足够的信任。前者目前仍是开放问题，后者在理论计算机科学界已有较强共识，但并非绝对。
ETH原作者Impagliazzo、Paturi与Williams正在做的事情，本质上是在修复这个缺口：由最有能力判断“形式声明是否等价于原始命题”的人，补充一道人工核查层。这道层本不应该是事后补丁，而应当是AI辅助数学发现的标配流程。
独立判断
从目前可核实的证据出发，给出以下判断：
极有可能成立的部分：AI模型确实在理论复杂度的某个技术路径上取得了实质性数学进展。Lean验证通过、顶级复杂度研究者愿意投入时间做独立审查（且不收报酬），这两点是正面信号。Lance Fortnow的谨慎乐观代表了理论界目前的主流情绪。
仍未闭合的缺口：Lean形式声明与ETH完整数学陈述的等价性，尚未被形式化证明。这不是小漏洞，这正是当前整个独立审查的核心工作。在此之前，“ETH已被推翻”是一个高置信度的预期，而非已确认的结论。
更大图景：这次事件展示了AI在数学发现中的真实能力边界——它可以在没有人类路线图的情况下完成高度技术性的数学构造，而且速度极快。但它同时暴露了现有知识验证体系的脆弱性：当AI的输出速度超过人类核查速度，科学社区如何在不降低标准的前提下及时消化这些结果，将是未来几年的核心制度挑战，与数学本身的难度同等重要。
© 2026 Winzheng.com 赢政天下 | 转载请注明来源并附原文链接