Polynomials evaluated in just two multiplications, verified in Lean with AI's help after years unpublished
thomasahle · x · 2026-09-11
A fun result—proved years ago but unpublished because the 100-page proof made the authors unsure, until AI-assisted Lean verification gave them confidence.
Core result: a quartic P(x) = x⁴ + a₃x³ + a₂x² + a₁x + a₀ can be evaluated in just two multiplications, by rewriting it as y = (x + b₀)x + b₁, then P(x) = (y + x + b₂)y + b₃, where b₀…b₃ come from cheap preprocessing of the coefficients.
Why it matters
- Polynomial evaluation underlies exp/sin computation, cryptographic hashes, and codes
- Over finite fields multiplication is especially costly, so a 2x speedup is significant
- Knuth and others showed n/2 multiplications suffice for degree n, but their preprocessing needs complex roots—numerically unstable and useless over finite fields; Rabin & Winograd's rational scheme adds 2logn extra multiplications
A neat example of human-generated math with AI/formal verification closing the confidence gap.
More from Research
- A tractable approach to pairwise interactions in ancestral sequence reconstruction — KevinKaichuang · 2026-09-12
- Generative Reward Models Fix Deceptive Autoformalization in Neurosymbolic Reasoning — CWRU · 2026-09-12
- AIRO launches automated catastrophic AI risk forecasts, matching top human forecasters — soumitrashukla9 · 2026-09-12
- LiveBench agentic coding eval questioned: outlier score rests on 4 Python issues — teortaxesTex · 2026-09-12
- 31 million protein complex predictions run on NVIDIA BioNeMo, saving an estimated 1.35 GWh — AllThingsApx · 2026-09-12
- Why RL Environments Work Better in 2026: Greenblatt's Two Reasons — dejavucoder · 2026-09-12