All open problems
Source labels openChecked July 26, 2026

Green's Open ProblemsCombinatorics

Ben Green's Open Problem 5

Which finite groups have the smallest biggest product-free sets?

Mathematical statement

Which finite groups have the smallest biggest product-free sets?

We formalise this as: determine the supremum of exponents α\alpha such that every nontrivial finite group of order nn contains a product-free set of size cnα\geq c n^{\alpha} for some absolute constant c>0c > 0. (The trivial group is excluded since its only product-free subset is empty.) Kedlaya [Ke97] showed that α=11/14\alpha = 11/14 is admissible, and Green suggests this exponent may well be sharp; the candidate extremal family is the Ree groups 2G2(q){}^2G_2(q), q=32m+1q = 3^{2m+1}.

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_5

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem green_5 :    IsLUB {α :  |  c > (0 : ),  (G : Type) [Group G] [Fintype G], Nontrivial G        S : Finset G, IsProductFree (S : Set G)         c * (Fintype.card G : ) ^ α  (S.card : )}      answer(sorry) := 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