AI verified a years-old polynomial proof in Lean, a coauthor says

A coauthor says the team proved the result years ago without AI, but the proof ran to 100 pages and they weren't confident enough to publish. They say AI has since verified it in Lean, a proof assistant. Their method reportedly needs ⌈(n+1)/2⌉ multiplications—rounding (n+1)/2 up to a whole number—to evaluate a degree-n polynomial, and they claim that count is optimal. The author highlights the potential benefit for finite fields, where they say multiplication is particularly expensive, and shares a tool for trying the method.