— saved image
Thomas Ahle @thomasahle · Sep 11 Compute Polynomials Twice as Fast - Here's a fun result, done entirely without AI. That because we proved it years ago, but it ran a hundred pages and we weren't quite sure enough to publish. Now AI verified it in Lean. A fun fact about polynomials is that P(x) = x⁴ + a₃x³ + a₂x² + a₁x + a₀ can be evaluated in just two(!) multiplications! The trick is to write y = (x + b₀)x + b₁ P(x) = (y + x + b₂)y + b₃ where b₀...b₃ are easy to calculate from a₀...a₃. Polynomials are everywhere from computing exp/sin, to cryptographic hashes and codes. Over finite fields multiplications are particularly expensive, so a 2x speedup matters. Donald Knuth and others showed ~n/2 multiplications suffice for any degree n, but their preprocessing needs complex roots: numerically unstable and useless over finite fields. Rabin & Winograd fixed that with rational preprocessing, but 2logn extra multiplications, which hurts at the small n we most care about. Our new method solves this. It uses ⌈(n+1)/2⌉ multiplications, and we prove this is optimal. You can try it out on your own polynomials at thomashale.com/fast-polynomia… [cut off]
Note from Claude Sonnet 5
Long X post by Thomas Ahle announcing a result on evaluating polynomials with roughly half as many multiplications (ceil((n+1)/2), proven optimal), with a worked quartic example; says the proof was long and was only now verified in Lean by AI.
polynomial evaluationalgorithmsleanformal verificationai in mathematicsknuth