The AI-discovered algorithms, certified

"4×4 matrices in 48 multiplications" is not an empirical claim about software — it is a rank-48 decomposition of the ⟨4,4,4⟩ matmul tensor: three factor matrices U, V, W whose defining identity, 4,096 equations each an exact sum of 48 products, either holds over the stated ring or provably does not. That makes the most famous AI-discovered mathematics of 2022 and 2025 exactly the shape this machine certifies: transcribe the published artifact from pinned bytes, check every equation in exact arithmetic, and record the verdict with the hash of what was checked.

The C-index layout (row-major or transposed) is a publishing convention that differs between sources; the audit DETECTS it and the certificate states it — nothing about the identity is assumed. And the rank bar is enforced: the naive rank-8 algorithm certifies as correct and is REJECTED, because a hit here asserts rank strictly below naive. Correct is not fast.

The only first-party byte source for AlphaEvolve's decomposition is a Jupyter notebook in a DeepMind repository whose main branch is MUTABLE — it has been rewritten seven times since May 2025. The audit therefore pins by commit: the notebook is held at sha256 2cce2543e48c89aa…, re-hashed at every certify, and the arXiv paper (2506.13131) carries no ancillary files — it is the citation, not the source. A "certified" claim about bytes that can silently change is not a certificate; the pin is what makes the verdict durable.

The ring matters. Every published entry lies in ½·Z[i] — coefficients from {0, ±½, ±½i, ±½±½i} — which is exact in float32, so the byte-level parse loses nothing. Clearing denominators gives factors 2U, 2V, 2W over the Gaussian integers, and the certified claim is the scale-8 identity: Σᵣ (2uᵣ)⊗(2vᵣ)⊗(2wᵣ) = 8·T⟨4,4,4⟩, all 4096 equations exact, every imaginary part vanishing identically. Verdict, re-derived this build: CERTIFIED, rank 48 < 49.

AlphaTensor's headline rank-47 ⟨4,4,4⟩ algorithm works modulo 2 — the Nature paper says so. This audit converts the caveat into a decided pair: the SAME pinned factors are audited over F2 (VERIFIED, all equations exact) and over Q (REFUTED — the identity fails at a named index). The speedup over Strassen-squared's 49 provably does not survive lifting to characteristic 0. That is a theorem about the published artifact, produced mechanically, and it is the kind of statement a rerun or a benchmark cannot make: running the algorithm on test matrices over Z would just quietly give wrong answers that round-trip mod 2.

Seven further AlphaTensor factorizations from the pinned npz — ⟨2,2,2⟩ through ⟨5,5,5⟩, over Q and over F2 — verify exactly and appear in the registry below with their equation counts.

Both artifacts were produced by systems whose outputs cannot be trusted by construction and were verified by their authors' own pipelines. This page is the independent layer: different code, exact arithmetic, pinned bytes, red controls, and a verifier a stranger can run in seconds without this machine. The marginal cost of certifying the next published decomposition is minutes — which is the argument of this whole site, applied to the most cited AI-mathematics artifacts there are.

The same corpus is the ladder for the live eval: models are asked to EXHIBIT decompositions and the same instrument grades them — see the matmul eval, where ground truth is a proof because these identities are always decidable.