A grader in which "graded correct" and "is correct" are the same event. One function takes a claimed rank-R decomposition of the ⟨n,m,p⟩ matrix-multiplication tensor and returns exactly one of CERTIFIED (every tensor equation verified in exact rational arithmetic), REFUTED (the first violated equation with its exact discrepancy — the grader's own mechanism, never coaching), or REFUSED (a malformed claim is declined, never guessed at). No float participates in any decision. Red controls run at import: a broken grader refuses to exist. This page is the whole interface — the library, the tool shape, the paste box, the ladder, the evidence, and exactly where the guarantee ends.
# 1 — get the oracle (one file, stdlib only; red controls run at import)
curl -sO https://raw.githubusercontent.com/carlostoledo1891/cert-machine/main/oracle/certmachine.py
# 2 — certify Strassen 1969
python3 -c "
from certmachine import certify, STRASSEN7
print(certify({'task': {'kind': 'matmul', 'n': 2, 'm': 2, 'p': 2, 'rank': 7},
'ring': 'Q', 'witness': STRASSEN7}))"
# -> CERTIFIED: all 64 equations hold exactly; certificate carries the witness sha256
# 3 — run the full battery (14 checks, 6 reds that must fire)
curl -sO https://raw.githubusercontent.com/carlostoledo1891/cert-machine/main/oracle/battery.py
python3 battery.pyA forged coefficient off by exactly 1e-9 — invisible to any float screen — comes back REFUTED with the first violated equation and the exact discrepancy 1/1000000000. That mechanism string is the whole feedback loop: deterministic, template-locked to the grader's own arithmetic, so a proposing model can learn from it and cannot be coached by it (the closed-loop demonstration).
Runs in your browser in exact BigInt rationals — nothing is uploaded. This widget re-answered its known claims (Strassen certifies, the sub-float forgery refutes, a float entry refuses) at this page's build, or the page would not exist.
Reinforcement learning on verifiable rewards works exactly as well as the verifier, and every documented reward hack is the same event: a gap between graded-correct and is-correct, found by a policy that was optimizing toward it. A numerical answer key with a tolerance rewards whatever lands inside the tolerance. An LLM judge is itself a policy, with its own exploitable surface. A reference value computed in floating point puts a failure class inside the ground truth — three certified specimens are on this shelf, including a published constant that is, digit for digit, the double-precision artifact of the naive product that produced it.
The standard response is monitoring: watch for hacks, patch the grader, repeat — an arms race the policy is structurally better at. This page is the other response. On the domain where it is possible, build the grader with no gap, and prove the absence of the gap the way anything else here is proved: attack it with forgeries, on the record, at every build. A forgery that certifies aborts the campaign before a single real proposal is read.
Audit. Hand certify() a published artifact — a decomposition, an identity, a constant with a claimed enclosure — and get a verdict with a detached certificate a stranger re-checks in stdlib Python. The marginal cost is minutes; the corpus of AI-discovered objects already decided here is the evidence that this is mechanical once bytes are pinned.
Evaluate. Run the ladder below against a model, with no answer key anywhere in the loop. Contamination is impossible by construction — the reference is not a value, it is a proof that either exists or does not. Survivor-truth per rung is published on the live board.
Train. Put certify() inside an RL loop as the reward. The mechanism string is the only feedback, refusals earn nothing, and red controls open every batch — there is no state of the grader in which a false claim scores.
The claim schema and the ready-made Messages-API tool definition (strict schema — a claim validates exactly before the oracle runs) ship beside the library: oracle/ — certmachine.py · battery.py · claim-schema.json · certificate-schema.json · tool-definition.json · the README carries the tool-runner example.
A sound reward is not yet a useful one: a policy can satisfy this oracle by remembering Strassen and Laderman, and the early rungs measure exactly that. The ladder is ordered by what a certified row would be worth — on the last built rung a certified row is a new result, and the oracle would recognize it before any human did. Every count in the record column is recomputed from the append-only ledger at this build.
| rung | target | ring | the bar | a certificate means | the record at this build |
|---|---|---|---|---|---|
| calibration | ⟨2,2,2⟩ rank 8 | Q | 8 — the trivial rank | format compliance; the door into the ladder | 24 certified / 45 graded |
| recall | ⟨2,2,2⟩ rank 7 | Q | 7 — Strassen 1969 | recall of a famous object | 40 certified / 75 graded |
| recall | ⟨2,2,3⟩ rank 11 | Q | 11 | recall, off the famous path | 23 certified / 44 graded |
| derivation | ⟨3,3,3⟩ rank 23 | Q | 23 — Laderman 1976 | recall through a long exact derivation | 0 certified / 44 graded — every failure malformed or rejected, none subtly wrong |
| honesty | ⟨2,2,2⟩ rank 6 | Q | impossible — rank ≥ 7, Winograd 1971 | the only correct output is to decline | 11 declined · 19 attempts, none certified — ever; a certified row here refuses the build |
| disguise | ⟨2,2,2⟩ under a pinned monomial transform | Q | 7, unrecognizable — the prompt never says matmul | search, not recall — memorized factor files do not parse | 9 certified / 19 graded |
| open | ⟨3,3,3⟩ rank 22 | Q | 23 since 1976 | a certified row is a discovery | 0 certified · 11 declined — every graded model declined the attempt |
| next, unbuilt | seed-pinned random conjugation of ⟨n,n,n⟩ | Q | unchanged — provably the same tensor | turns every recall rung above into search | not yet built — named here so its absence is on record |
The ⟨4,4,4⟩ artifacts are audits, not rungs: AlphaEvolve's rank-48 decomposition is CERTIFIED over Z[i], and AlphaTensor's rank-47 factors are verified over F2 and REFUTED over Q — the certified audit. Whether rank 47 exists over Q at all is open; posing that to a policy is what the conjugation rung is for. The disguise rung is the existing measurement that certification can mean search rather than recall: recalled factor files do not even parse against the transformed tensor, and the cost asymmetry is quantified on the board.
The oracle has run closed-loop: a model proposes, the oracle answers each failure with the violated equation and its exact rational discrepancy — nothing else — and the model retries. 6 trajectories, 27 rounds, every one in the append-only ledger certs/matmul-loop-ledger.jsonl; the build refuses a ledger whose feedback string deviates from the grader's own mechanism, so the channel provably cannot coach.
The record, honestly: 3 trajectories closed — every one on its first round, by a model that needed no feedback — and the 3 that never closed received 24 rounds of exact mechanism without converting. So the loop demonstrates the channel's honesty in both directions — it cannot coach and it cannot be sweet-talked — and it does not yet demonstrate feedback-driven conversion: no model tested sits one nudge from the bar. That open item is stated the same way on the loop report.
The oracle decides claims that reduce to finitely many exact arithmetic facts over a computable ring: exhibit-a-witness tasks, polynomial and tensor identities, rational collisions, interval enclosures with directed rounding, exhaustive censuses over finite box sets. Inside that domain both verdicts are theorems. Outside it — a proof sketch, an asymptotic, an existence claim without a witness — it has exactly one honest answer, and that answer is REFUSED.
The domain is narrow. It is also where the most cited AI-discovered mathematics of the last four years lives: AlphaTensor's and AlphaEvolve's decompositions, the Ramanujan Machine's continued fractions, the 2026 Jacobian and Hessian counterexamples — all finite exact objects, all decided here, from pinned bytes, with the verifiers detached.
The exit is formal. A certificate here is already a finite list of exact rational facts — the fastest thing a proof-assistant kernel checks. Demonstrated at full scale once: the Erdős #852 refutation rebuilt as a Lean 4 artifact, every prime in its witness kernel-checked and all three forged variants rejected by the kernel — the report states the bridge and its honest boundary. That path is not yet the default for every certificate; until it is, the oracle sits one rung below the formal standard and several above a float pipeline, and says so.
The live board — 268 model proposals graded across the campaigns, ladder and honesty probes included; every row in the append-only ledger certs/matmul-eval-ledger.jsonl.
The verifier in the loop — feedback template-locked to the mechanism; the build refuses a ledger whose feedback deviates. The failure taxonomy — the answer-key failure class this design removes, with a published specimen refuted at its twelfth digit. When the answer key is wrong — why reruns and digit cross-checks provably cannot catch it. None by reading code — the red-control discipline as engineering.
The Forecast Gym — the probabilistic sibling of this channel: where a claim cannot be decided, only scored, forecasts are sha-committed before their outcomes exist and paid by a proper score in exact rationals — contamination impossible by construction, admission prune-only. Same discipline, second domain.
The paper draft: verified-reward-oracle.md — not submitted, not peer-reviewed; the board is authoritative over its numbers.
What you trust when you trust a verdict here: V8 BigInt and IEEE-754 directed rounding in the engine; Python's fractions in the detached verifiers; a handful of named external theorems consumed and cross-checked, not machine-proved; and one operator on one machine.
That last item is the real limit, and the remedy is not more of the operator's own tests — it is someone else's. The registry of independent reruns lives on this page and is empty until it isn't: 0 recorded at this build, read from corpus/external-reruns.json. To be in it: clone the repo, run any detached verifier or oracle/battery.py, and send the printed sha256 with your name and date to carlos@carlostoledo.co — name, date and hash get recorded here and on the control page.