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
Finset.greedySidon 5 = 21TestStatement only, no proof