Corroborate

Claim in Erdős problems that formal-conjectures marks solved

A published paper or arXiv preprint answers the main question of Erdős Problem #489 (theorem erdos_489 in formal-conjectures) in full (proof, disproof, or the exact value asked for) with no hypotheses beyond the problem's own.

Problem as stated at github.com/google-deepmind/formal-conjectures/blob/34ee0e3c5fd52d202d62a71094a37970cb5fb870/FormalConjectures/ErdosProblems/489.lean. The claim text is written by Corroborate; that site has not reviewed or endorsed it.

The problem, as stated in formal-conjectures (Apache 2.0):

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].

Verdict: no verdict yet

formal-conjectures marks problem #489 as solved. Those pages say who settled it and how.

Evidence for

None yet.

Evidence against

None yet.