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 ?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/340.lean∀ ε > 0, (fun n => √↑n / ↑n ^ ε) =O[Filter.atTop] fun n => ↑(Set.range Finset.greedySidon ∩ Set.Icc 1 n).ncardOpenStatement only, no proof