Erdős problem 44
Erdős Problem 44: Let N ≥ 1 and A ⊆ {1,…,N} be a Sidon set. Is it true that, for any ε > 0, there exist M = M(ε) and B ⊆ {N+1,…,M} such that A ∪ B ⊆ {1,…,M} is a Sidon set of size at least (1−ε)M^{1/2}?
Sources
FormalConjectures/ErdosProblems/
44.lean
Retained formal statement
The greedy construction gives a Sidon set of size approximately √N.
∀ (N : ℕ), 1 ≤ N → ∃ A ⊆ Finset.Icc 1 N, IsSidon ↑A ∧ A.card ≥ N.sqrtTextbookStatement only, no proof