Erdős problem 489 · problems.science

If $A$ is a forbidden-divisor set with $|A \cap [1,x]| = o(\sqrt{x})$ and $B = \{b_1 < b_2 < \cdots\}$ the sifted set, must $x^{-1} \sum_{b_i < x} (b_{i+1} - b_i)^2$ converge to a finite limit?

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

489.lean

Retained formal statement1 of 2

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

FormalConjectures/ErdosProblems/489.leanErdos489.erdos_4894 linesExact file

1True ↔2  ∀ (A : Set ℕ),3    ((fun x => ↑{x ∈ Finset.Icc 1 x | x ∈ A}.card) =o[Filter.atTop] fun x => √↑x) →4      (Erdos489.sievedSet A).Infinite → ∃ L, Filter.Tendsto (fun x => Erdos489.GapSumSq A x / ↑x) Filter.atTop (nhds L)

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science