Source labels openChecked July 26, 2026

Green's Open Problem 12

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\}$ ?

Combinatorics AMS 5 AMS 11

Mathematical statement

Note: We interpret indices modulo 5.

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_12

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem green_12 : answer(sorry) ↔    ∀ {G : Type*} [AddCommGroup G] [Fintype G] [DecidableEq G],    ∀ (A : Finset G),    let N := Fintype.card G    let α := (A.card : ℝ) / N    let valid_tuples : Finset ((Fin 5 → G) × (Fin 5 → G)) := Finset.univ.filter (fun t =>      ∀ i : Fin 5, ∀ j ∈ ({i, i + 1, i + 2} : Finset (Fin 5)), t.1 i + t.2 j ∈ A)    (valid_tuples.card : ℝ) ≥ α ^ 15 * (N : ℝ) ^ 10 := 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, Ben. "100 open problems." (2024).background