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 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. Mathematics Subject Classification (2020): 68Q17, 15A69; 68V05, 68V15. Supplementary file rank333-f2-v3-collection-check.zip: the programs and results of the check of the collection of schemes of length 23 of M. Kauers (Section 3.4 and Table 4 of the paper). The collection itself is not included; it is at http://www.algebra.uni-linz.ac.at/people/mkauers/333x23.tgz.

The authors’ abstract, as arXiv lists it. arXiv’s listings, abstracts included, are free for anyone to reuse.

More in Computational Complexity

• arXiv preprint · 8 October 2026

  A structure-preserving neural density functional for the ions of a polymer electrolyte

  Liyao Lyu
• arXiv preprint · 9 October 2026

  Block encoding of semiseparable matrices via their generators

  Giacomo Antonioli, Gianna M. Del Corso and Roel Van Beeumen
• arXiv preprint · 8 October 2026

  asdex: Automatic Sparse Differentiation in JAX

  Adrian Hill and Guillaume Dalle
• arXiv preprint · 9 October 2026

  Sustainable Cloud-Fog-Edge Systems for Smart Buildings: Algorithmic Adaptation under Memory Constraints and Dynamic Orchestration Strategies

  Mamadou Sow and Christophe Cerin
• arXiv preprint · 8 October 2026

  Mesh-Native Tokenisation: Retrofitting Foundation Models to Unstructured Data

  Georg Maierhofer, Miles Cranmer and Payel Mukhopadhyay

All new papers in Computational Complexity