51 Additions per Recursive Step for Rank-23 $3\times3$ Matrix Multiplication, Machine-Checked over Arbitrary Rings
Greg Sidebottom
cs.MS
Oct 17, 2026 · v1
cs.CC cs.DS cs.SC
TL;DR
Lean 4/Mathlib kernel-checked proofs that the 51-addition rank-23 3x3 scheme computes AB over arbitrary rings, plus a class-optimality proof via decide.
Abstract
We present a rank-23 bilinear scheme for $3\times3$ matrix multiplication that uses 51 additions per recursive step in the alternative-basis (Karstadt-Schwartz) cost model, one below Nielsen's 52 (arXiv:2609.06588). The count 51 itself was first posted, on a different scheme, by Stapleton and Perminov (arXiv:2609.32388), found by heuristic sparse-basis search; the present work is independent and complementary: exactness and breadth rather than a single construction. The scheme is valid over every ring, so it recurses on block matrices, and its correctness is machine-checked in Lean 4/Mathlib. The count is exactly optimal for the scheme's equivalence class: we introduce an exact free-basis minimization procedure whose negative answers are exhaustion proofs, and use it to show that 51 is the minimum for this class, that 52 is exactly optimal both for Nielsen's class and for the class of the current flat-model record, and to sweep the complete Heule-Kauers-Seidl database of rank-23 classes. The sweep is complete: exactly four classes attain 51, all in a single HKS invariant family. We machine-check Stapleton and Perminov's scheme as well, and prove in Lean that their 51 is optimal for its class. Separately, we document a systematic gap between $\mathbb{F}_2$ and signed optima: the $\mathbb{F}_2$-optimal chains of a class typically admit no sign assignment under most of the class's integer sign models, and certificate lifting fails where a direct signed search succeeds.
Problem
Rank-23 bilinear schemes for 3x3 matrix multiplication are compared by their additive cost per recursive step in the alternative-basis (Karstadt-Schwartz) model. Two questions are open: whether fewer than 52 additions is achievable over arbitrary rings, and what is exactly optimal for each equivalence class.
Approach
An exact free-basis minimization procedure computes optimal leg addition chains. Its negative answers are finite exhaustion proofs, and its positive answers emit certificates that an independent checker replays. Integer sign models are found by SAT so that schemes are valid over rings. The resulting scheme, and Stapleton and Perminov's scheme, are machine-checked in Lean 4 against Mathlib's matrix product. A separate Lean proof shows the class optimality of Stapleton and Perminov's 51 by counting sum triples, with finite facts checked by decide.
Results
The scheme found uses 51 additions per step (legs 12, 13, 12) and is optimal for its class. A full sweep of the Heule-Kauers-Seidl database finds exactly four classes attaining 51, all in one invariant family. The work also documents a systematic gap between F2-optimal and signed (ring-valid) optima.
| class | legs | ring-valid | conversions | one-shot | Lean |
|---|
| i12w211c23fg | (12,13,12) | yes (sign model 21) | 11 | 62 | Ring51.lean |
| i12w219c23fg | (11,13,13) | open (F2 only) | — | — | — |
| i12w219c23ci-008 | (13,12,12) | yes (published) | 5 | 56 | SP51.lean |
| i12w227c23ci-012 | (14,12,11) | yes (sign model 15) | 17 | 68 | — |
The four 51-addition classes