Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated Oct 8

Problem 489

claims/: The 3 claim pages of Problem 489, one per claimant's result; the problem's standing derives from them.

Statement. Let $A\subseteq \mathbb{N}$ be a set such that $\lvert A\cap [1,x]\rvert=o(x^{1/2})$. Let

B=\{ n\geq 1 : a\nmid n\textrm{ for all }a\in A\}.

If $B=\{b_1<b_2<\cdots\}$ then is it true that

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

exists (and is finite)?

Status. OPEN, in the site's label. The site notes that for $A$ the set of prime squares, when $B$ is the squarefree numbers, Erdős proved the limit exists (Publ. Math. Debrecen 2 (1951), 103--109; claim page Erdős's squarefree case, accepted and partial). A full proof claim posted to the site's proof-claims tab on 15 July 2026 by Colin Snyder, produced with GPT 5.6 (custom harness), as the tab names the system, answers yes with a Lean 4 proof bundle; the site has not accepted it, nothing was built or audited here, and the claim page Snyder's Lean proof records it, together with the formal-conjectures collection's marking of the problem as solved on the strength of a hosted copy of that proof, which is not acceptance. A note of 20 April 2026 by Przemyslaw Chojecki, produced with GPT-5.4 Pro, as Chojecki's thread comment says, claims a proof that the limit always exists in $[0,+\infty]$ and is finite for a structured class of $A$ ; it is the partial claim page Chojecki's note. The frontmatter standing derives from the pending full claim, and it departs from the label for that reason: Snyder's claim answers the Statement yes and would settle it, so the derived standing is claimed with claim proved, while the site, which has not accepted the claim, labels the problem OPEN.

Source. erdosproblems.com/489, accessed 2026-09-04; proof-claims tab accessed 2026-10-06. Cite as: T. F. Bloom, Erdős Problem #489, https://www.erdosproblems.com/489.

Formalization. The file ErdosProblems/489.lean of formal-conjectures, pinned to its commit of 2026-09-17 (on main as of 2026-10-07 the file differs only by a module header), defines sievedSet A as the positive integers divisible by no member of A and GapSumSq A x as the sum of the squared gaps between consecutive members below x, and declares erdos_489 : answer(True) ↔ ∀ A, (counting function of A on [1,x]) =o[atTop] √x → (sievedSet A).Infinite → ∃ L : ℝ, Tendsto (GapSumSq A x / x) atTop (𝓝 L), with x running over the naturals, under category research solved with proof sorry and a formal_proof attribute pointing at the copy of Snyder's Lean proof in the williamjblair/lean-proofs repository, linked on the claim page; a second declaration states the squarefree case. The site's indicator records a formalized statement. The solved marking records that claim and is not acceptance evidence; nothing was built or audited here.

Progress

Not yet compiled.

Known Results

Not yet compiled.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

Linked from (9)

Erdős's second moment of squarefree gaps Chojecki's extended-limit theorem and finiteness criterion Lean proof that the mean squared gap converges problems/integer_sequences/E0489/claims Sequences and Densities of Integers integer_sequences/erdos_1951_problems_results_elementary_number_theory (23) for α = 2 (pp. 107, 109): the second moment of squarefree gaps is asymptotic to x Σ t² β_t Lemma 2 (p. 107): squarefree gaps longer than t number at most c x / (t² (log t)²)Closing remarks (p. 109): gap densities for general sifted sequences, a first-moment tail bound, and an example

Graph