Over F₂, does multiplying a 2×3 matrix by a 3×4 matrix really need 20 scalar multiplications, or can 19 do it?
Multiplying a 2×3 matrix by a 3×4 matrix takes at most 20 scalar multiplications, by an algorithm Hopcroft and Kerr gave in the late 1960s. They conjectured that 20 is also necessary, but did not prove a lower bound of 19 or 20. Over the field with two elements, where addition is XOR and the only nonzero scalar is 1, Wang proved a machine-checked lower bound of 19 earlier this year. That left the exact rank open in the two-point set {19, 20}.
This paper closes it: the exact F₂ rank is 20.
Matrix multiplication rank in ninety seconds
A bilinear algorithm for matrix multiplication uses additions and products of linear forms, with no branching on the entries. Its rank is the number of those products. Over F₂, a rank-r algorithm is a sum of r triples, one per product, checked against the tensor's 576 coefficients (24 of them nonzero) that record which input products feed which output entry.
What we found
The upper bound is the exact AlphaTensor F₂ decomposition, extracted from its public factorization file and checked against all 576 coefficients of the 6×12×8 tensor. The new step is the lower bound: excluding rank 19 entirely.
How rank 19 is excluded
Wang's checked first-factor capacities force all 19 first factors in any hypothetical 19-term decomposition to be pairwise distinct. A 62,267-variable CNF with a checked DRAT/LRAT proof pair proves that at most one can have matrix rank two; exhaustive enumeration of 56,070 candidates then reduces the possibilities to exactly 252 legal profiles in four symmetry orbits.
Row restriction excludes all four. Restrict the first matrix to one row: when exactly 12 terms survive, every surviving output factor is forced into a shared four-dimensional row space. For the (7,7,5) orbit, two active term sets share five nonzero output factors, but their associated row spaces intersect only at zero. When 13 terms survive, there is a unique one-dimensional relation among them, and uniqueness of nonzero pure-tensor factorization over F₂ would force six quotient tensors with distinct first factors to be equal, a contradiction for both (7,6,6) orbits.
The last orbit (18 rank-one factors plus one of rank two) needs at least 18 support incidences across its three row restrictions, but each restriction can carry at most 3. Nine is not eighteen, so the fourth orbit falls too.
Why the verification is strong
A clean-extraction replay outside the repository fetched and hash-checked every pinned source, rebuilt the proof checkers, freshly replayed the 191 MB DRAT and 279 MB LRAT proof pair, and returned all 252 excluded profiles, rank 20, and the 20-term upper witness. It passed the exact evaluator's 576-coefficient control, all 35 unit tests, and recompiled the paper. A separate independent referee re-derived the row-restriction argument and repeated the focused exact checks and prior-art search.
Earlier exact SAT searches (native-XOR, Tseitin, CEGAR, and cubed encodings across several solvers) stalled for hours at the same residual frontier. The proof only emerged after restricting the first matrix to a single row, where a hypothetical decomposition meets a flattening lower bound with zero or one excess term. Exact code checks every profile case against the independently reviewed row-restriction lemmas.
Beyond, the research system operated by Nth Research Collective, materially assisted with literature retrieval, hypothesis generation, the finite exclusion search, exact controls, and adversarial review. Research systems are not authors; the author made the final scientific judgments and accepts full responsibility.
What this does and doesn't establish
The result is exact for this one small format over one field. It does not determine the exact rank of this tensor over other fields; Nazarov and Smirnov's characteristic-zero result concerns approximate rank, a different notion. It does not change the asymptotic complexity of matrix multiplication or produce a faster practical algorithm; Hopcroft and Kerr's 20-multiplication algorithm already exists, and the format is tiny. The profile lemma is machine-checked with a DRAT/LRAT certificate; the row-restriction case analysis is reviewed and exact but not formalized in a proof assistant. It depends on Wang's public capacity certificate and its pinned replay. Wang's lower bound is correct, and the missing piece was the exclusion of rank 19, not an error in that bound. No earlier exact determination of the F₂ rank of this format was found in searches current to August 11, 2026. This is a public preprint, not peer-reviewed.
Read it, run it
Archived record (manuscript and certificates): doi.org/10.5281/zenodo.21895176
Verifier and certificates: github.com/Nth-Research-Collective/research — run python3 projects/f2-234-tensor-rank/verification/verify_all.py from the repository root.
If you know of an earlier equivalent result, please send it to research@nthresearch.org.