---

Submission note. Posted to erdosproblems.com as a proof claim by Declan Gessel (account declangessel) on 5 September 2026, giving "GPT-6 Astra (Codex)" as the AI used:

We give a counterexample to Erdős problem #488. For a fixed finite set, the fraction of whole numbers divisible by a member of the set can more than double as we count further, even when both endpoints are at least as large as every member. Our set consists of numbers greater than T and at most 256T whose prime factors are all below 257. A counting argument guarantees a choice of T where these numbers grow slowly, giving an upper bound on the covered count at the first endpoint. At a larger endpoint, we construct many distinct multiples of members of the set. This gives a lower bound there. Comparing the bounds proves that the fraction more than doubles. The proof has been formalized and checked in Lean. Notes: It was machine-checked through Jig: https://jig.so/p/398?s=40

The claim. Submitted to the proof-claim tab of Problem 488 on 2026-09-05 (23:44 UTC) by Declan Gessel as a full proof claim made with GPT-6 Astra (Codex), the system the tab names: the site's inequality fails, so the question is answered no. The set is the $257$-smooth integers in $(T,256T]$ for $T=256^k$ at a suitable scale $k$; the endpoints are $n=256T=\max A$ and $m=2TQ$, with $Q$ the product of the $53$ odd primes below $257$. The note bounds $\lvert B\cap[1,n]\rvert=\lvert A\rvert$ above by a counting argument that guarantees some $k<4096$ at which the smooth numbers grow slowly, bounds $\lvert B\cap[1,m]\rvert$ below by exhibiting many distinct multiples of members of $A$, and compares the two bounds; the inequality $3Q<16\varphi(Q)$ it uses holds, since $\varphi(Q)/Q=0.2007\ldots$. The Lean file Erdos488.lean at the linked revision (toolchain v4.33.0, Mathlib pinned in lakefile.toml) declares finite_counterexample, proof and Erdos488ExactAdapter.refutation : ¬ proposition, where proposition is the right-hand side of the formal-conjectures statement; its README reports the axiom closure propext, Classical.choice, Quot.sound, and that the scale is established by pigeonhole and not named. The claimant first posted the Lean proof through Jig, an external verification service, at 20:25 UTC the same day, as statement 40 of Jig problem 398 (both postings linked above). The Jig record reports that it passed the verifier's build, axiom (propext, Classical.choice, Quot.sound), manifest, refutation, no-new-axioms, static-policy and anti-restatement checks under Lean v4.33.0 with Jig's pinned Mathlib. The gist was revised six times the same evening: the Lean file is linked at the revision the claim names (22:27 UTC), and the proof note, absent from that revision, is linked at the revision of 23:27 UTC in which it first appears.

Standing. Claimed. On 2026-09-18 and again on 2026-10-07 the site's label (FALSIFIABLE) and its commentary of 8 April 2026 were unchanged, the thread carried no curator comment on the claim, the tab entry had no comments, and no referee or named expert has reviewed the note or the Lean file. The Jig verdict is an outside kernel check, not a review by a named mathematician, so it gives no evidence, as on Gessel's Problem 1040 page. The Lean file is neither built nor audited here, so it is not acceptance evidence. The claim is consistent with the partial positive claim of 27 August 2026: every element of $A$ in $(T,2T]$ is a minimal element under divisibility, so $A$ has far more than seven primitive elements, and with the partial claim on the shoal-rat page, since every even element of $A$ above $2T$ is a multiple of a smaller element, so the excess of $A$'s minimal subset at $n$ is far above $15$.

Depends on. Nothing in this wiki: the claim rests on its own note and Lean file.