Erdős Problem 155

Reference: erdosproblems.com/155

@[reducible, inline]

noncomputable abbrev Erdos155.F (N : ℕ) : ℕ

Let $F(N)$ be the size of the largest Sidon subset of $\{1, \dots, N\}$.

Equations

• Erdos155.F N = (Finset.Icc 1 N).maxSidonSubsetCard

theorem Erdos155.erdos_155 : (∀ k ≥ 1, ∀ᶠ (N : ℕ) in Filter.atTop, F (N + k) ≤ F N + 1) ↔ sorry

Is it true that for every $k \geq 1$ we have $$ F(N + k) \leq F(N) + 1 $$ for all sufficiently large $N$?