green_2

Let $A \subset \mathbf{Z}$ be a set of $n$ integers. Is there a set $S \subset A$ of size $(\log n)^{100}$ such that the restricted sumset$S \hat{+} S$ is disjoint from $A$?

theorem green_2 : answer(sorry) ↔
    ∀ᶠ n : ℕ in atTop, ∀ A : Finset ℤ, A.card = n →
      (maxRestrictedSumAvoidingSubsetSize A : ℝ) ≥ (Real.log n) ^ 100

Recent Submissions

No submissions yet. Be the first to attempt this problem.