Erdős problem 158

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

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

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