The matmul eval: model proposes, the machine certifies

Each bar is one campaign, split by what the grader did with each proposal. The band worth watching is REFUTED: a proposal that got past the float screen and then failed the exact tensor identity — the "almost right" failure that a digit-matched benchmark would have scored as a near miss and a human grader might have waved through.

Every row aggregates the append-only ledger; every underlying proposal carries its exact certificate. To put a model on this board, run ANTHROPIC_API_KEY=… python3 tools/llm-harness.py --family matmul --model <id> --n 40 --ledger certs/matmul-eval-ledger.jsonl from the repository, then rebuild this page. The red controls run first and ABORT the campaign if any forgery certifies — the eval refuses to produce numbers under a broken grader.

The aggregate board hides the shape of failure; this table is where it lives. The rungs are ordered easy to hard within each campaign: <2,2,2> r7 is Strassen 1969, r8 is the naive format rung, <2,2,3> r11 and <3,3,3> r23 (Laderman) test whether recall survives precision. Every count is read off the append-only ledger at build time.

Two corrections, applied here rather than hidden. The answered column counts only proposals the model actually returned: a reply cut off by OUR output budget is counted in its own column and kept out of every rate, because it measures what we paid for, not what the model can do. Counting those in the denominator is what this page did until 2026-08-31, and it published opus-5 at a 30% certified rate where the honest figure over rows it answered is 90%. And the prompt tag reading v4 (tagged effort-low; ran at DEFAULT effort) is a correction too: the harness dropped its --effort argument in campaign mode, so 90 rows carry a label that was never true. The rows are not rewritten — the ledger is append-only — so the correction lives in certs/matmul-eval-corrections.json and is applied at display time.

The rank of <2,2,2> is EXACTLY 7 — Winograd 1971, a consumed theorem this page names rather than proves — so no rank-6 decomposition exists, every submitted attempt provably fails exact grading, and the CORRECT response is a declared refusal. The prompt offers the refusal explicitly ({"impossible": true}) on every rung, so declining is never a trick option — and the last column is the control: a model that also declines the achievable rank-7 is refusing indiscriminately, not reasoning about rank. Attempts here are confabulation with a certificate attached: the grader does not just suspect the attempt is wrong, it proves it. A red control (truncated Strassen) runs against this rung every campaign and must never certify.

The recall-proof rung: the <2,2,2> tensor conjugated by a FIXED monomial transform — permutations and signs on the three index spaces, pinned in the harness source and stated here — and presented as a bare 4×4×4 tensor by its nonzero entries, never as matrix multiplication. Monomial transforms preserve rank, so rank 7 is achievable (the transformed Strassen witness is the green control that must certify before every campaign) and rank 6 is impossible by the same theorem. Reciting memorized Strassen fails the grader; recognizing the disguised structure and transporting a solution through it is the reasoning the plain rung cannot separate from recall. The gap between the last two columns is the recall gap, measured.

The cost asymmetry is itself the measurement. The plain rank-7 rung costs a capable model almost nothing — recall — while this rung, the SAME task up to relabeling, spends real output on every proposal: the largest single reply in this ledger is 4k tokens, and replies cut off by OUR budget are recorded under their own name and kept out of every rate on this page. Removing the label converts a free lookup into genuine derivation — which is exactly what an anti-recall rung is for. Corrected 2026-08-31: this paragraph used to say the 2026-08-27 campaigns ran under 16k and 32k output budgets. Nothing in this ledger records an output above 4k, so that claim was not ours to make and the figure is now computed from the record.

Whether 3×3 matrices multiply in 22 products is an open problem: Laderman's 23 has stood since 1976, the lower bound is 19, and nobody knows which side is right. This rung is labeled accordingly — no model is penalized for failing it, a declared refusal is a defensible answer, and a certified row would be a discovery this page renders in bold rather than a score. It exists because an eval whose grader is a certifier can ASK open questions safely: the one thing that cannot happen is a false positive.

The disguise rung generalized from one fixed transform to a FAMILY: the <2,2,2> tensor conjugated by seed-pinned random unimodular integer matrices on each index space (instance c1 here; every new tag mints another). Unimodular actions preserve tensor rank, so rank 7 stays achievable — the transported Strassen witness is the green control that must certify — and rank 6 stays impossible by the transported theorem. RAW Strassen runs as a red control that must fail: on this rung, recall provably scores zero, and a certified row is a derivation by construction. Because instances are minted from a seed, this is a benchmark that cannot be contaminated by its own publication — the same property the Forecast Gym gets from time, obtained here from algebra.

The first campaign hit a measured wall. On the fixed d7 disguise, opus-5 certified. On instance c1 — denser after conjugation, entries to |8| — opus-5 and sonnet-5 returned empty text on every attempt, exhausting the output budget (those replies are recorded under their own name and kept out of every rate on this page); haiku attempted every time and was exactly rejected every time. So the honest current record on this rung is the table above: recall scores zero by construction, and derivation has not yet fit inside any budget this harness can buy. Streaming support for deeper budgets is the named next step; fresh seeds wait either way.