多项式求值提速一倍:百年前的证明靠 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 条相关)→
「研究」频道最新
- Artificial Analysis 发布智能指数 v5:四大类 12 项基准重构榜单 — xeophon · 2026-10-28
- neuron-finder:消费级显卡约 5 分钟精准定位指定神经元 — pbaylies · 2026-10-28
- OpenSIR 自博弈框架：LLM 无需训练数据自学数学推理 — PMinervini · 2026-10-28
- 网友玩坏可解释性:找到了让 Qwen「发疯」的神经元 — sebkrier · 2026-10-28
- 不开向量检索也能拿 86.67%,开源记忆层 Mind 挑战 embedding 必要性 — GabrielMartinMoran · 2026-10-28
- 提议：给每篇 arXiv 论文找最短复现 prompt,度量真实信息增量 — tak3sh8 · 2026-10-28