Erdős Problem 39

Reference: erdosproblems.com/39

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

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$?