多项式求值提速一倍:百年前的证明靠 AI 用 Lean 验证后得以发表
thomasahle · x · 2026-09-11
一条有趣的结果,但作者强调这次「完全没用 AI 做数学,只用了 AI 验证」:他们多年前就证明了该结果,但证明长达上百页,信心不足一直未发表,如今用 Lean 形式化验证通过才敢发布。
核心结论:四次多项式 P(x) = x⁴ + a₃x³ + a₂x² + a₁x + a₀ 只需两次(!)乘法即可求值。技巧是把 Horner 式嵌套改写为 y = (x + b₀)x + b₁,再算 P(x) = (y + x + b₂)y + b₃,其中 b₀…b₃ 可由系数低成本预处理得到。
为什么重要
- 多项式求值遍布 exp/sin 计算、密码学哈希与编码
- 在有限域上乘法尤其昂贵,2 倍提速意义很大
- Knuth 等人早已证明 n 次多项式约需 n/2 次乘法,但其预处理依赖复数根:数值不稳定且无法用于有限域;Rabin & Winograd 的有理预处理方案则需额外 2logn 次乘法
这条也是 AI 辅助数学的一个样本:生成靠人,验证靠形式化工具。
所属事件:四次多项式仅需两次乘法，尘封旧证明经 Lean 验证后发表(5 条相关)→
「研究」频道最新
- 新方法将成对相互作用引入祖先序列重建 — KevinKaichuang · 2026-09-12
- 神经符号推理遭「错误但匹配判定」翻译欺骗，生成式奖励模型来救场 — CWRU · 2026-09-12
- AIRO 上线:用前沿模型自动预测 AI 灾难性风险,效果媲美人类专家 — soumitrashukla9 · 2026-09-12
- LiveBench agentic coding 评测遭质疑:4 个 Python 问题撑起异常高分 — teortaxesTex · 2026-09-12
- NVIDIA BioNeMo 跑 3100 万次蛋白质复合物预测,省约 1.35 GWh 能源 — AllThingsApx · 2026-09-12
- Greenblatt 谈 RL 环境为何 2026 比 2024 更有效 — dejavucoder · 2026-09-12