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

Ruzsa [Ru98b] constructed a maximal Sidon set of size $\ll (N\log N)^{1/3}$ .

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

1(fun N => ↑(Erdos156.minMaximalSidonSet N)) =O[Filter.atTop] fun N => (↑N * Real.log ↑N) ^ (1 / 3)

SolvedStatement only, no proof