尘封多年的多项式求值证明经 AI 用 Lean 验证后发表

thomasahle 分享了一项「完全没用 AI 做出、但靠 AI 验证」的数学成果：借助有理预处理，n 次首一多项式求值只需 ⌊n/2⌋+1 次乘法（一般多项式多一次），远优于 Horner 方法的 n 次乘法，例如四次多项式仅需两次乘法，求值速度提升一倍。该证明长达上百页，作者因信心不足搁置多年，如今借助 Lean 形式化验证通过才得以发表。

2026-09-11 ~ 2026-09-11 · 4 条相关

• 四次多项式仅需两次乘法,AI 用 Lean 验证尘封证明 — thomasahle · 2026-09-11
• 多项式求值提速一倍:百年前的证明靠 AI 用 Lean 验证后得以发表 — thomasahle · 2026-09-11

另有 2 条近重复转述:thomasahle · thomasahle