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
It is possible to construct a Sidon set with positive density.
∃ A, IsSidon A ∧ 0 < Erdos329.sidonUpperDensity ATextbookStatement only, no proof