49.lean`

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

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

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

Green's Open Problem 49

Also known as the Marton's conjecture or the Polynomial Freiman-Ruzsa conjecture (PFR).

References:

[Gr24] Ben Green's 100 Open Problems
[Aa19] Aaronson, James. "A counterexample to a strong variant of the Polynomial Freiman-Ruzsa conjecture." arXiv preprint arXiv:1902.00353 (2019).
[Fa00] I. Farah, Approximate homomorphisms. II. Group homomorphisms, Combinatorica 20 (2000), no. 1, 47–60.
[GGM25] W. T. Gowers, B. J. Green, F. Manners and T. C. Tao, On a conjecture of Marton, Ann. of Math. (2) 201 (2025), no. 2, 515–549.
[Gr05] B. J. Green, Finite field models in additive combinatorics, Surveys in combinatorics 2005, 1–27, London Math. Soc. Lecture Note Ser., 327, Cambridge Univ. Press, Cambridge, 2005.
[GrTa10] B. J. Green and T. C. Tao An equivalence between inverse sumset theorems and inverse conjectures for the U3 norm, Math. Proc. Cambridge Philos. Soc. 149 (2010), no. 1, 1–19.
[Lo12] S. Lovett, Equivalence of polynomial conjectures in additive combinatorics, Combinatorica 32 (2012), no. 5, 607–618.
[LoRe17] S. Lovett and O. Regev, A counterexample to a strong variant of the Polynomial Freiman Ruzsa conjecture in Euclidean space, Discrete Anal.(2017), Paper No. 8, 6 pp.
[Ma19] F. R. W. M. Manners, Formulations of the PFR conjecture over Z, Math. Proc. Cambridge Philos. Soc. 166 (2019), no. 2, 243–245.
[Sa12] T. Sanders, On the Bogolyubov-Ruzsa lemma, Anal. PDE 5 (2012), no. 3, 627–655.
[Ta08] T. C. Tao, A counterexample to a strong polynomial Freiman-Ruzsa conjecture, blog post November 2008, available at http://tinyurl.com/36j6hyxv.

Imports (1)

FormalConjecturesUtil

theorem Green49.green_49 Suppose that $A \subset \mathbb{F}_2^n$ is a set with $|A + A| \leq K|A|$ sorry line 55 source
Source documentation
Suppose that $A \subset \mathbb{F}_2^n$ is a set with $|A + A| \leq K|A|$. Is it true that $A$ is covered by $K^{O(1)}$ translates of a subspace of size $\leq |A|$?
Solved by [GGM25], with at most $2K^{12}$ translates. The factor $2$ cannot be omitted: for $A = \mathbb{F}_2^n \setminus \{0\}$ one has $K = 2^n / (2^n - 1)$, so $K^C \to 1$ as $n \to \infty$, while every subspace of size at most $|A|$ is proper and two translates are needed.

depends on sorry what this means
Statement uses: Iff, True, Exists, Nat, And, GT.gt, OfNat.ofNat, Finset, 𝔽₂, Finset.Nonempty, Real, GE.ge, LE.le, Finset.card, HAdd.hAdd, Fin, ZMod, HMul.hMul, Submodule, Nat.card and 4 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
80 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem green_49 : answer(True) ↔
    ∃ C > 0,
      ∀ n (A : Finset (𝔽₂ n)), A.Nonempty →
      ∀ K ≥ (1 : ℝ), (#(A + A) : ℝ) ≤ K * #A →
        ∃ (W : Submodule (ZMod 2) (𝔽₂ n)) (T : Finset (𝔽₂ n)),
          Nat.card W ≤ #A ∧
          (#T : ℝ) ≤ 2 * K ^ C ∧
          (A : Set (𝔽₂ n)) ⊆ T + W := by
…
```
Mentions: 𝔽₂