HEXAGONbeta

The rank of 3×3 matrix multiplication over F2 is 23

A mix of human-written and AI-generated textHuman understanding: all partsmath.RA — Rings and Algebrascs.CC — Computational Complexity

Contributed by Tejasvi Singh Tomar ↗

Version 1 / Oct 26, 2026/ arXiv: 2610.11823 / CC BY 4.0

Abstract

The rank of the tensor of 3×33\times 3 matrix multiplication over the field with two elements is at most 2323 by Laderman's algorithm, and Rudich and Rousseau recently proved that it is at least 2222. We prove that it equals 2323. Hence Laderman's algorithm uses the fewest multiplications among all bilinear algorithms over F2\mathbb{F}_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 111111 of Wang's 496496 classes of subspaces, constrain the ranks of the first factors through a 27×2727\times 27 flattening of the tensor, and list, up to symmetry, all sets of 2222 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.

References

  1. B. Alexeev, M. A. Forbes and J. Tsimerman, Tensor rank: some lower and upper bounds , in: 26th Annual IEEE Conference on Computational Complexity (CCC 2011), 2011, 283--291.
  2. P. Bürgisser, M. Clausen and M. A. Shokrollahi, Algebraic Complexity Theory , Grundlehren der mathematischen Wissenschaften 315, Springer, 1997.
  3. S. Beuchert, Independent verification of the Wang $\F$-certificate for R(⟨3,3,3⟩)≥20R(\langle 3,3,3\rangle)\ge 20 , Zenodo, 2026, https://doi.org/10.5281/zenodo.20691957.DOI
  4. M. Bläser, On the complexity of the multiplication of matrices of small formats , J. Complexity 19 (2003), 43--60.
  5. M. Bläser, Fast matrix multiplication , Theory of Computing Library, Graduate Surveys 5, 2013.
  6. N. T. Courtois, G. V. Bard and D. Hulme, A new general-purpose method to multiply 3×33\times 3 matrices using only 2323 multiplications , arXiv:1108.2830, 2011.arXiv
  7. I. D'Ambrosio, The exact $\F$-rank of 2×32\times 3 by 3×43\times 4 matrix multiplication , Zenodo, 2026, https://doi.org/10.5281/zenodo.21895176.DOI
  8. L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language , in: Automated Deduction -- CADE 28, Lecture Notes in Comput. Sci. 12699, Springer, 2021, 625--635.
  9. G. Gonthier, Formal proof---the four-color theorem , Notices Amer. Math. Soc. 55 (2008), 1382--1393.
  10. T. Hales et al., A formal proof of the Kepler conjecture , Forum Math. Pi 5 (2017), e2.
Show all 27 referencesShow fewer references
  1. J. E. Hopcroft and L. R. Kerr, On minimizing the number of multiplications necessary for matrix multiplication , SIAM J. Appl. Math. 20 (1971), 30--36.
  2. M. J. H. Heule, M. Kauers and M. Seidl, New ways to multiply 3×33\times 3-matrices , J. Symbolic Comput. 104 (2021), 899--916.
  3. M. Kauers, collection of schemes of length 2323 for 3×33\times 3 matrix multiplication over $\F$, file 333x23.tgz , http://www.algebra.uni-linz.ac.at/people/mkauers/333x23.tgz, SHA-256 bfe79080120ab9eb55e04126d943df7b 2c279544bf13ba623488a1f527ca1923 , retrieved 18 October 2026.link
  4. M. Kauers and J. Moosbauer, A normal form for matrix multiplication schemes , in: Algebraic Informatics -- CAI 2022, Lecture Notes in Comput. Sci. 13706, Springer, 2022, 149--160.
  5. J. D. Laderman, A noncommutative algorithm for multiplying 3×33\times 3 matrices using 2323 multiplications , Bull. Amer. Math. Soc. 82 (1976), 126--128.
  6. J. M. Landsberg and M. Michałek, Abelian tensors , J. Math. Pures Appl. 108 (2017), 333--371.
  7. The mathlib Community, The Lean mathematical library , in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), 2020, 367--381.
  8. B. D. McKay, Isomorph-free exhaustive generation , J. Algorithms 26 (1998), 306--324.
  9. V. Y. Pan, Methods of computing values of polynomials , Russian Math. Surveys 21 (1966), 105--136.
  10. R. C. Read, Every one a winner, or how to avoid isomorphism search when cataloguing combinatorial configurations , Ann. Discrete Math. 2 (1978), 107--120.
  11. I. Rudich and L.-M. Rousseau, Lower bound of 2222 for 3×33\times 3 matrix multiplication over Z\Z , arXiv:2610.01639, 2026; Lean proof at https://doi.org/10.5281/zenodo.23047901.arXivDOI
  12. V. Strassen, Gaussian elimination is not optimal , Numer. Math. 13 (1969), 354--356.
  13. B. Tahir, A certificate-based conditional lower bound of 2121 for 3×33\times 3 matrix multiplication over $\F$ , public review draft, 2026, https://github.com/btahir/rank21-f2-review.link
  14. C. Wang, Automated lower bounds for bilinear complexity over finite fields , arXiv:2603.07280, 2026.arXiv
  15. C. Wang, A lower bound of 2121 for 3×33\times 3 matrix multiplication over $\F$ , arXiv:2609.06725, 2026.arXiv
  16. S. Winograd, On multiplication of 2×22\times 2 matrices , Linear Algebra Appl. 4 (1971), 381--388.
  17. S. Yang et al., A structural proof of the lower bound 2121 for 3×33\times 3 matrix multiplication over $\F$ , arXiv:2609.18722, 2026.arXiv

Version history

  1. v1Submitted by Tejasvi Singh TomarInitial depositCurrentOct 26, 2026