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
For any N, there exists a Sidon set of size at least √N/2.
∀ (N : ℕ), 1 ≤ N → ∃ A ⊆ Finset.Icc 1 N, IsSidon ↑A ∧ N.sqrt / 2 ≤ A.cardTextbookStatement only, no proof