---

Claim. For every $A\subseteq\mathbb N$ with $|A\cap[1,x]|=o(\sqrt x)$, if the integers divisible by no member of $A$ form an infinite set $B=\{b_1<b_2<\cdots\}$, then

$$\frac1x\sum_{b_i<x}(b_{i+1}-b_i)^2$$

converges to a finite real limit as $x\to\infty$. This answers Problem 489 yes. The hypothesis that $B$ is infinite is the write-up's; it excludes only the case $1\in A$, where $B$ is empty.

Submission note. Posted to erdosproblems.com as a proof claim by Colin Snyder (account coffeewithcolin) on 15 July 2026, giving "GPT 5.6 (custom harness)" as the AI used:

We claim the answer is yes: for every $A$ with $|A\cap[1,x]|=o(\sqrt{x})$, the limit of $\frac{1}{x}\sum_{b_i<x}(b_{i+1}-b_i)^2$ exists and is finite. Proved in Lean 4 / Mathlib, standard axioms only, no sorry. Idea: finite versions of the sieve are periodic, so their gap statistics converge on their own; the only danger is squared mass escaping into ever-longer gaps. We make every long gap pay a charge: inside any long gap, positions $n\equiv 1\pmod{Y!}$ supply many candidates, each blocked by a distinct large element of $A$, and after removing shared prime factors a gap of length $G$ yields on the order of $G^2$ coprime witness pairs. A lattice-geometry bound caps the total charge each pair of elements of $A$ can receive over all gaps at once, and that total is a convergent double sum. So long gaps carry uniformly little squared mass and the periodic limits converge to the true limit. Notes: Verify: unzip, build with the included checker, then "#print axioms" on the final theorem gives exactly [propext, Classical.choice, Quot.sound]. The bundle includes a statement-fidelity audit (open intervals, exact gap squares, limit over real cutoffs).

Argument, as the claimant describes it. The sieve by the members of $A$ below a threshold is periodic, so for it the mean squared gap has a limit; what remains is to show that the gaps the full sieve lengthens beyond the truncated one contribute a vanishing amount to the sum of squares. The write-up assigns each such gap to pairs of members of $A$: a gap of length $G$ contains many integers excluded by distinct large members of $A$, and dividing out common factors produces about $G^2$ coprime pairs of such members. A count of lattice points limits how much any one pair receives across all gaps, the sum over pairs converges, and so the truncated limits approach the limit for $A$ itself.

Formalization. The write-up presents the result as proved in Lean 4 with Mathlib, with the final theorem depending on the axioms propext, Classical.choice and Quot.sound only and no sorry, and offers a bundle to unzip and build with an included checker. The theorem shown on the write-up's page, erdos489_statement, quantifies over A : Set ℕ, assumes the counting function of $A$ on $[1,x]$ is little-o of $\sqrt x$ along $x\in\mathbb N$ and that the sieved set is infinite, and concludes that gapSumSq A x / x tends to some real L along $x\in\mathbb N$; the claim's note says the bundle includes a statement-fidelity audit covering open intervals, exact gap squares and limits over real cutoffs. The page also says an independent referee confirmed a kernel-checked build under Lean 4.31.0 and verified the statement; that sentence is the claimant's site's own and names nobody. A copy of the development was added on 23 July 2026 to the starfleet/erdos-489 folder of the williamjblair/lean-proofs repository and is linked above at that repository's commit of 30 July 2026; its Erdos489.lean proves erdos489_statement with the same hypotheses (the counting function of $A$ little-o of $\sqrt x$ along the naturals, the sieved set infinite) and the limit along the naturals, and the folder's README describes its proofs as rebuilt on CI against the pinned Mathlib and read for faithfulness, that repository's own gate. The formal-conjectures file for the problem marks erdos_489 category research solved with answer(True) and points its formal_proof attribute at that copy, at the commit of 2026-09-17 the problem page pins and on main as of 2026-10-07; that is the collection's record of a claimed proof, not acceptance evidence. Nothing was built, kernel-checked or audited here, so nothing is counted as formalized.

Claimant. Colin Snyder, posting as coffeewithcolin; the proof-claims tab names the system used as GPT 5.6 (custom harness). The write-up is hosted on the Star Fleet Math site.

Standing. Claimed. The site labels the problem OPEN; the claim's thread had no comments, the problem's discussion thread (three comments of 20 April 2026 on Chojecki's note, the partial claim Chojecki's note) does not mention it, Erdős's refereed squarefree case is the accepted partial claim [[problems/integer_sequences/E0489/claims/1951_05_04_erdos|Erdős's squarefree case]], and there is no refereed version of this claim and no outside acceptance. The formal-conjectures collection marks the problem solved on the strength of the hosted copy of this proof, a maintainers' label and not a review of the claim.

Depends on. No page of this wiki.