TejasviTomar
October 2026 · Preprint

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

Tejasvi Singh Tomar

In plain words

A shortcut for multiplying small tables of numbers (matrices) can be applied to large ones cut into blocks. For 4×4 tables of bits, where addition is done without carrying, the best shortcut known uses 47 multiplications and was found by a computer search in 2022. In 2003 Bläser proved that any such shortcut needs at least 34 multiplications, a bound that stood for over twenty years until this paper raised it to 35. The key step uses exhaustive computer searches to show that any shortcut for multiplying a 3×3 table of bits by a 3×4 one needs at least 27 multiplications.

Abstract

We prove that the rank of the 4×4 matrix multiplication tensor over F2 is at least 35; the previous lower bound was 34. The bound follows by substitution from RF2(⟨3,3,4⟩) ≥ 27, which also gives RF2(⟨3,4,4⟩) ≥ 31. Each of the three bounds is one more than what follows from RF2(⟨3,3,3⟩) = 23. A flattening argument reduces the bound for ⟨3,3,4⟩ 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.

A tree of cards on white. A central card with a 3-by-3 grid holding one teal square and two black dots is joined by lines to thirteen cards, seven on the right and six on the left, each showing a magenta 3-by-4 grid and a yellow 3-by-4 grid. Each of these leads to a card with a teal 3-by-3 grid and one to three dots, filled or open, followed by a short vertical bar.
For the quotient by the span of the rank-two matrix v₂, the search has a single leaf; this illustration shows the 14-node certificate that refutes the leaf (Section 6). The middle card is the root, which branches on the term whose first factor is E₀₂ (teal grid). The root’s 13 branches are the candidates for that term’s pair (b, c), with b in magenta and the transpose of c in yellow. Each child card shows the first factor of the term it branches on next. No candidate remains for any of these terms, so a bar marks each branch as closed. The dots are the 31 rank claims that the checker verifies. Each concerns a functional X: a filled dot claims rank R_X = u_X, and an open dot claims rank R_X = u_X − 1.