Green's Open ProblemsCombinatorics
Ben Green's Open Problem 50
Let be a set of density . Does contain a coset of some subspace of dimension at least ?
Mathematical statement
Let be a set of density . Does contain a coset of some subspace of dimension at least ?
More precisely: does there exist an absolute constant such that for all and all nonempty with density , the sumset contains a coset of some subspace of dimension at least ?
The sumset is defined as , using the pointwise
scalar multiplication notation 10 • A where • denotes the iterated addition of a set.
Note: We model as Fin n → ZMod 2, which is an -dimensional vector space
over .
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
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