AI produces mathematical claims faster than anyone can read them, and the graders that check those claims mostly compare decimals. This machine decides claims — other people's and its own — in exact arithmetic, without ever running the claimant's code. It refuted a published constant at its twelfth digit, measured what an ordinary tolerance grader actually accepts (89.5% of submissions that are provably wrong), and settled two values of a sequence conjectured open since 2019. Every verdict is a re-runnable certificate: proved, disproved, or honestly refused — never a probability argument. It is one engine with two faces: the reports, where a claim gets a verdict a build can refuse to ship, and the instruments, where the same arithmetic runs in your tab and every mark says what decided it.
No probability arguments and no digit-matching. A claim is admitted only by exact arithmetic on whole numbers, and an instrument that cannot decide refuses instead of guessing. When a page here says REFUTED, that is a proof, and the falsifying witness is printed beside it.
Everything on this site is one system. The engine generates objects and screens them in float; the certifiers decide the survivors in exact arithmetic and refuse what they cannot decide; and the same certifiers face two ways. The reports are the gated face: every page re-derives its record at build and a number that moves stops the deploy. The instruments are the open face: the same arithmetic drawn, and pulled on, in your tab, with every mark saying what decided it. Neither is an illustration of the other.
Only a machine that can prove a theorem should be trusted to refuse one. The audits are what the instruments are for; the theorems below them are the evidence that the instruments are strong enough for their refusals to count.
The first of them ships as a package anyone can install: prime env install carlos-toledo/break-the-grader puts the environment behind the first card on your own machine, where its forgery battery runs before it will score anything. What it measured.
A certificate settles a number. It does not make anyone look at it. Charts and graders both assert things, and neither distinguishes what the data forces from what the renderer or the tolerance chose. The instruments are the same certifiers pointed the other way: sixteen pages that draw the set the data admit instead of the one answer a prior picked, and let you pull on it. The black-hole image as the set of skies the data allow; a calibration line as the set the standards admit (132× the reported ±, assuming only monotone); a two-population equilibrium's split as a face whose dimension is decided in exact rationals while you drag it.
Every mark on those pages says what it is standing on. Solid where an exact decision backs it, dashed where the arithmetic was not verified, dotted where something other than the data chose it, and no mark at all where the instrument declined — stroke rather than colour, so it survives greyscale. A mark's standing is the weakest standing on its path to the pixel, so an argmax over a non-unique optimum yields chosen, not decided.
All sixteen instruments → — the geometry a model will admit to from the outside, a grader you can rewire wrong, the SVP records re-decided, a transit without a law for the star, an attention row as a point.
No number on those pages has a certificate row this build checks, and none of them can refuse a deploy. Four of the sixteen run a battery in make test all the same; one draws a certificate straight from the shelf below; twelve decide their headline number in exact integer or rational arithmetic; three are floats and say so beside the number rather than at the bottom. Those counts are read off the instruments' own manifest at build, and a page listed there that is not built stops this one.
Erdős problem #852 has a constant attached to it. In 2026 a value for that constant appeared, produced with frontier-model help and quoted to 13 decimal places. This machine enclosed the same constant in exact arithmetic. The two agree for a while and then they do not.
published 0.0752403861777
certified 0.0752403861783092455893…
↑ wrong from here
The interesting part is which wrong digits. The obvious way to compute this constant is a loop: take a few million prime numbers, turn each into a factor slightly larger than one, and multiply them together in ordinary floating point. Past a certain size those factors are so close to one that rounding makes them exactly one, and they stop contributing anything at all. The running product goes still. Going still is what convergence looks like, so the loop appears to have settled, and it prints.
The published constant is what that loop prints, digit for digit. It was not approximately right with unlucky endings. It was the bug.
That is why one wrong constant is worth a whole page. Every ordinary defence fails against this. Rerunning it reproduces the same wrong digits, because two independent floating-point implementations agree with each other rather than with the truth. Spending more compute changes nothing, because the loop is already ignoring almost every factor you would be adding. Checking the digits against a reference value fails whenever the reference came out of the same kind of pipeline — which is how a bad number gets into an answer key and stays there.
What settles it is arithmetic that never rounds. The refutation here is a strict inequality between two whole numbers, with a denominator millions of digits long and no approximation anywhere in it. The corrected value is trapped between two exact fractions that agree for 15 decimal places, so the true constant cannot be anywhere near the published one.
The correction has been public in the problem’s own thread on erdosproblems.com since 27 August 2026. The full audit → — the refutation as integers, the certified correction, and a catalogue of the other ways a mathematical answer key goes wrong without anyone noticing.
All 58 reports → — the AI-verification shelf, the Erdős problems, the applied fronts in aerospace and energy, and the classical ground the instruments were proven on first. Every number on every page is recomputed from the certificates and records at build time, and a build that drifts refuses to ship.
Everything here rests on a single rule, and most of the engineering is the cost of keeping it.
The control page carries the full drawing, live: every family, every instrument, every battery executed at its build (never remembered), the full ledger decomposition, drift status. If you have a claim you want put through it, the claims desk takes one: certified, refuted, or honestly refused, published whichever way it falls — 18 decided so far, 0 of them sent by somebody else.
A real, hash-pinned day of New York helicopter traffic — 82 aircraft, 382 flights — replayed on a map. Every trail is coloured by a verdict rather than by telemetry: each flight is re-flown on paper by an electric aircraft, using that manufacturer’s own published numbers, under the FAA’s energy-reserve rule, and decided.
Beta’s ALIA can certifiably cover 100 of the 382 flights and needs exactly 10 aircraft to do it — the lower half proved by pigeonhole, the upper half by an actual schedule. Joby, Archer and Eve publish too little to certify a single fleet, and the app says NEEDS DATA rather than guessing, with the exact number that would flip it printed beside the verdict.
Open SkyAudit → — the replay, the certificate panel, the fleet frontier and the what-if sliders, live. Data © adsb.lol (ODbL). Also live: the São Paulo pack — the world’s busiest urban helicopter market, decided under Brazil’s own reserve rule.
The instrument that audits a published claim also grades a model’s output, and that is turning out to be the more useful job. A model proposes an exact object; the grader re-derives it from whole numbers and answers CERTIFIED or REFUTED. There is no judge model, no rubric, and no stored answer key — so there is nothing to leak into a training set and nothing to game. The gap between “graded correct” and “is correct” that a policy would learn to exploit does not exist, because the grade is the proof.
That is measured, not asserted. Every campaign opens with deliberate forgeries — including one wrong by a billionth, invisible to any floating-point check — and if a single forgery grades as correct the run aborts before it touches real work. Across every real-model campaign so far, 364 proposals, nothing false has ever been graded correct and no certified row has ever turned out to be wrong.
The honest limit: this works for claims that come down to finitely many exact arithmetic facts — exhibit a witness, verify an identity, bound a quantity. It does not work for mathematics at large, and nothing here pretends otherwise. Inside that boundary the same grader can sit unchanged inside a training loop, with the verifier strictly stronger than the thing it is grading.
And the grader itself is now measured, not assumed. Point a suite of provably-wrong submissions — minted from certified enclosures, so each one is outside a certificate by construction — at the four grader shapes, and an absolute-tolerance grader accepts 89.5% of them while a grader that compares against the certificate accepts none. We graded the graders →
The oracle, packaged → — one curl, no dependencies, running on your laptop in under a minute: the claim schema, the tool definition a model calls mid-generation, the paste box, the paper draft, the ledgers.
Every headline claim detaches into a certificate — a JSON file of exact numbers — plus a verifier in plain Python: standard library only, nothing to install, zero code shared with the engine. Each verifier re-derives the mathematics from the certificate alone, re-hashes the pinned sources, must refute a deliberately forged value before it will exit green, and prints the sha256 of the certificate it checked.
python3 verify/verify_erdos852.py certs/erdos852-certificate.json python3 verify/verify_keller.py certs/keller-certificate.json python3 verify/verify_strassen.py certs/strassen-certificate.json
Run from a clone of the repository (add --sources corpus/sources to re-hash the pinned source bytes too), or download the certificate and verifier right here — the proof travels without the machine.
| certificate | what it holds | re-verify |
|---|---|---|
| erdos852-certificate.json | Both Erdős #852 constants as exact data: the c0 window re-decidable at 130 digits, the C∗ refutation as strict integer inequalities with no tail bound. | verify_erdos852.py |
| keller-certificate.json | The Jacobian/Hessian counterexample corpus — every polynomial as explicit exact rational monomials; determinants and collisions re-derivable from the file alone. | verify_keller.py |
| strassen-certificate.json | 10 fast matrix-multiplication algorithms as exact tensor identities over Q and F2 — including AlphaTensor’s rank-47, decided both ways. | verify_strassen.py |
Those three carry a detached verifier: standard library only, nothing to install, zero code shared with the engine. The other 74 records are gated by a battery instead — re-derived at every build, with planted forgeries that must fire — and the whole shelf, with what each one holds, is on the machine page.
Code, corpus, and full provenance: github.com/carlostoledo1891/cert-machine — MIT, no dependencies. Instruments lifted from a private source lab are hash-pinned in PROVENANCE.json; patches are declared so they can never be mistaken for drift.
This is one machine and one operator. The trust base is stated rather than hidden: V8’s big-integer arithmetic and IEEE-754 correct rounding are assumed correct, and a handful of named external theorems are consumed and cross-checked rather than machine-proved. Nothing here is a formal proof in the sense of Lean or Coq, and no page claims to be.
What it does meet is the working standard of the computer-assisted-proof tradition — Tucker on the Lorenz attractor, Galias on the Hénon censuses, whose published counts this machine reproduces independently. That is one rung below a formal proof and several rungs above a decimal that looked convincing.
What independence means here, exactly. Independence from the CLAIMANT: when this machine decides someone else's claim, it does not run their code and their code is never in the trust path. It does not mean every checker is a clean-room rewrite of every producer. Two instruments reuse code across the producer/checker line, both times this lab's own and both deliberately: instruments/mfgcap IMPORTS the frozen verifier published with the congestion result rather than editing it — freezing those bytes is the point, and they are re-extracted from the sent page at every build — and instruments/lemniscate was crossed from this lab's own bench with its require paths repointed at the certifier that bench already used. Where a page claims clean-room independence — the λ(4) clause walk, the #1038 forcing re-check, the band verifier — it says so on that page, and it means it.