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
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 ?
∀ ε > 0, (fun n => √↑n / ↑n ^ ε) =O[Filter.atTop] fun n => ↑(Set.range Finset.greedySidon ∩ Set.Icc 1 n).ncardOpenStatement only, no proof