FormalConjectures/GreensOpenProblems/50.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

1 declarations, 1 contain sorry, 0 declared as axioms

Ben Green's Open Problem 50

Suppose that $A \subset \mathbb{F}_2^n$ is a set of density $\alpha$. Does $10A$ contain a coset of some subspace of dimension at least $n - O(\log(1/\alpha))$?

Here $kA$ denotes the $k$-fold iterated sumset, i.e., the set of all sums of $k$ elements from $A$ (with repetition allowed). In Mathlib, this is denoted k • A using pointwise scalar multiplication on sets.

Reference: [Ben Green's Open Problem 50](https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#section.6 Problem 50)

Imports (1)
  1. theorem Green50.green_50 Let $A \subset \mathbb{F}_2^n$ be a set of density $\alpha > 0$ sorry line 54 source

    Source documentation

    Let $A \subset \mathbb{F}_2^n$ be a set of density $\alpha > 0$. Does $10A$ contain a coset of some subspace of dimension at least $n - O(\log(1/\alpha))$?

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

    The sumset $10A$ is defined as $\{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 $\mathbb{F}_2^n$ as Fin n → ZMod 2, which is an $n$-dimensional vector space over $\mathbb{F}_2$.

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Real, And, GT.gt, OfNat.ofNat, Nat, Finset, 𝔽₂, Finset.Nonempty, Finset.dens, Fin, ZMod, Submodule, LE.le, Set, HVAdd.hVAdd, HSMul.hSMul, HSub.hSub and 6 more

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    126 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem green_50 : answer(sorry) ↔
    ∃ C > (0 : ℝ), ∀ n : ℕ, ∀ A : Finset (𝔽₂ n),
    A.Nonempty →
    let α : ℝ := A.dens
…

    Mentions: 𝔽₂