We check the math that machines publish

Erdős problem #852 has a constant attached to it. In 2026 a value for that constant appeared, produced with frontier-model help and quoted to 13 decimal places. This machine enclosed the same constant in exact arithmetic. The two agree for a while and then they do not.

published  0.0752403861777
certified  0.0752403861783092455893…
                        ↑ wrong from here

The interesting part is which wrong digits. The obvious way to compute this constant is a loop: take a few million prime numbers, turn each into a factor slightly larger than one, and multiply them together in ordinary floating point. Past a certain size those factors are so close to one that rounding makes them exactly one, and they stop contributing anything at all. The running product goes still. Going still is what convergence looks like, so the loop appears to have settled, and it prints.

The published constant is what that loop prints, digit for digit. It was not approximately right with unlucky endings. It was the bug.

That is why one wrong constant is worth a whole page. Every ordinary defence fails against this. Rerunning it reproduces the same wrong digits, because two independent floating-point implementations agree with each other rather than with the truth. Spending more compute changes nothing, because the loop is already ignoring almost every factor you would be adding. Checking the digits against a reference value fails whenever the reference came out of the same kind of pipeline — which is how a bad number gets into an answer key and stays there.

What settles it is arithmetic that never rounds. The refutation here is a strict inequality between two whole numbers, with a denominator millions of digits long and no approximation anywhere in it. The corrected value is trapped between two exact fractions that agree for 15 decimal places, so the true constant cannot be anywhere near the published one.

The correction has been public in the problem’s own thread on erdosproblems.com since 27 August 2026. The full audit → — the refutation as integers, the certified correction, and a catalogue of the other ways a mathematical answer key goes wrong without anyone noticing.

Everything here rests on a single rule, and most of the engineering is the cost of keeping it.

• A fast check may only rule things out. Floating-point screens run first and discard candidates by the million. They are never allowed to let one through. Nothing reaches a verdict without exact arithmetic behind it, so a rounding error can cost time and can never cost truth.
• Both verdicts are theorems. CERTIFIED means the statement was re-derived from whole numbers. REFUTED means a falsifying witness exists, and it is printed. Neither one is a confidence level.
• An instrument that cannot decide says so. REFUSED is a real verdict here and it gets used. A number that cannot be proved does not get published as though it were.
• Every battery carries forgeries that must fail. Fake inputs are planted in each run, including one wrong by a billionth — invisible to any floating-point check. If a forgery ever passes, the run aborts before it grades anything real. Every genuine bug this project has found was caught that way; none by reading code.

A real, hash-pinned day of New York helicopter traffic — 82 aircraft, 382 flights — replayed on a map. Every trail is coloured by a verdict rather than by telemetry: each flight is re-flown on paper by an electric aircraft, using that manufacturer’s own published numbers, under the FAA’s energy-reserve rule, and decided.

Beta’s ALIA can certifiably cover 100 of the 382 flights and needs exactly 10 aircraft to do it — the lower half proved by pigeonhole, the upper half by an actual schedule. Joby, Archer and Eve publish too little to certify a single fleet, and the app says NEEDS DATA rather than guessing, with the exact number that would flip it printed beside the verdict.

Open SkyAudit → — the replay, the certificate panel, the fleet frontier and the what-if sliders, live. 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.

The instrument that audits a published claim also grades a model’s output, and that is turning out to be the more useful job. A model proposes an exact object; the grader re-derives it from whole numbers and answers CERTIFIED or REFUTED. There is no judge model, no rubric, and no stored answer key — so there is nothing to leak into a training set and nothing to game. The gap between “graded correct” and “is correct” that a policy would learn to exploit does not exist, because the grade is the proof.

That is measured, not asserted. Every campaign opens with deliberate forgeries — including one wrong by a billionth, invisible to any floating-point check — and if a single forgery grades as correct the run aborts before it touches real work. Across every real-model campaign so far, 364 proposals, nothing false has ever been graded correct and no certified row has ever turned out to be wrong.

The honest limit: this works for claims that come down to finitely many exact arithmetic facts — exhibit a witness, verify an identity, bound a quantity. It does not work for mathematics at large, and nothing here pretends otherwise. Inside that boundary the same grader can sit unchanged inside a training loop, with the verifier strictly stronger than the thing it is grading.

The oracle, packaged → — one curl, no dependencies, running 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.

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

This is one machine and one operator. The trust base is stated rather than hidden: V8’s big-integer arithmetic and IEEE-754 correct rounding are assumed correct, and a handful of named external theorems are consumed and cross-checked rather than machine-proved. Nothing here is a formal proof in the sense of Lean or Coq, and no page claims to be.

What it does meet is the working standard of the computer-assisted-proof tradition — Tucker on the Lorenz attractor, Galias on the Hénon censuses, whose published counts this machine reproduces independently. That is one rung below a formal proof and several rungs above a decimal that looked convincing.