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.
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.
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.
The domain is deliberately inconvenient: a convex trapezoid with side slopes 6 and 18/5, no symmetry axis, nothing any existing proof technique can grab. The machine proves its second Neumann eigenvalue is simple by certifying a spectral gap — upper bounds from an interval Galerkin method, lower bounds from exact-rational finite elements with eigenvalue counts by interval inertia. It then builds a trial function that solves the eigenvalue equation EXACTLY — a sum of Bessel fans anchored at the four corners — and certifies that its boundary defect is a hundred-thousandth, which pins the true eigenfunction within an explicit distance of the trial.
Then the geography: every interior point is assigned, in exact rational arithmetic, to a deep core, a boundary collar, or a corner sector — and each region is killed by its own argument. Core and collar cells die by comparison against certified interior witnesses; the corner sectors die by certified series expansions, where the delicate corner needs a Bessel ladder identity to tame a divergent second derivative whose singular part arrives, provably, with the helpful sign. Zero cells survive. The extremes are on the boundary, the hottest point is vertex A and nowhere else, and the whole chain — eight records, every red control firing — re-runs from one command in about two minutes. The full account:
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 49 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.
Charts and graders both assert things, and neither distinguishes what the data forces from what the renderer or the tolerance chose. Everything above is the grader half. The instruments are the other one: nine of them, the same arithmetic, none of the gates.
They are not illustrations of the results above. The famous black-hole image is an argmax under a prior whose optimum is not unique — one sky chosen from the set the data still allow, and the set is drawn. A published calibration line is one curve out of the set 20 NIST standards admit: assuming only that the response is monotone, the honest interval is 132× the reported ±; joining the dots it is 1.0×, which says that precision was earned by the experiment and not by the model. And one plate is a picture of this repository’s own lower-bound certificate, shaded so the bright seams are where the argument nearly ran out.
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. One rule composes them: a mark’s standing is the weakest standing on its path to the pixel. The consequence that does the work is that an argmax over a non-unique optimum yields chosen, not decided, which is the shape of every regularised inverse problem ever published.
Nothing on those pages is gated: no number has a certificate row this build checks, none of them can refuse a deploy, and make test does not cover them. That is a fact about ceremony rather than about the mathematics — two of the nine draw a certificate straight from the shelf above, and five decide their headline number in exact integer or rational arithmetic — so each page states which of the two it is claiming, beside the number rather than at the bottom. The encoding itself is narrowed against real prior art and says so: uncertainty visualization, provenance visualization, verifiable visualization, and the lineup protocol, which one of those pages reinvented before it knew the name.
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 65 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.