First-hand information for everyone
The paper presents a concrete scheme that multiplies two 3×3 matrices using 23 multiplications and 55 additions over any ring. It improves the prior additive record of 56 by one and is reported as the first sub‑56 scheme for exact non‑commutative 3×3 multiplication without a change of basis.
The algorithm forms 13 signed linear combinations of A’s entries and 14 of B’s entries. It takes 23 pairwise products of those combinations and recombines the products with 28 further additions, totaling 13+14+28 = 55.
Both input and output additive costs are minimized exactly. Input‑side minimization is an exact chain‑covering search implemented in sidemin.py. The search uses a closure normal form and iteratively deepens over the number of helper values. Output‑side minimization applies the transposition principle: for an addition‑only linear map W, A(W) = A(W^T) + inputs(W) − outputs(W). This reduces the 9×23 output problem to a 9‑input problem that the input minimizer solves; the process is constructive and is implemented in tcmin.py.
Applied to Perminov’s cn122 representative (de Groote class i19w225c4efh), the method yields input sides 13+14 and an exact output side 28 (greedy CSE returned 29), producing the 55 = 13+14+28 scheme. The explicit straight‑line program is provided and tested.
The implementation is runnable (src/mm55.rs and matmul/external/i19-55adds-slp.txt). It was checked against the naive 27‑multiplication triple loop on 500,000 random integer inputs and 50,000 non‑commutative 2×2‑block inputs. An operation counter confirmed exactly 23 multiplications and 55 additions. The scheme’s correctness is machine‑checked in Lean 4. Artifacts (program, verifier, Lean proof, repository snapshot) are archived at the cited DOI.
Context. Earlier additive records (60 down to 56) were obtained by greedy common‑subexpression elimination (CSE), which provides only upper bounds per side. The two‑sided exact minimization here finds the missing addition on the Perminov representative and improves the record by one. The authors also report that Sun’s published representative remains output‑optimal at 56 (13+13+30) under the same model.
Independent report. Karunaratne and Idamekorala independently reported a 55‑addition, rank‑23 scheme with the same tensor and the same 13+14+28 split and transposed output construction.
Scope and limitations. The cost model counts binary additions/subtractions in a straight‑line program; unary negation is free and no change of basis is allowed. Computing the exact additive minimum for a general linear map is NP‑hard, so greedy CSE can miss the true minimum. The optimality statement is relative to the published catalogue of 17,376 classes: within that catalogue no representative with rank‑23 attains fewer than 55 additions. A sub‑55 scheme would require a rank‑23 class not in that catalogue or a different cost model (for example, genuine dyadic coefficients).
Reproducibility notes. sidemin.py reproduces Sun’s input‑side optima and impossibility certificates, validating the input‑side search. Deterministic caveats include that kissat may return different sign models across versions (each returned model is Z‑verified). Some Lean proofs depend on classical axioms as noted in the reproduction instructions. The committed representative and the emitted SLP make the 55 count deterministic to check.
Overall, the work provides a concrete, machine‑checked 23×/55‑additions scheme for 3×3 matrix multiplication over any ring, documents exact two‑sided minimizers that locate the savings, and supplies tests and formal proofs under a clear cost model.