Machine-Verifying Toom-Cook Multiplication with Integer Evaluation Points
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 obtain a formula for a base case threshold $θ(k_x, k_y, \vec v)$ sufficient to ensure termination 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 continuing capability of AI to automate the machine verification process.