Evaluating polynomials twice as fast: old 100-page proof finally verified in Lean by AI
thomasahle · x · 2026-09-11
thomasahle shares a result "done entirely without AI, but AI-verified": polynomials can be evaluated roughly twice as fast.
- The fact: a quartic like P(x) = x⁴+a₃x³+a₂x²+a₁x+a₀ can be evaluated in just two multiplications. They proved this years ago, but the 100-page proof left them unsure enough to publish — until AI verified it in Lean.
- The trick: build nested polynomials H2, H4, H8 and use the difference-of-squares identity H4 = (H₂+x+a)(H₂−x−a) to double the degree with a single multiplication; represent polynomials as coefficient lists (H4 = [1,b,c,a,e]) decodable left to right; finally interleave two prefix-compatible polynomials H8 and H'8 via P = x·H8 + H'8, keeping them jointly decodable. The general strategy: always build two compatible polynomials at once.
Both an algorithmic result and a real case of AI-assisted formal verification unblocking a publication.
More from Research
- ECCV 2026 paper shows a clever way to train segmentation on misaligned labels — ducha_aiki · 2026-09-11
- NTU's Facet-0 robot model lifts precision assembly success from 16% to 82% — jiqizhixin · 2026-09-11
- Wiz Launches Cyber Model Arena: Gemini 3.8 Flash Cyber Tops at 74.9% — rseroter · 2026-09-11
- Meta's Auto-RecSys runs autonomous research on industry-scale recommenders — omarsar0 · 2026-09-11
- SW-graph Won the First ANN-benchmarks in 2015 and Was Already Production-Ready, Author Recalls — srchvrs · 2026-09-11
- New Paper Shows Self-Replicating AI Agents Evolve Cooperation From Scratch — AdaptiveAgents · 2026-09-11