Ben Green's Open Problem 1

Reference: [Ben Green's Open Problem 1](https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#section.1 Problem 1)

theorem Green1.green_1 : (∃ (Ω : ℕ → ℝ), Filter.Tendsto Ω Filter.atTop Filter.atTop ∧ ∀ (n : ℕ) (A : Finset ℕ), (∀ a ∈ A, 0 < a) → A.card = n → ∃ S ⊆ A, IsSumFree ↑S ∧ ↑n / 3 + Ω n ≤ ↑S.card) ↔ sorry

Let $A$ be a set of $n$ positive integers. Does $A$ contain a sum-free set of size at least $\frac n 3 + Ω(n)$, where $Ω(n) → ∞$ as $n → ∞$?