Source labels openChecked July 26, 2026

Ben Green's Open Problem 18

Suppose that $G$ is a finite group, and let $A \subset G \times G$ be a subset of density $\alpha$ . Is it true that there are $\gg_\alpha |G|^3$ triples $x, y, g$ such that $(x, y), (gx, y), (x, gy)$ all lie in $A$ ?

Combinatorics AMS 5 AMS 11 AMS 20

Mathematical statement

Note: A is taken as $\alpha$ -dense, i.e. $|A| \ge \alpha |G|^2$ [Au16, Question 2]

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_18

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem green_18 : answer(sorry) ↔    ∀ α > 0, ∃ c > 0, ∃ m₀ : ℕ,      ∀ (G : Type*) [Group G] [Fintype G] [DecidableEq G] (A : Finset (G × G)),      Fintype.card G ≥ m₀ →      (A.card : ℝ) ≥ α * (Fintype.card G) ^ 2 →      (numNaiveCorners A : ℝ) ≥ c * (Fintype.card G) ^ 3 := 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 Ben Green's Open Problem 18background