OpenAI 用 Lean 证明指数时间假说为假，复杂度理论界震动

fortnow · x · 2026-10-29

Lance Fortnow 撰文评述本周大新闻：OpenAI 宣布用 Lean 形式化证明指数时间假说（ETH）为假，Anthropic 随后也发布了自己的论文，Ryan O'Donnell 与 Shiva Kintali 跟进给出更简洁优先的证明。OpenAI 将与 Russell Impagliazzo、Mohan Paturi、Ryan Williams 三位顶尖复杂度理论家合作验证与研究。

背景：ETH 由 Impagliazzo 与 Paturi 于 1999 年提出，断言 3-SAT 必需 2^{cn} 时间；OpenAI 论文给出算法对任意固定 k，可在 (n+m)^{O(1)}·2^{O(n log log n / sqrt(log n))} 时间内判定 k-CNF 可满足性并计数解，从而反驳 ETH 及更强的 SETH。作者建议从 Ryan O'Donnell 的论文入手理解证明。