AI systems now propose mathematical claims faster than anyone reads them, and most checks compare decimals. Each claim here is decided in exact arithmetic, without running the claimant’s code, and the outcome is published as a re-runnable certificate: proved, refuted with a witness, or refused with the reason. The theorems on this site are the calibration; the audits are the work.
| recorded | claim | claimant | verdict |
|---|---|---|---|
| 2026‑10‑05 | The 2026 Navier–Stokes blowup claim: the Lean proof read against its statement | OpenAI | CERTIFIED |
| 2026‑10‑05 | the object is a feasible solution of "Erdős Minimum Overlap (Upper Bound)" | CodexProLong | REPAIRED |
| 2026‑10‑05 | the polynomial map with the sparse rational coefficients given has the Jacobian property claimed | The Station agents | CERTIFIED |
| 2026‑10‑04 | the notebook's "Rank-32 decomposition of <2,4,5> over 0.5*Z" is a decomposition of that… | AlphaEvolve | CERTIFIED |
| 2026‑10‑04 | the factors stored under key 2,2,3 of alphatensor_f2.npz are a decomposition of the ⟨2,2,3⟩… | AlphaTensor | CERTIFIED |
131 published claims decided since August 2026, each with its verdict and the record that decided it. The monthly registers: September, October. What was refused, by kind.
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.
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. The verdict is one of three words — CERTIFIED, REFUTED with the falsifying object, REFUSED with the reason — and NEEDS DATA where the claimant published no bytes. Every battery carries red controls, deliberately wrong inputs that must be rejected before a page is published, and every record is pinned by path and SHA-256. The method paper describes the arithmetic, the certifiers and the discipline; the rerun kit re-derives any decided claim with the standard library.
Carlos Toledo, working alone, from 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. Open to collaboration — an independent audit of a release or a registry, a benchmark review, a certified decision product — and to roles in evaluation and verification. A conventional CV on request.