Erdős problem 340
Let be the greedy Sidon sequence: we begin with and iteratively include the next smallest integer that preserves the Sidon property (i.e. there are no non-trivial solutions to ). What is the order of growth of ? Is it true that for all and large ?
Sources
FormalConjectures/ErdosProblems/
340.lean
Retained formal statement
It is trivial that this sequence grows at least like .
∀ ε > 0, (fun n => ↑n ^ (1 / 3)) =O[Filter.atTop] fun n => ↑(Set.range Finset.greedySidon ∩ Set.Icc 1 n).ncardTextbookStatement only, no proof