Erdős problem 158 · problems.science

Let A be an infinite B₂[2] set. Must liminf |A ∩ {1, ..., N}| * N ^ (- 1 / 2) = 0?

Sources

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

4 retained statements2415f78e850a

FormalConjectures/ErdosProblems/

158.lean

Retained formal statement2 of 4

Let A be an infinite B₂[2] set. Must liminf |A ∩ {1, ..., N}| * N ^ (- 1 / 2) = 0?

FormalConjectures/ErdosProblems/158.leanErdos158.erdos_1583 linesExact file

1True ↔2  ∀ (A : Set ℕ),3    A.Infinite → Erdos158.B2 2 A → Filter.liminf (fun N => ↑(A ∩ Set.Iio N).ncard * ↑N ^ (-1 / 2)) Filter.atTop = 0

OpenStatement only, no proof