四次多项式仅需两次乘法,AI 用 Lean 验证尘封证明

thomasahle · x · 2026-09-11

作者分享了一个完全没用 AI 做出、但由 AI 用 Lean 定理证明器完成验证的有趣结果：多项式 P(x) = x⁴ + a₃x³ + a₂x² + a₁x + a₀ 只需两次乘法即可求值。技巧是先算 y = (x + b₀)x + b₁，再算 P(x) = (y + x + b₂)y + b₃，其中 b₀…b₃ 可由 a₀…a₃ 容易推出。

作者称这个证明几年前就完成了，但长达百页、一直不敢发表，现在 AI 在 Lean 中验证通过。背景：Knuth 等人证明 n 次多项式约需 n/2 次乘法，但其预处理依赖复数根，数值不稳定且在有限域上不可用；Rabin & Winograd 的有理数修正版要多花 2logn 次乘法。多项式求值广泛存在于 exp/sin 计算与密码学哈希中，有限域上乘法尤其昂贵，2 倍加速意义不小。