OpenAI、Anthropic 都宣称推翻 ETH：AI 突破了什么，还不能说明什么？
这几天关于 AI 的一条大新闻，既没有新模型可下载，也没有新的订阅按钮：OpenAI 和 Anthropic 都公开宣称，其内部模型找到了反驳“指数时间假设”的算法与证明材料。这个假设简称 ETH，与以太坊代币没有关系，它关系到某类计算问题究竟能快到什么程度。
OpenAI 在10月26日的研究公告中公布了这项主张；Anthropic 的相关论文也标注10月26日。消息随后进入科技媒体与计算机科学社区的讨论。真正值得关心的，是两家实验室交出了什么，以及“证明已经能被机器检查”究竟意味着什么。
ETH 为什么值得整个行业认真对待？
可以先想象一组需要同时满足的开关条件：甲开、乙关、丙开，满足其中一条还不够，必须让全部规则成立。计算机科学里的3-SAT，就是这类问题的一个标准形式：每条规则涉及至多三个布尔条件，问题是能否找到一组真假取值，让所有规则都满足。
如果有100个开关，把每种组合都试一遍，就有2的100次方种可能。这个例子只是帮助理解搜索空间，并不是这次论文的性能测试。研究者当然早已在寻找比逐个试验更聪明的办法；ETH 提出的限制更强：在最坏情况下，3-SAT 是否仍然无法摆脱某种指数级的增长？Impagliazzo 与 Paturi 的2001年原始论文给出了这个研究框架。
所谓“亚指数时间”，也不是把指数算法快一点点。把2的n次方变成2的0.1n次方，仍属于指数增长；2的根号n次方则是亚指数增长的直观例子。它讨论的是问题规模不断变大时的增长方式，不是在某台电脑上跑完一次任务用了几秒。
ETH 多年来被用于建立条件性的计算困难结论：如果这个假设成立，一些问题就很难达到某种速度。现在出现反驳声明，受到冲击的是这些“如果成立”的前提。已有研究中的方法、转换关系与技巧，并不会因此全部失去价值。
两家实验室交出的，是可公开检查的研究材料
OpenAI 表示，内部模型于10月16日得到自然语言论证，10月17日完成 Lean 形式化。它邀请 Russell Impagliazzo、Ramamohan Paturi 和 Ryan Williams 组织开放审查，其中前两位正是 ETH 的提出者。
Anthropic 的论文则称，核心算法同样在10月16日由内部 Claude 研究模型找到，过程产生约1400万输出 token、没有人工输入；随后研究人员与 Claude 一起整理表达。这是作者对发现过程的陈述，不能扩写成“整篇论文与所有审查完全无人参与”，更不能推断日常订阅里的某个 Claude 版本也一定能重复这一过程。
它的算法主张不只回答“有没有满足条件的组合”，还计数有多少种组合。仓库公开了论文、Lean 文件和检查说明，让外部研究者能够具体追问算法、陈述与证明的对应关系。Anthropic 原始仓库说明
这比只展示一张成绩榜多了一层可审查性。不过，公开材料也把新的工作交给了研究社区：既要读算法，又要确认机器检查的陈述准确表达了论文所讨论的问题。
已有外部复跑，为什么还要继续读证明？
Lean 可以检查一条形式化命题是否由相应论证推出，但不会自动替人判断：写进系统的定义，是否恰好就是论文里那个数学问题。这是两项不同的工作。
Anthropic 的MainResults.lean专门写明算法采用的计算模型、输入编码和适用范围，并说明与通常算法模型之间的一些转换仍以文字解释，没有包含在 Lean 证明里。阅读这些范围说明，与看到检查通过的结果同样重要。它不自动说明证明有错，也不该在新闻报道里被省略。
外部复跑已经开始。Carlos Toledo 的公开核查记录报告，两家的形式化证明都通过了其所用检查工具，但他同样把“检查通过”与“数学含义的阅读判断”分开，并披露工具由 Claude 协助编写。这里引用的是他的检查报告，本文没有独立运行整套证明，也没有代替数学家审定算法。
组织审查的三位学者在致社区公开信中明确表示，参与不等于为主张背书。他们希望大家重建、质疑、解释和扩展论证。这种表态既保留了对重大结果的期待，也给核验留下必要空间。
离“所有困难问题都能轻松解决”，还远得很
ETH 被反驳，即使最终成立，也不等于证明 P=NP。后者追问的是：容易检查答案的问题，是否也都能容易地找到答案。克雷数学研究所的P 与 NP 问题介绍可以帮助区分这两个层次；亚指数算法并不自动成为多项式时间算法。
更实际的限制来自论文自己。Anthropic 在第二页解释，该结果主要属于规模趋于极大时的理论改进，给出的界限并不带来现实规模下的通用优势。由此无法推出“排班、物流或软件验证明天就全面提速”，也无法推出“银行密码已经被破解”。从理论算法到可用工具，中间还隔着算法结构、常数、实现与适用问题的研究。
这条新闻的重要性，因此不必靠夸张结论支撑。AI 开始交出足够具体、足够重大、可以让专业群体逐项检查的研究主张，研究流程也随之改变：发现之后，解释与验证成为新的重心。本站此前讨论Claude 对开源库的形式化验证时，关注的也是证明确切覆盖什么。
接下来值得跟进的，是审查者能否给出更清晰的论证、发现需修正之处，以及哪些后续结论真正成立。对这类 AI 科研新闻，保留这些层次，才看得见进展有多大。
评论