cert-machine · report · generated from the records
Erdős #488: an AI-assisted refutation certified against DeepMind’s current statement
Erdős asked whether the share of numbers that are multiples of a finite set can ever more than double as you look further out. On 5 September 2026 Declan Gessel, working with OpenAI’s GPT-6 Astra, showed with a Lean proof that it can, and asked Google DeepMind’s list of open problems to mark the question settled. The request sat for two months, and the list changed its wording in the meantime. I checked it from every side, pre-registered and sealed before any code ran: it refutes the problem exactly as DeepMind states it today.
tl;dr
The finding. Gessel’s Lean refutation of Erdős #488 is correct against the statement as it stands in google-deepmind/formal-conjectures: Lean’s kernel accepts it three ways, an independent kernel (nanoda) accepts all 10,177 declarations, and nothing but the three standard axioms is used.
The mechanism. His proof restated the problem instead of importing it, and the problem’s file changed after his request. Here the statement is taken from DeepMind’s own declaration, so an edit cannot pass unnoticed; three planted wrong statements were each refused.
Check it.node tools/record-erdos488.js --check re-derives every verdict from the run’s facts; the two arithmetic deciders re-run in it.
his statement vs DeepMind’s
CERTIFIED
the same expression up to variable names; 3 wrong variants refused
kernels
2 accept
Lean (also from scratch, 36 min) and nanoda, 10,177 declarations
planted fakes caught
4 of 4
a false sum, a sorry, an axiom, an unchecked shortcut
a small counterexample
none found
4,253 setups to 10,000,000; best 1.38× with 10+ numbers
The discovery is Declan Gessel’s, made with GPT-6 Astra. This page certifies his proof; it is not a new result, and who found the counterexample first is a reading of dated sources.
first, the limits
What this does not decide
Whose result it is. The refutation is Gessel’s, with GPT-6 Astra in Codex (5 September 2026). Others went further the same week: an explicit instance, and a proof that the ratio has no bound at all (below).
Four checkers were not run. leanchecker-paranoid, con-leche, con-ron, lean4lean: Lean 4.33.1 does not bundle them, and only nanoda and an exporter were built here.
The smallest counterexample. Still unknown. My search found none among small cases; the known ones live at numbers with over a hundred digits.
Who was first. A reading of the sources as dated on 6 November 2026, not a decision.
also first
Where the run differs from the plan
The plan was sealed before the run; three things differ from it, and the record keeps all three.
A wrong pin in the plan. The pre-registration gives DeepMind's Mathlib as b7eb3304; that is the plausible package's pin. Mathlib is v4.33.1 at 0df444a3 (the entry's lake-manifest.json; fc-cache.log).
One Lean checker short. The pre-registered rule names three Lean checkers (leanchecker, leanchecker-paranoid, --fresh); leanchecker-paranoid is not in Lean 4.33.1, so P3 rests on leanchecker and --fresh, with nanoda as an independent kernel. The separate re-elaboration of each source with -Ddebug.skipKernelTC=false was not run; the audit records the kernel check on by default.
A planted fake that was not false. The pre-registered false variant (4095 for 4096) is in fact true, 2^4095·32769^53 < 3^4095, so it would not have been a fake; the run used 1000, which is false.
the question
Can the share of multiples more than double?
Take a finite set of whole numbers, none of them 0 or 1, and count how many numbers up to a limit are multiples of at least one of them. With the set {5}: up to 9, one number in nine is a multiple (about 11%); far out, one in five (20%). The share grew by a factor of about 1.8. Erdős asked whether, from a limit n at least as large as every number in the set to any larger m, the share can ever reach more than twice what it was at n. With a single number it gets close to 2 and never reaches it.
The set {5}. Each dot is the share of the numbers up to x that are multiples of 5, exact. At x = 9 the share is 1 in 9 (the diamond); the upper line is twice that, 2 in 9. The share climbs back to exactly 1 in 5 at every multiple of 5 and never reaches the upper line: here the share grows by a factor of 1.8, not 2. Erdős asked whether any finite set can push it past the line.Record: none — the share ⌊x/5⌋/x, computed exactly as the page is built.
In DeepMind’s list the question is the Lean declaration Erdos488.erdos_488 in FormalConjectures/ErdosProblems/488.lean, still marked open at commit 2055e5a.
the claim
A Lean proof that waited two months
Gessel’s construction takes every number between T and 256·T whose prime factors are all below 257. Up to 256·T their multiples are rare; much further out they fill more than twice the share. A counting argument shows that some T = 256k with k below 4,096 works, without saying which. His proof is a single Lean file, and it restates the problem’s text instead of importing DeepMind’s declaration.
His request to mark the problem solved (pull request #5297) drew one approving review and a maintainer’s question: how is the counterexample built, and who found it first? It was not answered, the request’s licence check failed, and on 14 October the problem’s file changed its form, so the request no longer applies as written.
who did what
Each step is a separate job
Find the result. Declan Gessel, with OpenAI’s GPT-6 Astra in Codex.
State the question formally. Google DeepMind, in its list of open problems in Lean (formal-conjectures).
Turn a claim in words into a formal statement. Not needed here: the question already existed in Lean, and the proof came in Lean. When a claim arrives in words, this is the job of claimbox, which was not used for this claim.
Write the proof. Gessel, in one Lean file.
Decide it, independently. cert-machine: the statement checked against DeepMind’s own declaration, the axiom audit, two arithmetic deciders, the search, the planted fakes.
Check the proof. Lean’s kernel (three ways) and nanoda, a kernel written apart from Lean.
Prove the dates. Verify Seal: salted fingerprints in a public registry and in Bitcoin, before each step ran.
the checks
Seven questions, written down and sealed before any code ran
question
what was done
verdict
P1 · the same question?
DeepMind’s statement taken from its declaration; his restatement compared as an expression; 3 planted wrong statements
CERTIFIED
P2 · works as delivered?
built unchanged in his environment (Lean 4.33.0) and in DeepMind’s (4.33.1)
CERTIFIED
P3 · do the kernels accept it?
our axiom audit; Lean’s checker; Lean’s checker from scratch (36 min); nanoda on an export of 39,709,680 bytes
CERTIFIED · nanoda ACCEPTS
P4 · is the arithmetic right?
five closed facts re-derived by two deciders in two languages, by two authors
CERTIFIED
P5 · a small counterexample?
4,253 setups, exact counts to 10,000,000
none found
P6 · who was first?
the dated sources, from Liu’s history
a reading
P7 · can the checks be fooled?
4 planted fakes of his proof
4/4 caught
P1 · the statement
Exactly DeepMind’s question, as it reads today
A Lean module of mine states ¬ (type_of% @Erdos488.erdos_488), the negation of DeepMind’s own declaration, and proves it with Gessel’s refutation. It builds, on the three standard axioms. His restated proposition and DeepMind’s statement are the same expression up to the names of bound variables. Three planted variants were each refused by Lean with a type mismatch: the wording before 14 October (answer(sorry) ↔ …), the constant 3 for 2, and m ≥ n for m > n.
One correction, on the record: the first planted variant first failed for the wrong reason, a missing import, not the statement. With the import it was refused for the right one.
P2 · P3 · the kernels
Two kernels, nothing but the standard axioms
The proof compiles unchanged in both environments. My audit of every declaration finds only Classical.choice, Quot.sound, propext across a closure of 9,898 constants, the two traversals agreeing. Lean’s checker accepts the module, and accepts it again from scratch, replaying every constant it rests on, the mathematics library included, into an empty environment (36 minutes). nanoda, a checker written apart from Lean, accepts all 10,177 declarations of the export.
P4 · the arithmetic
The numbers the proof leans on
Two deciders, one in JavaScript and one in Python, written by different authors who did not see each other’s code or the proof, re-derive the closed facts the proof evaluates: there are 53 odd primes below 257; Q, their product, and φ(Q); 128 < Q; 3·Q < 16·φ(Q); and 24096·3276953 < 34096. They agree to the last digit. The margin that makes the construction work is thin but real: φ(Q)/Q = 0.200706592524 against the 3/16 = 0.1875 it needs.
One correction, on the record: one of my planted false facts (3·Q < 15·φ(Q)) was in fact true; the second author had computed the right one, 14.
P5 · a small counterexample
None among the small cases
I searched the same kind of construction at small sizes, 4,253 setups with exact counts up to 10,000,000: no counterexample. The share comes close to doubling only for one to four numbers, where a short argument keeps it below 2; with ten or more numbers the best was 1.38×. This was the outcome predicted before the search, and it matches Liu’s computation at n = 6.7·1013, which reaches 1.447.
How close the share comes to doubling, by the size of the set. Light dots: the best ratio my search found among sets of about that size (exact counts up to 10 million; the ratios are double-precision values of those counts, while the 2× test itself was decided in exact integers). One number alone comes within a hair of 2 and provably stays below it; larger sets fall back to about 1.25× wherever the counts reach. The hollow diamond is Liu’s direct computation at 65 million numbers, 1.447, read from his paper. The known counterexamples are far off the right edge, among numbers with more than a hundred digits.Records: certs/erdos488.json · sha256 e575c7210e88; corpus/erdos488/p5/scan1.out · sha256 daba62427561The build refuses this figure if a point of the search reaches 2× (that would be a counterexample, and it is decided in exact integers), or a plotted point disagrees with the record.
P6 · who was first
The dated sources
D. Gessel (with GPT-6 Astra in Codex), 2026-09-05. the counterexample, Lean-verified; formal-conjectures PR #5297; Jig problem 398, statement 40 source.
woshuajolk (Jig), 2026-09-05. statement 39: the inequality holds whenever A ⊂ (n/5, n] source.
woshuajolk (Jig), undated in the sources read. statement 41: an explicit instance, A = the 257-smooth integers in (2^384, 2^392] source.
C. Benefield (Jig), 2026-09-06. statements 42, 43: the ratio exceeds 3, then is unbounded source.
shoal-rat, 2026-09-05. Lean-verified bounds and counterexamples for a sieved variant source.
Zongmin (Dylan Z.) Liu, 2026-10-17. the sharp order of the growth; the threshold λ* in [5, 54.18]; open problems source.
As far as these sources show, Gessel’s is the first counterexample. This reading is dated 2026-11-06, from Liu (Zenodo doi:10.5281/zenodo.23439872, 2026-10-17) and the sources it cites.
P7 · the red team
Four fakes, four caught
Red1 · the endpoint gap with 1000 for 4096 (false). The build fails: decide proves the planted inequality false.
Red2 · a sorry in constant_ratio. The audit lists sorryAx.
Red3 · an added axiom. The audit lists plumbRedAxiom.
Red4 · native_decide in endpoint_gap. The audit lists endpoint_gap._native.native_decide.ax_1_1.
the method
Rules first, sealed, then the run
Each step’s plan was written and committed before the step ran (notes/erdos488-preregistration-2026-11-06.md), and each stage was sealed: a salted fingerprint of the private work posted to a public registry and to Bitcoin through OpenTimestamps, proving the date without showing the content.
Seal 0.6269947088f4b720… · cert-machine seals/registry.jsonl @ 8173ba17 (2026-11-06); OpenTimestamps pending
Seal 1.e9058a8da01944ae… · cert-machine seals/registry.jsonl @ f431bcbb (2026-11-06); OpenTimestamps pending
Seal 2.0759afc2cb272297… · cert-machine seals/registry.jsonl @ 53259050 (2026-11-06); OpenTimestamps pending
The order of events. The plan and the rules were sealed at 22:21 and 22:23 UTC, before the Lean run began at 22:39; the results were sealed at 23:44, before nanoda’s answer a minute later, which came in after that seal and is said so. The page went live at 01:28 on Carlos’s word; the final drafts were sealed at 01:42; the note, the review and the thread followed. Seal times are this repository’s public commits; the run’s come from its own log; the publications’ from Zenodo, GitHub and X.Record: certs/erdos488.json · sha256 e575c7210e88The build refuses this figure if a run starts before the rules were sealed, or the events fall out of order.
The record.node tools/record-erdos488.js --check re-derives every verdict from corpus/erdos488/runs/pod-2026-11-06 and re-runs both arithmetic deciders.
The arithmetic alone.node tools/erdos488-p4.js --controls and python3 -I tools/erdos488-p4.py --controls, standard library only.
The Lean run.tools/erdos488-lean/runpod-488.sh with its statement, check and planted files beside it: a Linux machine with elan, about an hour for the from-scratch replay.
His proof.the gist at 034be67a, sha256 f2a7dcfde9689e00…. It is not copied here: its licence is not stated.