Erdős Problem 42: Maximal Sidon Sets and Disjoint Difference Sets

Theorem 42 · Erdős

The set {1, 2, 4} is a maximal Sidon set in {1, ..., 4}.

Formal statement · Lean 4.lean

theorem example_maximal_sidon : IsMaximalSidonSetIn {1, 2, 4} 4 := by
  sorry

Proof. sorry

Nobody has tried yet.