AI 声称推翻「指数时间假设」：该兴奋到什么程度
OpenAI 与 Anthropic 几乎同时宣布内部模型给出 ETH 的反例，并附 Lean 形式化；人类专家仍在审，加密与日常算力不必立刻恐慌。
过去一周，理论计算机科学圈被一条消息打断节奏：多家消息源称，OpenAI 与 Anthropic 的内部模型各自给出了「指数时间假设」（Exponential Time Hypothesis，ETH）不成立的论证，并用 Lean 做了形式化。消息在 10 月下旬集中发酵，X 上既有兴奋帖，也有冷静的「先等审稿」提醒。
到底说了什么
ETH 大致主张：一类以 3-SAT 为代表的难题，在变量规模变大时，不存在显著亚指数的通用算法。它自 1990 年代末、2001 年前后被提出以来，成了数百篇论文的默认脚手架——不是 P vs NP 本身，但和复杂度下限强相关。
据 X 上多条转述与新闻摘要（含 MIT 的 Ryan Williams 在 10 月下旬公开提及 OpenAI 内部模型「声称反驳 ETH」）：
- 发现日期多被记为 10 月 16 日 左右；公开讨论则在 10 月 26–28 日 前后集中爆发。
- OpenAI、Anthropic 两侧都有「内部模型 + Lean 形式化 / GitHub」的说法；Anthropic 一侧有转述称核心算法由内部 Claude、约 1400 万输出 token、无人工介入完成（仍属二手转述，需对照官方稿）。
- 审阅名单里反复出现 ETH 相关奠基者与 MIT 研究者，说明实验室至少把材料交到了「听得懂的人」手里。
Peter Diamandis 等账号把这件事写成「计算机科学支柱被拆掉」的叙事，传播很快；同时加密从业者强调：即便 ETH 真被推翻，也不等于明天就能破现有公钥体系——渐近结果与工程可实现速度是两回事。
我们怎么读这条「突破」
- Lean 通过 ≠ 人类读通。 形式化助手能检查推导步骤是否合法，却不能替代「这个陈述是不是你以为的那个猜想」的语义核对。多条帖子明确写：人类尚未完整确认。
- 双实验室同日叙事要打折。 「同一天独立发现」很吸睛，也可能是训练数据与评测管道高度同构的产物；在官方技术报告出来前，更适合记成「两家都在推同一条前沿」而不是「科学史级巧合已定案」。
- 对读者有用的行动项不是转发口号，而是：等可复核的证明仓库与专家勘误；把「AI 做前沿数学」记进能力地图，同时把「审稿滞后于生成」记进风险地图。
对「洛晚观察」来说，这类选题的价值不在追热点形容词，而在训练一种习惯：把实验室声明、媒体摘要、大 V 情绪三层拆开。ETH 若最终站住，影响的是理论脚手架；若被撤回或大幅收窄，则提醒我们——AI 新闻的半衰期往往短于证明的半衰期。