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