FormalConjectures/GreensOpenProblems/12.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

Green's Open Problem 12

References:

Imports (1)
  1. theorem Green12.green_12 Let $G$ be an abelian group of size $N$, and suppose that $A \subset G$ has density $\alpha$ sorry line 41 source

    Source documentation

    Let $G$ be an abelian group of size $N$, and suppose that $A \subset G$ has density $\alpha$. Are there at least $\alpha^{15} N^{10}$ tuples $(x_1, \dots, x_5, y_1, \dots, y_5) \in G^{10}$ such that $x_i + y_j \in A$ whenever $j \in \{i, i+1, i+2\}$?

    Note: We interpret indices modulo 5.

    depends on sorry what this means

    Statement uses: Iff, True, AddCommGroup, Fintype, DecidableEq, Finset, Nat, Fintype.card, Real, HDiv.hDiv, Finset.card, Prod, Fin, OfNat.ofNat, Finset.filter, Membership.mem, Insert.insert, HAdd.hAdd, Singleton.singleton, Prod.fst and 5 more

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

    64 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem green_12 : answer(sorry) ↔
    ∀ {G : Type*} [AddCommGroup G] [Fintype G] [DecidableEq G],
    ∀ (A : Finset G),
    let N := Fintype.card G
…