Source labels openChecked July 26, 2026

Green's Open Problem 52

Suppose that $A \subset \mathbb{F}_2^n$ is a set with an additive complement of size $K$ . Does $2A$ contain a coset of codimension $O_K(1)$ ?

Combinatorics AMS 5 AMS 11

Mathematical statement

Suppose that $A \subset \mathbb{F}_2^n$ is a set with an additive complement of size $K$ . Does $2A$ contain a coset of codimension $O_K(1)$ ?

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_52

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem green_52 :    answer(sorry) ↔ ∃ (c : ℕ → ℕ), ∀ (n K : ℕ) (A : Set (𝔽₂ n)) (S : Finset (𝔽₂ n)),      S.card = K → A + (S : Set (𝔽₂ n)) = Set.univ →      ∃ (V : AffineSubspace (ZMod 2) (𝔽₂ n)), (V : Set (𝔽₂ n)) ⊆ A + A ∧        n ≤ Module.finrank (ZMod 2) V.direction + c K := 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

Pinned Formal Conjectures sourceformalization Green's Open Problemsbackground