Carlos Toledo · independent certification
Independent exact certification of machine-generated mathematics
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.
kissing bounds of an autonomous discovery system
19 of 19
every pair decided exactly · 9.75 × 10¹⁵ pairs · the claimant published its points at the system’s request
a Lean certificate for Navier–Stokes blowup
certified
partial at the announced commit, certified at the next · every hypothesis read against the statement
tolerance graders against provably wrong answers
89.5%
admitted by an absolute-tolerance grader · a certificate grader admits none and rejects nothing right
The audits → · Contact →
three lines of work
What is decided here
35 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.leads: the optimization-constants registry, four asterisks removed on our replays · the Qiushi Engine’s kissing bounds, credited by the claimants · OpenAI’s math release under two kernels
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.leads: 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.leads: δ₃ = 117/2192 · λ(4) and λ(5) · Erdős #290 and #1038 · Janela (Portuguese), HarborProof, SkyAudit
the register
Decided recently
outside the building
What has come back
- Cited by a registry — 18 October 2026. The optimization-constants registry (D. Davis, P. Ivanisvili, T. Tao): Three asterisks removed on our replays — C₃b, C₃c and C₇₁ — merged by T. Tao (pull request #216); the constants' pages cite the replays as [T2026]. In their words: “with no code shared with the claimants, by C. Toledo” (the source, pinned).
- Cited by a registry — 18 October 2026. The optimization-constants registry (D. Davis, P. Ivanisvili, T. Tao): A fourth asterisk removed — C₃c's two-law certificate — on our replay, merged by T. Tao (pull request #230). In their words: “by C. Toledo, 17 Oct 2026; asterisk removed.” (the source, pinned).
- Credited by the claimant — 24 October 2026. The Qiushi Engine authors (Oxelra-AI): The claimants credit the complete verification of all nineteen kissing configurations in their English and Chinese READMEs, linking the report and the programs. In their words: “Carlos Toledo has independently verified the complete configurations in all 19 dimensions, confirming their point counts and exact dimensions.” (the source, pinned).
- Noted by an independent replayer — 23 October 2026. Maximusrufus, an independent replayer of AI-generated mathematics: Opening cert-machine issue 1, before re-running three of our records and finding no disagreement. In their words: “It covers much of the same ground, carefully, and I will cite it in our related-work notes.” (the source, pinned).
- Listed — 17 October 2026. Awesome-ai-proofs (a registry of AI-assisted mathematical results): Two of our audits recorded as audit events: the 4 × 4 matrix-multiplication decompositions (the row now marked verified) and the HorizonMath diagonal-Ramsey certificate (marked disputed). In their words: “Audit events from cert-machine (https://github.com/carlostoledo1891/cert-machine).” (the source, pinned).
- Independently re-derived, no shared code — 30 September 2026. rainrzk (GitHub): λ(4) for Erdős #510 (reports/lambda4.html): the cubic, the 14 generic collisions and the nine families re-derived from the write-up with independent code; every finite case re-certified in interval arithmetic. Outcome: the same verdict; three documentation findings in the write-up, folded in (commit 1c248ca) (the audit · the thread).
- Independently re-derived, no shared code — 23 October 2026. maximusrufus (GitHub): Twelve register rows re-decided with their own exact code, at cert-machine aa52e8d (Linux): the kissing configurations of AlphaEvolve (593) and EinsteinArena (594, 604); the sum–difference certificates of 3b (13 points) and 3c (147 and 95 points), agreeing to 30 digits. Outcome: the same verdict on all twelve rows, no disagreement; two findings, both answered on the thread (the audit · the thread).
- Independently re-derived, no shared code — 23 October 2026. maximusrufus (GitHub): The three ledgers re-derived with the tools that write them, at cert-machine aa52e8d (Linux, Python 3.14.4, Node v22.11.0); verify_sumdiff.py run beside the sum–difference ledger, its false-bound control firing.. Outcome: every verdict and count identical (the audit · the thread).
- Independently re-derived, no shared code — 24 October 2026. JeetuSK0808 (GitHub): The registry’s two C₃₁ rows (Lueker’s automaton at h = 9 and h = 10), our replay of reports/chvatal-sankoff.html re-derived with their own C program, written from Lueker’s published programs with no code of ours or the claimant’s: the state counts equal ours at h = 8, 9 and 10 (6,419,109; 51,425,006. Outcome: the same verdict on both rows; their bounds a little looser (vectors stopped once certified) (the audit · the thread).
- Independently re-derived, no shared code — 24 October 2026. JeetuSK0808 (GitHub): The registry’s C₈₄b correction (reports/optimization-constants.html §4) re-derived in their own interval arithmetic (mpmath), the note’s lemmas and inputs taken as given: c ≈ 0.000706 at the note’s choice; at most about 0.000707 over Y and X with R_K ≤ 103^d, and 0.00071385 with the regulator at its limit — so 0.000719 is not reached and 1.9993 is the entry.. Outcome: the same verdict; their 0.00071385 is the maximum, our 0.0007150508 a ceiling above it (answered on the thread, where we printed 0.0007150507: the ceiling truncated, rounded outward since 2026-10-24) (the audit · the thread).
- Independently re-derived, no shared code — 24 October 2026. maximusrufus (GitHub): The registry’s C₄₂ record (certs/turan-ledger.json) re-derived with the tool that writes it, at cert-machine 8924797: both rows identical. The rerun’s reading of instruments/turan/c42.py found three defects, none moving a verdict: failed checks answered REFUTED where the rule asks REFUSED, printed upper ends truncated rather than rounded outward, and the two routes compared on truncated strings.. Outcome: the same verdicts (PARTIAL); the three defects fixed, recorded in the self-audit’s amendment of 2026-10-24 (the audit · the thread).
- Independently re-derived, no shared code — 24 October 2026. maximusrufus (GitHub): Google’s AlphaEvolve Ramsey lower-bound graphs decided with their own clique search (two methods), before ours and with no code of ours: 15 of the 18 graphs, the verdicts compared with certs/ramsey-ledger.json.. Outcome: the same verdict on all 15; R(10,12) and R(7,13), which they could not finish, decided here; R(8,18) unfinished on both sides (the audit · the thread).
- Data published at the system’s request — from 11 October 2026. The Qiushi Engine (Oxelra-AI) released the point sets behind 17 of its 19 announced kissing bounds (dimensions 32–39, 43, 45, 49–55) after the audit asked for them; every bound was then witnessed, every pair decided (the kissing page · the release).
- Two announcements, one configuration. EinsteinArena provided the vectors of its 604-point dimension-11 configuration on request; it is the Station 604 up to a signed coordinate permutation, decided CONGRUENT (the kissing page).
- Answered on the mathematics — 31 August 2026. Erdős #290: Superseded on the mathematics five days later by arXiv:2609.00104, which proves the liminf exactly; our bracket is now the certified numeric value of that constant rather than one end of a range, and the page says so. Woett answered 2026-09-08 with the theorem; the follow-up with the 1/(1+c) bracket was posted 2026-10-06. (the thread).
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 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. 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.
carlos@carlostoledo.co · About → · GitHub · DOI