Erdős problem 143

Does this imply that $\liminf \frac{|A \cap [1,x]|}{x} = 0?$

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

FormalConjectures/ErdosProblems/143.lean

Formal Conjectures

FormalConjectures/ErdosProblems/143.leanErdos143.erdos_143.parts.i2 linesExact file

1True ↔2  ∀ (A : Set ℝ), Erdos143.WellSeparatedSet A → Filter.liminf (fun x => ↑(A ∩ Set.Icc 1 x).ncard / x) Filter.atTop = 0

OpenStatement only, no proof