Conjectures.io

Combinatorics

Green50.green_50

Let A⊂F2nA \subset \mathbb{F}_2^n be a set of density α>0\alpha > 0. Does 10A10A contain a coset of some subspace of dimension at least n−O(log⁡(1/α))n - O(\log(1/\alpha))? More precisely: does there exist an absolute constant C>0C > 0 such that for all n≥1n \geq 1 and all nonempty A⊆F2nA \subseteq \mathbb{F}_2^n with density α>0\alpha > 0, the sumset 10A10A contains a coset of some subspace of dimension at least n−Clog⁡2(1/α)n - C \log_2(1/\alpha)? The sumset 10A10A is defined as {a1+a2+⋯+a10:ai∈A}\{a_1 + a_2 + \cdots + a_{10} : a_i \in A\}, using the pointwise scalar multiplication notation 10 • A where • denotes the iterated addition of a set. Note: We model F2n\mathbb{F}_2^n as Fin n → ZMod 2, which is an nn-dimensional vector space over F2\mathbb{F}_2.

References

  • Ben Green's Open Problem 50

No one has attempted this yet.

Formal statement

Lean type

True ↔
  ∃ C > 0,
    ∀ (n : ℕ) (A : Finset (𝔽₂ n)),
      A.Nonempty →
        have α := ↑A.dens;
        ∃ W v, v +ᵥ ↑W ⊆ ↑(10 • A) ∧ ↑n - C * Real.logb 2 (1 / α) ≤ ↑(Module.finrank (ZMod 2) ↥W)

What you must prove

import FormalConjectures.GreensOpenProblems.«50»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green50.green_50" := by
  sorry

end Bounty

Pinned source: FormalConjectures/GreensOpenProblems/50.lean

Source type SHA-256
sha256:c1fd81cdd113651e6fdf8a717643066c5698d45712dac90180e3bfb33c0c468b
Task id
fc-379fc029-green50-green-50-3a9dc0035d-formalized-v1
Task commitment
sha256:f82e4df26768822a4d64980c43612e955b0d1b6cb70ae61f56112f0f0314898a

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.