解读 OpenAI 称其 AI 证伪指数时间假设：运行时间测算与 Lean 形式化证明细节

OpenAI 宣称其内部模型给出了证伪指数时间假设（ETH）的确定性算法，并已在 Lean 中完成定理形式化证明。该解读文章分析指出，论文给出的确定性算法虽能在多项式空间内亚指数级计数 k-CNF 解，但未给出隐藏常数，且在 Lean 形式化中证明的较弱界限仅在变量数达到约 2400 位数时才优于穷举。