Machine-Verifying Toom-Cook Multiplication with Integer Evaluation Points

TL;DR

This paper provides a machine-verified proof of the correctness of a generalized Toom-Cook multiplication algorithm using integer evaluation points, leveraging Lean 4 and AI theorem proving to automate verification.

Contribution

It introduces a formal proof framework for Toom-Cook multiplication with arbitrary integer evaluation points, integrating AI assistance for verification.

Findings

Verified correctness of Toom-Cook with integer evaluation points

Derived a threshold function for algorithm termination

Demonstrated AI's role in automating formal proofs

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.