Independent exact certification of machine-generated mathematics
AI systems now announce records, constants and proofs faster than anyone reads them, and most checks compare decimals. Each claim here is re-decided from its published bytes in exact arithmetic, without running the claimant’s code, and comes back as one of three words: CERTIFIED, REFUTED with the object that breaks it, or REFUSED with the reason. Nothing asks for trust: every page is built from records that re-run, and refuses to build when a record stops supporting a sentence.
since August 2026, each with its verdict and the record that decided it · the register
asterisks removed from a registry
10
the optimization-constants registry (Davis, Ivanisvili, Tao), on our replays: 3 + 1 + 4 + 2 in four merged pull requests (#216, #230, #232, #243), cited as [T2026] · the first round · the later rounds
provably wrong answers a tolerance grader admits
89.55%
an absolute-tolerance grader: 3,582 of 4,000 answers minted wrong from certificates, in a mix picked here (dotted: chosen); a certificate grader admits none and rejects nothing right · the measurement
claims refused, whole or in part, by kind
9 · 2
of 131 decided: 9 PARTIAL (certified + refused) · 2 NEEDS DATA (refused, cause with the claimant) · none REFUSED outright; never summed · every claim, with its verdict
Every send and its status, with the status words meant exactly, is on the about page. Nothing here has been peer-reviewed; the pages ship their own falsifiers rather than asking for trust.
the visual grammar
Every mark says what it rests on
A line is solid only where an exact decision backs it, dashed where float arithmetic or a printed number stands unverified, dotted where something other than the data chose it, and absent where the instrument refused. A mark’s standing is the weakest one on its path to the pixel. Where a number rests on a model, it also names its premises and how far each was checked:
decided
exact arithmetic backs it
computed
float, or a number someone printed; nothing decided it
chosen
one member of a set the data admits
refused
no mark — the void is drawn
validated · compared · verified · assumed — a conclusion is as checked as its weakest premise (Swell and Janela show the chain; the same arithmetic runs in the browser on the instruments).
three lines of work
The audits are the work; the theorems are the calibration
A claim is read as a predicate over a declared box of inputs and decided in exact rational arithmetic or in outward-rounded interval arithmetic; the claimant’s program is never run in the trust path. A red control, a deliberately wrong input, must be rejected before its check counts, and the control build refuses on any red battery. The rerun kit gives the command that re-derives each record of the register (23 of 25 in one line, 7 with a verifier in the standard library alone).
Every number and quotation above is read from a record when the page is built, and the build checks that the record still says it. Below are the 21 conditions it refuses on, written out by the checks that test them; if any one becomes true, nothing is written and the last good page stays up.
The 21 conditions
… the kernel record of OpenAI's math release stops deciding every challenge under its two kernels (Lean's and nanoda), or holds one rejected.
… a Qiushi Engine kissing bound in certs/kissing-wave.json is not witnessed on every one of its pairs, with no violation.
… the certificate grader in certs/envs-record.json admits one provably wrong answer or rejects one right answer.
… the tolerance grader's rate is not an exact count over the provably wrong answers it was shown.
… a quotation from outside is not found word for word in its pinned snapshot, or the snapshot's SHA-256 has changed.
… an outside re-derivation in corpus/external-reruns.json is of a kind this page has no words for (its own code, or the tools that wrote the record).
… the three pinned snapshots of the optimization-constants registry stop counting the asterisks removed on our replays the same way.
… the rerun kit stops giving a one-line re-derivation for most of its records and a standard-library verifier for some.
… the method paper's PDF or its row in paper/INDEX.json is missing.
… the pinned credits stop holding a registry page that cites our replays as [T2026], or the row the registry corrected on our check.
… one of the four outside voices quoted on this page is no longer in the pinned credits (corpus/recognition.json).
… an outside re-derivation on record came back with a verdict other than ours.
… the asterisk removals in the registry's pinned credits, pull request by pull request, do not add up to the count in its snapshots.
… the register's count of decided claims is not its number of rows that are not queued, or a decided row names no record that decided it.
… a register row carries a verdict word the method page does not define.
… an outside card would send a reader anywhere but a report on this site or GitHub.
… the δ₃ ledger stops verifying the theorem δ₃ = 117/2192 with all of its certificates.
… the title registry (design/titles.json) and the report pages on disk disagree on how many reports there are, so a series count would be wrong.
… a priority claim ("the first …") reaches this page without "to our knowledge".
… its share card is missing, is not a 1200 × 630 PNG under 300 KB, is not the image its receipt names, or sets words other than this page's title and the one description.
… its title is not the head of the one description in CLAUDE.md, word for word.
Carlos Toledo, independent, Brazil. The mathematics, the design of every check and the decision about what may be claimed are the author’s; the writing and much of the implementation are done with AI assistance under the discipline above.