cert-machine · both walls · an independent audit of someone else's certificate

The rank of 3x3 matrix multiplication, audited from both sides

Laderman multiplied two 3x3 matrices in 23 multiplications in 1976 and nobody has done better since. The lower bound sat at 19 from 2003 until March 2026, when it moved to 20 over F2 — in a preprint whose proof is a machine-checkable certificate, on a repository with two stars. This page re-verifies that certificate here, in exact arithmetic, with an instrument that could have contradicted it.

tl;dr
  • The finding. The certificate behind R_F2(<3,3,3>) ≥ 20 holds everywhere we attacked it: 18 of its 496 nodes were genuinely attacked and 0 were refuted. 4 are now proved TWO-SIDED here — for those, none of the paper's four inference rules is trusted at all. The honest limit is the other 478 nodes (96.4%), which this instrument cannot yet reach and which still rest on his reasoning.
  • The mechanism. We did not reimplement his proof. A verifier that re-runs an author's own inference rules can only ever AGREE with him. This instrument computes GROUND TRUTH instead — the true minimum rank of each constrained sub-tensor, over F2 — and asks whether his number is the truth. A method that can DISAGREE is worth strictly more than one that cannot. Two things his certificate never documents, the constraint semantics and the transposed c-index convention, were recovered from the bytes.
  • Check it. python3 instruments/tensorlb/battery.py — 12 checks and 3 red controls, all of which must fire; the audited bytes are pinned at sha256 25595a883ce877ee…, which is the git-lfs object id the author published upstream.
the interval, today
20 ≤ R ≤ 23
lower bound Wang 2026 over F2 (was Blaeser 19, 2003); upper bound Laderman 1976. Both walls re-verified by this machine
nodes attacked
18 of 496
a genuine attempt to find a cheaper decomposition than the certificate claims
refuted
0
no node admitted a decomposition below its claimed bound
proved two-sided here
4
rank == the claimed bound, computed exactly; the author's inference rules are not relied on for these
still on his reasoning
478
dimension > 2; beyond this instrument. Stated here rather than buried
control certificate
10/10 witnesses
<2,2,2>, where rank 7 has been known optimal since Winograd 1971 — every witness re-verified against a sub-tensor we rebuilt ourselves
§1 · the two walls

What is actually known about R(&lt;3,3,3&gt;)

wallvaluewho, whenstatus here
upper bound (any field)23Laderman 1976a rank-23 witness is pinned in certs/strassen-certificate.json and re-certified at every build
lower bound (F2)20Wang, arXiv:2603.07280, March 20264 of 496 certificate nodes proved two-sided here; 0 refuted
lower bound (any field)19Blaeser 2003not audited here — the 20 is an F2 statement and does not supersede it
border rank (over C)≥ 17Conner–Harper–Landsberga different quantity; never quote it as a rank bound

The gap is real and old: nobody has moved 23 in fifty years, and until this March nobody had moved 19 in twenty-three. A rank-22 algorithm, incidentally, would not even beat Strassen asymptotically — log₃22 > log₂7 — which is why the exhaustive-search literature deliberately stops at 21.

§2 · the audit

Ground truth, not a second opinion

certificatenodeswitnesses re-verifiedproved two-sidedattackedrefuted
&lt;2,2,2&gt; control (rank 7 known optimal)1010 / 10370
&lt;3,3,3&gt; — the new bound4964180

The control matters more than it looks. Its final node is the unconstrained <2,2,2> tensor with a claimed bound of 7 — a number Winograd proved optimal in 1971. Had our search found a rank-6 decomposition there, the search would have been broken, not the mathematics. It did not.

The <3,3,3> certificate carries no upper-bound witnesses at all, so there is nothing to cross-check against: it is a pure lower-bound argument across 496 nodes resting on four inference rules. That is exactly why computing ground truth independently is the right audit and reimplementing his rules is the wrong one.

what this page does NOT claim

No new mathematics was discovered here. We found no refutation, no better bound and no counterexample; 478 of 496 nodes were never attacked and still depend entirely on the author's reasoning. What this page claims is narrower and, we think, still worth publishing: the first independent check of any part of a new lower bound on a fifty-year-old open problem, by a different implementation, in a different language, from the author's published bytes. Published, not peer-reviewed, not independently rerun — and that last phrase is precisely what this page exists to stop being true of someone else's work.