Carlos Toledo · independent certification
How it works
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.
the method
How a verdict is made
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 (33 of 35 in one line, 9 with a verifier in the standard library alone).
the register
Decided recently
| recorded | claim | claimant | verdict |
|---|
| 2026‑11‑08 | 26 circles in the unit square, sum of radii 2.63598308, as the source states it. README: "*… | ThetaEvolve, entry… | CERTIFIED |
| 2026‑11‑07 | 26 circles in the unit square, no overlaps, sum of radii = 2.63586276 (the AlphaEvolve… | ThetaEvolve, entry… | CERTIFIED |
| 2026‑11‑07 | Second autocorrelation inequality: the step function stored under key "8B-w_RL@65" (3072… | ThetaEvolve, entry… | REFUTED |
| 2026‑11‑07 | 26 circles in the unit square, no overlaps up to tolerance 1e-6 as stated in the source, sum… | ThetaEvolve, entry… | CERTIFIED |
| 2026‑11‑07 | EinsteinArena solution 2506 (agent "CodexProLong", created 2026-08-15) to the problem "The… | EinsteinArena solution 2506… | REFUTED |
three lines of work
The audits are the work; the theorems are the calibration
45 reportsAudits of machine-generated mathematicsReleases, registries, manuscripts and announced records from AI systems and autonomous platforms, re-decided from their published bytes by programs that share no code with the claimant.the optimization-constants registry · the Qiushi Engine’s kissing bounds · OpenAI’s math release under two kernels · the two claimed refutations of ETH
10 reportsEvaluation whose ground truth is a proofGraders measured against answers that are provably wrong, published answer keys re-decided step by step, and environments and benchmarks in which a certificate replaces the answer key.METR’s time horizon · GSM8K’s answer key · the graders measured · three environments on two frameworks
38 reportsCertified decisions: theorems, exact values, operationsResults proved here in exact or interval arithmetic — the calibration of the instruments and some values that were not known — and operational numbers decided over declared envelopes for energy, maritime, aviation and ocean statistics.δ₃ = 117/2192 · λ(4) and λ(5) · Erdős #290 and #1038 · Janela, HarborProof, SkyAudit
what stops this page
This page refuses to build if …
Every number and quotation above, on the home page and on Verify is read from a record when the pages are built, and the build checks that the record still says it. Below are the 23 conditions it refuses on, written out by the checks that test them; if any one becomes true, nothing is written and the last good pages stay up.
The 23 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.
- … one of the three outside voices quoted on the home 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.
- … 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.
- … /verify/ says a share of OpenAI's formalized families state less than their headline; the statements record no longer counts one.
- … /verify/ says no planted forgery was certified; the self-audit record counts a false certification.
- … /verify/ says most outside re-derivations used their own code; the reruns record says otherwise.
- … a priority claim ("the first …") reaches this page without "to our knowledge".
- … the site's default 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 the head of the one description and the description whole.
- … the home page's browser title is not the head of the one description in CLAUDE.md, or the page does not print the description once, word for word.
- … the home page's own share card is missing, is not the image its receipt names, or does not set the page's headline.