Erdős Problem 156

Exercise 156 · Erdős

The formal statement below is all there is.

Formal statement · Lean 4.lean

theorem greedySidonSet_isSidon (n : ℕ) : IsSidon (Finset.greedySidonBelow n : Set ℕ) := by
  sorry

Proof. sorry

Nobody has tried yet.