All open problems
Source labels openChecked July 26, 2026

Green's Open ProblemsCombinatorics

Ben Green's Open Problem 50

Let AF2nA \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 nO(log(1/α))n - O(\log(1/\alpha))?

Mathematical statement

Let AF2nA \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 nO(log(1/α))n - O(\log(1/\alpha))?

More precisely: does there exist an absolute constant C>0C > 0 such that for all n1n \geq 1 and all nonempty AF2nA \subseteq \mathbb{F}_2^n with density α>0\alpha > 0, the sumset 10A10A contains a coset of some subspace of dimension at least nClog2(1/α)n - C \log_2(1/\alpha)?

The sumset 10A10A is defined as {a1+a2++a10:aiA}\{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.

Statement source: Green's Open Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

green_50

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem green_50 : answer(sorry)      C > (0 : ),  n : ,  A : Finset (𝔽₂ n),    A.Nonempty     let α :  := A.dens     (W : Submodule (ZMod 2) (𝔽₂ n)) (v : 𝔽₂ n),      v +ᵥ (W : Set (𝔽₂ n))  ↑(10 • A)       (n : ) - C * Real.logb 2 (1 / α)  Module.finrank (ZMod 2) W := by  sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References