Carlos Toledo · cert-machine

The conjecture engine

Verification layers under which AI-scale mathematical search produces only certified output — and certified audits of published AI-generated mathematics. Screens may prune; only exact arithmetic admits. A REFUTED here is proved.

closed forms refuted

54,635,201

every one exact; zero discoveries claimed

certified objects

16,943

of 819,152 generated across 11 families

period-16 Hénon points

EXACTLY 1,696

1,419,655,025 boxes exhausted, recheck clean

mu(5) bracket

≤ 1 + π/20

= 1.157080 — certified on a 1983→1992→2019→here lineage

Ramanujan Machine rows

52 decided

51 survive · 1 printed row refuted, correction certified

published claims refuted

Erdős #852 C* at digit 12 · one RM printed row — both with certified corrections

the three lanes

What almost nobody else publishes

Proved negatives at scale. 54,636,098 candidate closed forms tested against certified enclosures; 54,635,201 refuted, each refutation a proof. Twenty-one published OEIS constants fall in exact BigInt arithmetic at their full published precision — one impersonates 1/5 for 62 significant digits before the exact arithmetic separates them.

Completeness certificates for non-SAT numerics. Not "we found 1,696 period-16 points of the Hénon map" but "there are EXACTLY 1,696, and nothing else anywhere in the plane" — 452 census theorems across two maps, each an exhaustion from a certified a priori bound, plus a certified lower bound on topological entropy.

Certified audits of published AI-generated mathematics. The GPT-published constant on Erdős #852, refuted at its 12th significant digit and shown to BE the naive IEEE-754 float product, digit for digit — corrected value certified to width 3.2e-16. All 52 rows of the Ramanujan Machine's seven result sheets decided: 51 survive an unconditional audit; one printed row is refuted exactly (a sign slip in the published constant), its correction certified on the same enclosure.

the machine

How a conjecture becomes a certificate

the machine

Generate at scale, screen in float, certify the survivors exactly. Select any node for what it does — every count is read off ledger.json at build time.

The loop this repository runs. Families supply objects and mathematics; the engine supplies scale and bookkeeping; the instruments alone decide. REJECT and REFUSED are terminal by design — only a certificate reaches the ledger, the gates run on every build, and every page is rebuilt from the ledger alone.

The control page is this drawing, live: every family, every battery executed at its build (never remembered), the full ledger decomposition, drift status.

the reports

Research notes that re-prove themselves

the eval · live boardThe matmul eval: ground truth is a proofFrontier models are asked for exact rank-R matmul tensor decompositions; every proposal is certified or refuted in exact rational arithmetic. No judge, no rubric — a proof either exists or it does not.first board live · zero subtly-wrong survivors methods noteNone by reading codeEvery real bug this machine has found — ten, cataloged — was caught by a red control, a calibration, an impossible number, or a byte pin. The discipline stated as engineering, with living gates.every regression re-held by a battery at build audit · refutationThe constant that was a rounding errorA GPT-published constant on Erdős #852, refuted at its 12th significant digit and shown to BE the naive IEEE-754 float product, digit for digit — with the certified correction.refuted at digit 12 · correction certified audit · standing registryThe Ramanujan Machine, auditedEvery row of all seven published result sheets decided by rigorous enclosures and exact rational comparisons — the whole registry re-certified at every build.52 rows · 51 survive · 1 printed row refuted program · certified landscapeThe Mercer programChowla’s cosine dips and Newman’s 0/1 minima certified as one landscape: exhaustive box sweeps, exact champions, a Sturm equality — every claim re-proved at build.mu(5) ≤ 1 + π/20 · re-certified every build erdős #290 · theoremErdős #290: the 4k(k+1) theoremThe square-discriminant law proved and re-proved as exact integer identities during the build, the enclosure sweep deepened past the cited page, the exceptional degree closed.planted falsifiers must fire at build

All 13 reports → — every number on every page is recomputed from the certificates and records at build time, and a build that drifts refuses to ship.

rerun a proof

Check a result yourself, in ten seconds

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

sources

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.

the certificates

Proofs that travel 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	Nine fast matrix-multiplication algorithms as exact tensor identities over Q and F2 — including AlphaTensor’s rank-47, decided both ways.	verify_strassen.py
mercer-mu5.json	The mu(5) ladder, mu(5) ≤ 1 + π/m rung by rung to m = 20 — every exceptional tuple closed by one exact rational evaluation.	battery-gated
mu-table.json	The Newman min-modulus table: every set in the named boxes exhausted, champions certified, orbits classified, conservation per row.	battery-gated
mu-table-40.json	The wider-box extension of the mu table — billions of sets exhausted, the narrow-box crowding artifacts corrected.	battery-gated
lambda-table.json	The lambda table: the source lab’s rows reproduced exactly, plus rows nobody else holds, certified at the stated depth.	battery-gated
entropy-henon.json	The certified entropy lower bound for the classical Hénon map: h-sets, covering relations, and the exact spectral argument.	battery-gated
erdos290-tail-ext.json	The Erdős #290 sweep extension: degrees closed beyond the cited page, the constant’s enclosure tightened degree by degree.	battery-gated
matmul-eval-ledger.jsonl	The matmul eval’s append-only ledger — every campaign row, every verdict, every tag; the leaderboard is built from this file.	battery-gated

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.

the discipline

Why believe any of it

One load-bearing invariant: nothing floating-point can ever admit a claim. Screens only prune; every admission passes exact arithmetic (BigInt rationals, directed dyadic rounding, Sturm chains); an instrument that cannot decide REFUSES rather than guesses; every exhaustion carries a conservation identity that throws rather than return a record with a hole in it.

Every battery carries red controls — forged inputs that must FAIL — and every instrument is calibrated against a case with a known answer before it runs on anything new. Every real bug this project has found was caught by a control, a calibration, or an impossible number; none by reading code.

The trust base, honestly: V8 BigInt and IEEE-754 correct rounding; a handful of named external theorems consumed and cross-checked, not machine-proved; one machine, one operator. This meets the working standard of the computer-assisted-proof tradition — Tucker's Lorenz, Galias's Hénon censuses, whose published counts the census here reproduces independently — one rung below the formal-proof standard.