Green's Open ProblemsCombinatorics
Ben Green's Open Problem 14
It remains an interesting open problem to actually write down a colouring showing (say) for some . [Gr24]
Mathematical statement
It remains an interesting open problem to actually write down a colouring showing (say) for some . [Gr24]
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_14_variant_2r2
theorem green_14_variant_2r2 : -- Provide a pair (r, associated coloring) that avoids the monochromatic APs -- To show $W(3, r) > 2r^2 - 1$, we need a coloring of $\{1, \ldots, 2r^2 - 1\}$ -- that avoids monochromatic APs of length 3 and $r$. let ans : Σ r : ℕ, Icc 1 (2 * r^2 - 1) → Fin 2 := answer(sorry) let r := ans.1 let c := ans.2 3 ≤ r ∧ ¬ ((∃ s : Finset (Icc 1 (2 * r^2 - 1)), ({(s' : ℕ) | s' ∈ s}).IsAPOfLength 3 ∧ ∀ x ∈ s, c x = 0) ∨ (∃ s : Finset (Icc 1 (2 * r^2 - 1)), ({(s' : ℕ) | s' ∈ s}).IsAPOfLength r ∧ ∀ x ∈ s, c x = 1)) := 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