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
TL;DR
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.
Abstract
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.
Problem
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.
Approach
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.
Results
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.
| Class | Published | Exact (A+B+C) |
|---|
| i19w225c4efh (Perminov cn122) | 58 | 55 = 13+14+28 |
| i46w213c23ci (Sun) | 56 | 56 = 13+13+30 |
| i12w219c23ci (Perminov cn119) | 58 | 56 = 13+14+29 |
| i19w203c23ci (MWS) | 59 | 58 = 14+15+29 |
| i2w201c26fi (Stapleton) | 60 | 60 = 16+16+28 |
Exact additive totals per de Groote class (selected)