Erdős problem 156 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

4 retained statements2415f78e850a

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