sidon_set_size_conjecture
Provedadditive-combinatoricscombinatoricsextremal-combinatoricsnumber-theoryready-to-formalizesidon-sets
Sidon set (B₂ set) size: Maximum size of a set S ⊆ {1,...,n} with all pairwise sums distinct is ≤ (1+o(1))√n. The Erdős-Turán conjecture says the max is √n + O(n^{1/4}). Best construction gives ~0.998√n. Exact constant unknown.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem sidon_set_size_conjecture :
∀ eps : ℝ, 0 < eps →
∃ C : ℝ, 0 < C ∧
∀ (n : ℕ) (S : Finset (Fin n)),
(∀ a b c d : Fin n, a ∈ S → b ∈ S → c ∈ S → d ∈ S →
a ≠ b → (a.val + b.val = c.val + d.val) → ({a,b} : Finset (Fin n)) = {c,d}) →
(S.card : ℝ) ≤ C * Real.sqrt n * (1 + eps) := by
sorrySource