The conjecture engine

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 51 printed rows of the Ramanujan Machine's seven result sheets decided: 50 survive an unconditional audit; one printed row is refuted exactly, its correction certified on the same enclosure. AlphaEvolve's rank-48 ⟨4,4,4⟩ decomposition: CERTIFIED over Z[i]. AlphaTensor's rank-47: verified over F2 and REFUTED over Q — the speedup provably requires characteristic 2.

Evaluation whose ground truth is a proof. Frontier models propose exact tensor decompositions; the grader re-derives every claim from the witness in exact rational arithmetic — no judge, no rubric, and no answer key to contaminate. A reference value computed in float puts its failure class inside the answer key; here the reference is not a value at all. 268 model proposals graded so far, every certified row a theorem, every refuted row a proof of error.

A verified reward channel. The same harness is a reward oracle for mathematical search under which reward hacking is excluded by construction, not by monitoring — false positives are provably impossible, and an instrument that cannot decide refuses rather than pays. Stated as engineering below.

And the proving ground the verifiers earned their trust on: 54,629,173 candidate closed forms tested against certified enclosures, 54,628,296 refuted — each refutation a proof, zero discoveries claimed. Completeness censuses ("there are EXACTLY 1,696 period-16 Hénon points, and nothing else anywhere in the plane"), certified extremal tables, a certified entropy bound. The instruments were calibrated on hard classical ground — reproducing Galias's censuses, Goddard's boxes, Apéry's row — before they were pointed at anything a model produced.

The engine's one load-bearing invariant — a float screen may only PRUNE, never admit; every admission passes exact arithmetic; REFUSED earns nothing — is precisely the property a verified-reward signal needs: there is no gap between "graded correct" and "is correct" for a policy to exploit. A proposal either IS an exact certificate or it is not, and both directions of the verdict are theorems.

That property is measured, not asserted. Every campaign begins with red controls — deliberate forgeries, including one whose coefficient is off by 1e-9, invisible to any float screen — and a single control certifying ABORTS the run: the oracle proves its refusal path fires before it grades anything. Across every real-model campaign to date (268 proposals), no false proposal has ever certified and no certified row has ever been wrong — the channel has never paid out on a false claim.

The scope is stated as honestly as the property: this holds for claims that reduce to finitely many exact arithmetic facts — exhibit-a-witness tasks, identities, enclosures — not for mathematics at large. Inside that domain, the harness that evaluates a model can sit unchanged inside a training loop: reinforcement learning on certified rewards, with the verifier strictly stronger than the proposer. That is the verification half of scalable oversight, running, on the one domain where it is currently possible.

The oracle, packaged → — one curl, zero dependencies, certify() on your laptop in under a minute: the claim schema, the tool definition a model calls mid-generation, the paste box, the paper draft, the ledgers.

The audit as an experience: a Flightradar24-style replay of a real, hash-pinned day of New York helicopter traffic (82 aircraft, 382 flights) — except every trail is colored by a VERDICT, not telemetry. Each flight is re-flown on paper by an eVTOL under a published energy-reserve rule, and decided by interval arithmetic: mathematically certified enclosures with exact-rational falsifying corners, never Monte Carlo.

The day's findings: Beta ALIA certifiably covers 100 of the 382 flights under the FAA 20-minute rule and needs EXACTLY 10 aircraft to re-fly them (proved by pigeonhole below, by a verified schedule above); Joby, Archer and Eve publish too little to certify a single fleet. The optimizer prices the levers — battery floors, charge times, the reserve rule itself — with a proof on both sides of every threshold.

Open SkyAudit → — the replay, the certificate panel, the fleet frontier and the what-if sliders, live. Every number gate-checked at build; data © adsb.lol (ODbL). Also live: the São Paulo pack — the world's busiest urban helicopter market, decided under Brazil's own reserve rule (ANAC RBAC 91.151(b), pinned).

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

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.