The rank of 3x3 matrix multiplication over F2 is 23
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 𝔽2 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.
Related
- Unbiased Low-Rank Approximation for Repeated Matrix-Vector Multiplication: Stability and Optimal Sampling
- Low-Rank Masking for Single-Server Matrix Multiplication
- Comment on "The polarization hierarchy for polynomial optimization over convex bodies, with applications to nonnegative matrix rank"
- Finite Local Rings Free of Rank Three over Zpn: Radical Filtrations, Matrix Models, and the Frobenius Property
- Approximate Matrix Multiplication through Joint Leverage Score Sampling
BibTeX
@misc{tomar2026rank,
title = {{The rank of 3x3 matrix multiplication over F2 is 23}},
author = {Tejasvi Singh Tomar},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.11823},
eprint = {2610.11823},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.11823},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - The rank of 3x3 matrix multiplication over F2 is 23
AU - Tejasvi Singh Tomar
PY - 2026
DA - 2026/10/19
PB - arXiv
DO - 10.48550/arxiv.2610.11823
UR - https://arxiv.org/abs/2610.11823
AB - 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 𝔽_2 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.
ER -