Machine-Verifying Toom-Cook Multiplication with Integer Evaluation Points
Srihari Nanniyur, Siddhartha Jayanti
cs.DS
Mar 14, 2026 · v3
TL;DR
Formalizes Toom-Cook multiplication with arbitrary integer evaluation points in Lean 4 with Mathlib, proving termination and correctness with Aristotle AI assistance.
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 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.
Problem
Toom-Cook multiplication is parameterized by split sizes and a vector of evaluation points. When those points are arbitrary integers, it is not obvious that the recursion terminates, so a correctness proof needs a base-case threshold that does not depend on the operands.
Approach
The authors derive a threshold formula θ(k_x, k_y, v) by upper-bounding the subproblem sizes produced by the Toom-Cook recurrence; θ depends only on the split sizes, the point vector and the base b. They specify the algorithm, θ and the key lemma statements in Lean 4 using Mathlib, representing polynomials as coefficient vectors. The AI prover Aristotle completed the proofs, and GPT-5 helped locate Mathlib lemmas and choose proof strategies.
Results
A machine-verified Lean proof that Toom-Cook terminates and returns the correct product for any k_x+k_y-1 distinct integer evaluation points, given the derived threshold. The repository also contains an Aristotle-assisted correctness proof of Karatsuba's algorithm.
