HEXAGONbeta

The rank of 4×4 matrix multiplication over F2 is at least 35

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 / Nov 12, 2026 / CC BY 4.0

Abstract

We prove that the rank of the 4×44\times4 matrix multiplication tensor over F2\mathbb{F}_2 is at least 3535; the previous lower bound was 3434. The bound follows by substitution from RF2(⟨3,3,4⟩)≥27\mathrm{R}_{\mathbb{F}_2}(\langle 3,3,4\rangle)\ge27, which also gives RF2(⟨3,4,4⟩)≥31\mathrm{R}_{\mathbb{F}_2}(\langle 3,4,4\rangle)\ge31. Each of the three bounds is one more than what follows from RF2(⟨3,3,3⟩)=23\mathrm{R}_{\mathbb{F}_2}(\langle 3,3,3\rangle)=23. A flattening argument reduces the bound for ⟨3,3,4⟩\langle 3,3,4\rangle to lower bounds for two quotients of the tensor, by the span of a matrix of rank two and by the span of a matrix of rank three. These come from exhaustive searches over the possible patterns of a short decomposition, pruned by lower bounds for quotients by larger subspaces. The whole argument, including every step of the searches, is checked in the proof assistant Lean 4, with one compiled evaluation of a verified certificate checker.

Author comments: Published on Zenodo: https://doi.org/10.5281/zenodo.23749576

References

  1. M. Bläser, Lower bounds for the multiplicative complexity of matrix multiplication , Comput. Complexity 8 (1999), 203--226.
  2. M. Bläser, On the complexity of the multiplication of matrices of small formats , J. Complexity 19 (2003), 43--60.
  3. I. D'Ambrosio, The exact $\Ft$-rank of 2×32\times 3 by 3×43\times 4 matrix multiplication , Zenodo, 2026, https://doi.org/10.5281/zenodo.21895176.DOI
  4. 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.
  5. A. Fawzi et al., Discovering faster matrix multiplication algorithms with reinforcement learning , Nature 610 (2022), 47--53.
  6. Q. Huangfu and J. A. J. Hall, Parallelizing the dual revised simplex method , Math. Program. Comput. 10 (2018), 119--142.
  7. 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.
  8. J. D. Laderman, A noncommutative algorithm for multiplying 3×33\times 3 matrices using 2323 multiplications , Bull. Amer. Math. Soc. 82 (1976), 126--128.
  9. J.-G. Dumas, C. Pernet and A. Sedoglavic, A non-commutative algorithm for multiplying 4×44\times4 matrices using 4848 non-complex multiplications , arXiv:2506.13242, 2025.arXiv
  10. 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.
Show all 19 referencesShow fewer references
  1. A. Novikov et al., AlphaEvolve: a coding agent for scientific and algorithmic discovery , arXiv:2506.13131, 2025.arXiv
  2. V. Y. Pan, Methods of computing values of polynomials , Russian Math. Surveys 21 (1966), 105--136.
  3. I. Rudich and L.-M. Rousseau, Lower bound of 2222 for 3×33\times 3 matrix multiplication over Z\mathbb{Z} , arXiv:2610.01639, 2026.arXiv
  4. A. V. Smirnov, The bilinear complexity and practical algorithms for matrix multiplication , Comput. Math. Math. Phys. 53 (2013), 1781--1795.
  5. V. Strassen, Gaussian elimination is not optimal , Numer. Math. 13 (1969), 354--356.
  6. T. S. Tomar, The rank of 3×33\times 3 matrix multiplication over $\Ft$ is 2323 , arXiv:2610.11823, 2026.arXiv
  7. C. Wang, Automated lower bounds for bilinear complexity over finite fields , arXiv:2603.07280, 2026.arXiv
  8. C. Wang, A lower bound of 2121 for 3×33\times 3 matrix multiplication over $\Ft$ , arXiv:2609.06725, 2026.arXiv
  9. S. Yang et al., A structural proof of the lower bound 2121 for 3×33\times 3 matrix multiplication over $\Ft$ , arXiv:2609.18722, 2026.arXiv

Version history

  1. v1 · 11 pagesSubmitted by Tejasvi Singh TomarPublished on Zenodo: https://doi.org/10.5281/zenodo.23749576CurrentNov 12, 2026