AI-Verified Lean Proof Shows Quartic Polynomials Need Only Two Multiplications
thomasahle · x · 2026-09-11
A fun result done without AI but verified by AI in Lean: any quartic polynomial can be evaluated with just two multiplications via y = (x + b₀)x + b₁, then P(x) = (y + x + b₂)y + b₃. The author's original 100-page proof sat unpublished for years until the Lean verification. Context: Knuth showed n/2 multiplications suffice for degree n, but his preprocessing needs complex roots — numerically unstable and useless over finite fields; Rabin & Winograd's rational fix costs 2log n extra multiplications. With polynomial evaluation everywhere from exp/sin to cryptographic hashes, a 2x speedup over finite fields matters.
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