Toom-Cook multiplication splits large numbers into pieces, evaluates a polynomial at chosen integer points, multiplies the pieces, and interpolates to recover the product. The algorithm generalizes Karatsuba's trick: instead of splitting into two parts and saving one multiplication, split into k parts and save more. The evaluation points matter — different choices yield different algorithms with different performance characteristics.
Nanniyur and Jayanti formally verify in Lean 4 that Toom-Cook works correctly for generalized integer evaluation points. The verification covers the full parameterized family: for any split size k and any valid vector of evaluation points, the algorithm computes the correct product. The key contribution is a threshold function — a formula for the minimum input size at which the algorithm terminates, expressed purely in terms of the evaluation points, independent of the numbers being multiplied.
The threshold is necessary because Toom-Cook is recursive: it calls itself on smaller subproblems. If the subproblems don't shrink below the base case, the recursion never terminates. The threshold function guarantees termination by bounding the maximum recursion depth. Previous implementations either hardcoded specific evaluation points or verified termination case by case. The parameterized threshold covers all valid configurations at once.
The AI theorem prover Aristotle assisted the verification — automatically discharging many of the intermediate lemmas that make formal verification tedious for humans. The structural point is not that AI helped (many proofs now involve AI assistance) but what was verified: not a specific algorithm but a family of algorithms parameterized by their design choices, with a single proof covering the entire family. The verification is as general as the algorithm.