多项式求值提速一倍：旧证明被搁置多年，今由 AI 在 Lean 中验证
thomasahle · x · 2026-09-11
作者 thomasahle 分享一个「完全没用 AI 做出、但靠 AI 完成验证」的结果：多项式可以以两倍速度求值。
- 核心事实：n 次多项式传统 Horner 求值需 n 次乘法；他们多年前证明可大幅减少乘法次数（如四次多项式仅需 2 次乘法），但证明长达上百页，作者一直没有足够把握发表。
- 转折：如今用 AI 在 Lean 中完成形式化验证，证明的正确性终于得到确认。
- 技术思路：构造 H2、H4、H8 等嵌套多项式，用「平方差」技巧 H4 = (H2+x+a)(H2-x-a) 只花一次乘法就把次数翻倍；把多项式写成系数列表（如 H4 = [1,b,c,a,e]）并从左到右可解码各参数；最后构造两个共享前缀、交错可解码的多项式 H8 与 H'8，通过 P = x·H8 + H'8 合并，保持逐系数解码性。总策略是「始终同时构建两个兼容的」。
既是算法结果，也是 AI 辅助形式化验证（Lean）助力数学发表的实际案例。
所属事件:四次多项式仅需两次乘法，尘封旧证明经 Lean 验证后发表(5 条相关)→
「研究」频道最新
- Mandelbrot 集拼图结构在 Lean 中完成形式化计算,实拍级图表曝光 — geoffreyirving · 2026-10-28
- Geoffrey Irving 对 CSETH 突破给出 >80% 概率预测 — geoffreyirving · 2026-10-28
- 抗衰研究数据荒：Norn 募资 1500 万美元为 AI 备好训练数据 — juanbenet · 2026-10-28
- 研究员自曝置信度乌龙：把 SETH 当 CSETH，重估 P vs NP 赔率 — geoffreyirving · 2026-10-28
- Google 论文指出 softmax 标准实现藏两个数值 bug，引发形式验证讨论 — srush_nlp · 2026-10-28
- AI 提出的研究题 45/135 获专家认可有趣，覆盖数学物理等 — StanfordAILab · 2026-10-28