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

FormalConjectures/ErdosProblems/156.leanErdos156.greedySidonSet_isSidon1 lineExact file

1∀ (n : ℕ), IsSidon ↑(Finset.greedySidonBelow n)

TestStatement only, no proof