共 2 篇文章
深度解读 arXiv:2610.08144《Navier-Stokes lost in translation》：为什么 AI 把自然语言证明翻译成 Lean 并编译通过，仍不能保证原证明正确；OpenAI Navier-Stokes 爆破证明中的两类翻译失真、比停机问题更难的歧义消解、Meta 教科书形式化事件，以及这些结论对软件测试全自动化、AI 生成测试和形式化验证的直接启示。
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 科研范式和企业智能体的含义。