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 maximum size of a Sidon set in {1, ..., N} is less than or equal to 2 * √N.
∀ (N : ℕ), 1 ≤ N → ↑(Finset.Icc 1 N).maxSidonSubsetCard ≤ 2 * √↑NTextbookStatement only, no proof