← All papers
First page of A 55-Addition Rank-23 Scheme for $3\times3$ Matrix Multiplication via Exact Two-Sided Minimization

A 55-Addition Rank-23 Scheme for $3\times3$ Matrix Multiplication via Exact Two-Sided Minimization

Greg Sidebottom

cs.MS Oct 20, 2026 · v1 cs.CC cs.DS cs.SC
Correctness of the 55-addition 3x3 matrix multiplication scheme is machine-checked in Lean 4, using Mathlib's Matrix API, over general non-commutative rings.
We give a scheme that multiplies two $3\times3$ matrices with 23 multiplications and 55 additions over any ring, one addition below the previous record of 56 (Sun, 2026) and the first below 56 for exact non-commutative $3\times3$ multiplication without a change of basis. The scheme forms 13 signed combinations of the entries of A and 14 of B, takes 23 products, and recombines them with 28 further additions; its correctness is machine-checked in Lean 4. The previous records, from 60 down to 56, were obtained by greedy common-subexpression elimination, which only bounds each side of a scheme from above. We minimize both input sides exactly by chain covering, and the output side exactly through the transposition principle: the 9-by-23 output map costs its transpose plus 14, and the transpose is a 9-input map that the input-side minimizer solves exactly. Applied to Perminov's cn122 scheme (class i19w225c4efh, published at 58 additions) this gives 55 = 13 + 14 + 28, where greedy elimination reaches only 29 on the output side. The same method shows that Sun's representative is output-optimal at 56, and an exact orbit-wide computation over the Heule-Kauers-Seidl database shows that the record class is the only database class attaining 55.

The known record for exact non-commutative 3x3 matrix multiplication with 23 multiplications and no change of basis was 56 additions. Earlier records came from greedy common-subexpression elimination, which only gives upper bounds on each side's additive cost.

Both input sides are minimized exactly as addition-chain covering problems, using iterative deepening over helper values in a closure normal form. The output side is minimized exactly through the transposition principle, A(W)=A(W^T)+14, which turns it into an instance the input-side minimizer can solve. This is applied to Perminov's cn122 scheme. The resulting program is fuzz-tested and proved equal to A*B over any non-commutative ring in Lean 4 with Mathlib, sorry-free.

A rank-23 scheme with 55 = 13+14+28 additions is obtained. Sun's 56-addition representative is shown to be output-optimal. An exhaustive GF(2)-bound sweep over the Heule-Kauers-Seidl database shows that no published class reaches 54 and that only class i19w225c4efh attains 55.

ClassPublishedExact (A+B+C)
i19w225c4efh (Perminov cn122)5855 = 13+14+28
i46w213c23ci (Sun)5656 = 13+13+30
i12w219c23ci (Perminov cn119)5856 = 13+14+29
i19w203c23ci (MWS)5958 = 14+15+29
i2w201c26fi (Stapleton)6060 = 16+16+28
Exact additive totals per de Groote class (selected)