Erdős problem 329
Erdős Problem 329. Let A ⊆ ℕ be a Sidon set. How large can lim sup_{N → ∞} |A ∩ {1,…,N}| / N^{1/2} be?
Sources
FormalConjectures/ErdosProblems/
329.lean
Retained formal statement
Krückeberg ([Kr61]) exhibited an infinite Sidon set A with sidonUpperDensity A = 1 / Real.sqrt 2, improving Erdős’ earlier 1 / 2 lower bound.
[Kr61] Krückeberg, Fritz, -Folgen und verwandte Zahlenfolgen. J. Reine Angew. Math. (1961), 53-60.
∃ A, IsSidon A ∧ Erdos329.sidonUpperDensity A = 1 / √2SolvedStatement only, no proof