Erdős problem 39

Is there an infinite Sidon set $A\subset \mathbb{N}$ such that $\lvert A\cap \{1\ldots,N\}\rvert \gg_\epsilon N^{1/2-\epsilon}$ for all $\varepsilon > 0$ ?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

39.lean

Retained formal statement1 of 1

Is there an infinite Sidon set $A\subset \mathbb{N}$ such that $\lvert A\cap \{1\ldots,N\}\rvert \gg_\epsilon N^{1/2-\epsilon}$ for all $\varepsilon > 0$ ?

FormalConjectures/ErdosProblems/39.leanErdos39.erdos_392 linesExact file

1True ↔2  ∃ A, A.Infinite ∧ IsSidon A ∧ ∀ ε > 0, (fun x => ↑x ^ (1 / 2 - ε)) =O[Filter.atTop] fun N => ↑(Set.Icc 1 N ∩ A).ncard

OpenStatement only, no proof