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 statement1 of 4

A set is B₂[1] iff it is Sidon.

FormalConjectures/ErdosProblems/158.leanErdos158.b2_one1 lineExact file

1∀ {A : Set ℕ}, Erdos158.B2 1 A ↔ IsSidon A

APIStatement only, no proof