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 case where we start with an empty set (constructing large Sidon sets).
True ↔ ∀ ε > 0, ∀ᶠ (M : ℕ) in Filter.atTop, ∃ A ⊆ Finset.Icc 1 M, IsSidon ↑A ∧ (1 - ε) * √↑M ≤ ↑A.cardOpenStatement only, no proof