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
Erdős proved that upper density 1 / 2 can be attained; in particular, there exists a Sidon set whose upper density is *at least* 1 / 2.
∃ A, IsSidon A ∧ Erdos329.sidonUpperDensity A ≥ 1 / 2SolvedStatement only, no proof