多项式求值减半乘法数的老证明，多年后被 AI 在 Lean 中验证

thomasahle · x · 2026-09-11

作者 thomasahle 分享一个纯数学（非 AI 产出）的结果：借助有理预处理，首一多项式求值只需 ⌊n/2⌋+1 次乘法（一般多项式多一次），远优于 Horner 方法的 n 次。例如四次多项式 P(x) 可以只用两次乘法求值。该证明多年前完成，但因长达百页且作者信心不足未发表，如今由 AI 在 Lean 中完成形式化验证，终于可以发布。配套发布了在线「chain compiler」网站，输入多项式与域即可生成预处理方案，论文见 arXiv:2609.06022，代码在 GitHub。可用于 exp/sin/cos 逼近及密码学、哈希、编码理论中的多项式求值。