Lower Bound of 22 for 3x3 Matrix Multiplication over the Integers
Isaac Rudich, Louis-Martin Rousseau
cs.CC
Oct 1, 2026 · v1
TL;DR
Proves in Lean 4 with Mathlib that recursive 3x3 integer-constant matrix multiplication needs at least 22 multiplications, encoding algorithms as step programs.
Abstract
Strassen showed that two 2x2 matrices can be multiplied with 7 multiplications instead of 8. Applied recursively, his algorithm multiplies two nxn matrices with O(n^2.807) multiplications, beating the naive O(n^3). The best known 3x3 recursive matrix multiplication algorithm uses 23 multiplications O(n^2.854). The best published lower bound of 21 (on algorithms with integer constants) leaves room for an algorithm with O(n^2.771) multiplications, and thus does not rule out the possibility of an algorithm that would beat Strassen's. We prove a lower bound of 22 multiplications for any 3x3 recursive algorithm with integer constants, proving that no such algorithm can do better than O(n^2.814) multiplications, and eliminating the possibility of a 3x3 algorithm that beats Strassen's 2x2 method. The proof builds on a recent decomposition method from Wang, who approached the problem by turning it into 496 subproblems. We provide exact solutions for 359 of them. The proof is in Lean; verification requires auditing only a few short files. The Lean formalization directly encodes statements about the limitations of recursive algorithms for matrix multiplication, as opposed to just a statement about the rank of the problem.
Problem
The best known lower bound of 21 multiplications for 3x3 matrix multiplication with integer constants leaves open a recursive 3x3 algorithm that could beat Strassen's O(n^2.807) exponent. Raising the bound to 22 would rule this out.
Approach
The proof builds on Wang's decomposition of the problem into 496 restricted subproblems over F_2 (Wang's table), adding new lower bounds and new decompositions found with SAT solving, branch and bound, flip graphs and linear programming. In Lean, algorithms are modeled as lists of steps that must multiply 3x3 grids of blocks of any size. A theorem reduces such programs to bilinear decompositions, and the table bounds are then checked over F_2. Auditing requires reading only a few short Defs/Theorems files and checking the axioms used.
Results
The Lean theorem states that every program that multiplies on blocks uses at least 22 multiplications, which bounds any such algorithm at O(n^2.814). The proof bounds all 496 table elements, determines 359 exactly (against 195 for Wang), and raises 252 lower bounds. Its 3,521 modules take 11.1 hours to build on a single core.
| Wang | Ours |
|---|
| Elements determined exactly | 195 | 359 |
| Lower bounds raised by +1 | – | 245 |
| Lower bounds raised by +2 | – | 7 |
Summary of bounds on Wang's table (496 elements)
