Erdős Problem 44: Extending Sidon Sets

Theorem 44 · Erdős

The maximum size of a Sidon set in {1, ..., N} is less than or equal to 2 * √N.

Formal statement · Lean 4.lean

theorem maxSidonSubsetCard_icc_bound (N : ℕ) (hN : 1 ≤ N) :
    maxSidonSubsetCard (Icc 1 N) ≤ 2 * Real.sqrt N := by
  sorry

Proof. sorry

Nobody has tried yet.