The rank of 3×3 matrix multiplication over F2 is 23
In plain words
Computers multiply tables of numbers, called matrices, all the time, in graphics, simulations and machine learning, and methods with fewer multiplications can speed this up. Strassen found a shortcut for 2×2 matrices in 1969. For 3×3 matrices the best method, Laderman’s from 1976, uses 23 multiplications, and whether 23 are needed has been open since. During 2026 several groups raised the lower bound step by step. This paper closes the gap: 23 are needed when the arithmetic is done in bits, where 1 + 1 = 0, and for every method with whole-number constants.
Abstract
The rank of the tensor of 3×3 matrix multiplication over the field with two elements is at most 23 by Laderman's algorithm, and Rudich and Rousseau recently proved that it is at least 22. We prove that it equals 23. Hence Laderman's algorithm uses the fewest multiplications among all bilinear algorithms over F2 and among all bilinear algorithms with integer coefficients. The proof uses the substitution method in the form developed by D'Ambrosio, Wang and Yang et al., which bounds the number of first factors of a decomposition that lie in a given subspace of the space of first factors. We sharpen these bounds for 111 of Wang's 496 classes of subspaces, constrain the ranks of the first factors through a 27×27 flattening of the tensor, and list, up to symmetry, all sets of 22 first factors that satisfy these constraints. An exact completion search shows that none of them is the set of first factors of a decomposition. The computation emits certificates, which are checked in the Lean 4 proof assistant. In one formal proof the largest checks are evaluated as compiled code, and in a second one the kernel evaluates every check, so that its final theorem depends only on the three standard axioms of Lean. The Lean proofs build on the formalization of Rudich and Rousseau and import their table of bounds and their reduction for block algorithms.
