Erdős Problem 329: Maximum Density of Sidon Sets

Theorem 329 · Erdős

It is possible to construct a Sidon set with positive density.

Formal statement · Lean 4.lean

theorem exists_sidon_pos_density : ∃ (A : Set ℕ), IsSidon A ∧ 0 < sidonUpperDensity A := by
  sorry

Proof. sorry

Nobody has tried yet.