Erdős Problem #489

OPENdatabase updated 2025-08-31

No proof or disproof is known, and it isn't known whether a finite computation could settle it.

What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).

The set of positive integers not divisible by any element of `A`.

The squared-gap sum `∑_{b_i < x} (b_{i+1} - b_i)²`, where `b_i` enumerates the positive integers not divisible by any element of `A`.

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_{x \to \infty} \frac{1}{x}\sum_{b_i < x}(b_{i+1}-b_i)^2\] exists (and is finite)? For example, when \(A=\{p^2: p\textrm{ prime}\}\) then \(B\) is the set of squarefree numbers, and the existence of this limit was proved by Erdős. See also [208].

Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 1 further variant / known partial result in the Lean file. The authoritative wording is on erdosproblems.com/489.

Prizenone

Topicsnumber theory

Statement in LeanFormal Conjectures

Solution in Leanno

Original pageerdosproblems.com/489

Attempts

submit one →

FULL WRITE-UP BY THIS SITE · JUL 25, 2026

Read our full write-up →

Star Fleet Math (Colin Snyder, GPT-5.6 with a custom Lean harness) has quietly submitted full proof claims for four open Erdős problems on the tracker — ten days before we noticed. We almost shipped these as our own unflagged finds, on a triage brief whose search access was blocked from seeing the tracker's proof-claims pages. We caught it before posting anything: all four (#489, #394, #336, #1188) are already on record, zero comments, zero scrutiny. So instead of "we found this," here's the honest version — an independent from-scratch rebuild of two of the four, on our own compute, as a second opinion nobody had given yet.

CLOSED

← #488 the board #490 →