The machine proves it — or breaks it

The domain is deliberately inconvenient: a convex trapezoid with side slopes 6 and 18/5, no symmetry axis, nothing any existing proof technique can grab. The machine proves its second Neumann eigenvalue is simple by certifying a spectral gap — upper bounds from an interval Galerkin method, lower bounds from exact-rational finite elements with eigenvalue counts by interval inertia. It then builds a trial function that solves the eigenvalue equation EXACTLY — a sum of Bessel fans anchored at the four corners — and certifies that its boundary defect is a hundred-thousandth, which pins the true eigenfunction within an explicit distance of the trial.

Then the geography: every interior point is assigned, in exact rational arithmetic, to a deep core, a boundary collar, or a corner sector — and each region is killed by its own argument. Core and collar cells die by comparison against certified interior witnesses; the corner sectors die by certified series expansions, where the delicate corner needs a Bessel ladder identity to tame a divergent second derivative whose singular part arrives, provably, with the helpful sign. Zero cells survive. The extremes are on the boundary, the hottest point is vertex A and nowhere else, and the whole chain — eight records, every red control firing — re-runs from one command in about two minutes. The full account:

the report · the archived release.

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: on the eval board it is 13% of 301 submitted claims, and every other refusal in the lab is counted by kind — with its own denominator, never merged into one number — on the refusals page. 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.

And the grader itself is now measured, not assumed. Point a suite of provably-wrong submissions — minted from certified enclosures, so each one is outside a certificate by construction — at the four grader shapes, and an absolute-tolerance grader accepts 89.5% of them while a grader that compares against the certificate accepts none. We graded the graders →

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.

What independence means here, exactly. Independence from the CLAIMANT: when this machine decides someone else's claim, it does not run their code and their code is never in the trust path. It does not mean every checker is a clean-room rewrite of every producer. Two instruments reuse code across the producer/checker line, both times this lab's own and both deliberately: instruments/mfgcap IMPORTS the frozen verifier published with the congestion result rather than editing it — freezing those bytes is the point, and they are re-extracted from the sent page at every build — and instruments/lemniscate was crossed from this lab's own bench with its require paths repointed at the certifier that bench already used. Where a page claims clean-room independence — the λ(4) clause walk, the #1038 forcing re-check, the band verifier — it says so on that page, and it means it.