Erdős problem 156

Does there exist a maximal Sidon set $A\subset \{1,\ldots,N\}$ of size $O(N^{1/3})$ ?

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

156.lean

Retained formal statement2 of 4

It is easy to prove that the greedy construction of a maximal Sidon set in $\{1,\ldots,N\}$ has size $\gg N^{1/3}$ .

FormalConjectures/ErdosProblems/156.leanErdos156.erdos_156.variants.greedy_lower_bound1 lineExact file

1(fun N => ↑N ^ (1 / 3)) =O[Filter.atTop] fun N => ↑(Finset.greedySidonBelow N).card

SolvedStatement only, no proof