The matmul eval: model proposes, the machine certifies

Mathematical ground truth usually inherits the failure class of whatever computed it — the failure taxonomy on this site exists because digit-matched reference values shipped a float artifact as a constant. Here the reference is not a value at all: the task is to EXHIBIT a witness (a decomposition), and the grader re-derives the claim from the witness alone, exactly. Grading a proposal means checking Σᵣ u[r][a·m+b] · v[r][c·p+d] · w[r][e·p+f] against the matmul tensor at every index — a finite, exact computation with no tolerance anywhere. The eval cannot be gamed by memorizing digits, and it cannot false-accept: both directions of every verdict are theorems.

Five outcomes per proposal, and all five are informative: MALFORMED (the reply did not parse), REJECTED (the prune-only float screen caught a shape or gross-value error), REFUTED (well-formed, plausible to the screen, exactly false — the bucket digit-matching cannot see), CERTIFIED (exactly true), UNDECIDED (never occurs here; the identity is always decidable). The headline number is the SURVIVOR TRUTH RATE: of proposals that looked right to a float screen, how many were actually true.

The prompt states the convention completely: A is n×m and B is m×p, both vectorized row-major; a decomposition is three lists u, v, w of at most R rows, entries integer or exact fractions; the claim is C[i][k] = Σᵣ w[r][i·p+k] · ⟨u[r], vec A⟩ · ⟨v[r], vec B⟩ for ALL A, B. The grader checks the equivalent finite identity — every (a,b,c,d,e,f) index of the tensor — in exact rational arithmetic, plus the rank bound. The float screen (shape checks and one random spot-multiplication at tolerance 1e-6) may only PRUNE; nothing it passes is believed. Rung one (rank 8 = naive) tests format-following; rank 7 is Strassen 1969; the upper rungs test whether recall survives precision. Achievable ranks only — every rung has a witness on record.

The eval is open-scaffold: the task is defined by the GRADER, not by a prompt. Use any model, any provider, any agentic scaffold, any thinking budget — the certificate does not care how the witness was found, and the tag field records what you used.

Anthropic models run directly: ANTHROPIC_API_KEY=… python3 tools/llm-harness.py --family matmul --model <id> --n 40 --tag <yours> --ledger certs/matmul-eval-ledger.jsonl.

Anything else goes through the submission path: generate proposals however you like, write one JSON line per attempt — {"target": "(2, 2, 2, 7)", "proposal": "<the model's raw reply>"} — and grade the file with python3 tools/llm-harness.py --family matmul --proposals yours.jsonl --model-label <name> --tag <yours> --ledger …. Same float screen, same exact certifier, same red controls, run before any grading; a target outside the published ladder is refused, so a submission cannot smuggle in an easier task.

To land on the public board, open a pull request carrying the PROPOSALS file, not graded rows — grading is deterministic, so rerunning it here reproduces your outcomes bit for bit, and the board never has to trust a submitted verdict. The one thing a submission is trusted about is its own attribution: the model name and the scaffold the tag describes.