An independent certification of the refutation of Erdős Problem #488

Erdős Problem #488 asks whether, for a finite set A of integers at least 2 and every m > n ≥ max A, the density of the multiples of A up to m is less than twice their density up to n. On 5 September 2026 Declan Gessel, working with OpenAI's GPT-6 Astra in Codex, gave a Lean-verified counterexample (google-deepmind/formal-conjectures pull request #5297). This note certifies that proof independently: the discovery is Gessel's. Pre-registered and sealed before any code ran, the certification finds that the proof refutes the entry as it stands in google-deepmind/formal-conjectures (taken from the entry's own declaration by type_of%, with three planted wrong statements refused); that it compiles unchanged on Lean v4.33.0 and v4.33.1; that Lean's checker accepts it, also from scratch, and that an independent kernel (nanoda) accepts all 10,177 declarations of its export, on the three standard axioms only; that two independent deciders re-derive its closed arithmetic; and that four planted fakes are caught. Not run: leanchecker-paranoid, con-leche, con-ron, lean4lean. A search for a small explicit counterexample found none. Provenance is given as a dated reading of the sources. Prepared with Claude agents (Anthropic).