Fortnow 谈为何复杂性结果难以 Lean 形式化：难在证明多项式时间

fortnow · x · 2026-10-16

理论计算机科学家 Lance Fortnow 在博客讨论 OpenAI Math Drop 中部分论文有 Lean 证明、部分（含 L = RL = BPL）没有的原因。

以 Lautemann 证明 BPP ⊆ Σ₂ᵖ 为例：证明核心是一个单一公式加上概率论证。让 Claude 把概率论证形式化并不太难，但 Lean 会强制处理论文里一笔带过的细节（如 x∉B 时需要 nᵏ·2⁻ⁿ < 1 这类条件）。真正的难点在于：证明算法确实运行在多项式时间内——像「给定 x、y 和 zᵢ，可在多项式时间内计算该析取式」这样在纸面上「痛苦地显然」的命题，写进 Lean 反而最费劲。