sumfree_set_density
Provedadditive-combinatoricscombinatoricsextremal-combinatoricsnumber-theoryready-to-formalizesum-free-sets
Sum-free sets: A set is sum-free if no element equals the sum of two others. Max size of sum-free subset of {1,...,n} is ⌈n/2⌉ - ⌈n/4⌉ (odd numbers in the upper half). Various quantitative conjectures on structure of large sum-free sets open.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem sumfree_set_density :
∀ eps : ℝ, 0 < eps →
∀ (n : ℕ) (A : Finset (Fin n)),
(∀ a b c : Fin n, a ∈ A → b ∈ A → c ∈ A →
a.val + b.val ≠ c.val) →
(A.card : ℝ) ≤ (n : ℝ) / 2 + eps := by
sorrySource