Abstract:We present a machine-verified proof of the correctness of Toom-Cook multiplication with generalized integer evaluation points. Toom-Cook is a class of fast multiplication algorithms parameterized by a triple $(k_x, k_y, \vec v)$ consisting of two positive integer split sizes $k_x, k_y$ and a vector $\vec v$ of distinct evaluation points. As part of our proof, we verify that for any selection of $k_x+k_y-1$ distinct integer evaluation points, we can compute a threshold function $\theta(k_x, k_y, \vec v)$ such that, if the algorithm's base-case problem size is set above this threshold, then the algorithm's termination is guaranteed regardless of the values of the operands. The threshold formula, which we derive by obtaining upper bounds on the subproblem sizes produced by the Toom-Cook recurrence, does not depend on the operands; it depends only on $k_x$, $k_y$, $\vec v$, and the base $b$ in which we operate.
We write the proof in Lean 4, making use of the Mathlib library. We formalize the algorithm, our base case threshold formula, and our key lemma statements in Lean. We then use the AI theorem prover Aristotle to assist in completing the machine verification of the algorithm's correctness. This proof, through its synthesis of human input and AI assistance, demonstrates the considerable power of AI to automate the machine verification process.
From: Srihari Nanniyur [view email]
[v1]
Sat, 14 Mar 2026 17:19:04 UTC (114 KB)
[v2]
Sun, 5 Jul 2026 01:56:05 UTC (118 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。