共 1 篇文章
2026 年 10 月 26 日，OpenAI 宣布其内部模型证伪了指数时间假设（Exponential Time Hypothesis，ETH）——一个由 Impagliazzo、Paturi 与 Zane 于 1999 年前后提出、被数百篇论文当作前提的计算复杂性猜想。模型于 10 月 16 日给出自然语言反证，10 月 17 日完成 Lean 形式化；论文给出一个确定性算法，能在亚指数时间、多项式空间内精确计数固定宽度 CNF 公式的满足赋值，取 3-SAT 即推翻 ETH。ETH 的原始提出者 Impagliazzo、Paturi 与 MIT 的 Ryan Williams 牵头独立审查，并明确“参与不代表认证”。Anthropic 随后也发布了自己的 ETH 反证。本文用通俗语言解释 ETH 是什么、这次到底证明了什么、没证明什么（不是以太坊、不推出 P=NP、目前没有发现密码学被攻破、不意味着 SAT 求解器立刻变快），Lean 形式化能保证什么、不能保证什么，以及它对学术界、AI 科研范式和企业智能体的含义。