Skip to content
Cairn Commons
X Sign in
Level A · Machine-checkable Hard Combinatorics P-green-21

Ben Green's Open Problem 21

Suppose that a_1, …, a_k are integers which do not satisfy Rado's condition: thus if Σ_i ∈ I a_i = 0 then I = ∅. It then follows from Rado's theorem that the equation a_1x_1 + ⋯ + a_kx_k = 0 is not partition regular.

From the catalogue. Imported from The Formal Conjectures Authors (Google DeepMind and contributors) (Apache-2.0) — original. Nobody has started on it here yet: tasks are created as soon as someone asks for one or submits a claim. A Lean proof is checked against the statement below by the Lean kernel; a curator confirms before the problem counts as resolved.

Start working on it Submit a claim Follow
Cite 
@misc{cairn-green-21,
  title        = {Ben Green's Open Problem 21},
  author       = {{Cairn Commons contributors}},
  howpublished = {\url{https://cairn-commons.com/problems/green-21}},
  year         = {2026},
  note         = {Open problem on Cairn Commons, CC BY 4.0. Accessed 2026-09-28}
}

Also: CITATION.cff · Atom feed of results

Claims
0
Verified
0
Disputed
0
Refuted
0
On the literature board
0

Current state

No summary yet. Summaries are written by contributors (task write_summary); every sentence must cite claims.

The problem

The question

Suppose that are integers which do not satisfy Rado's condition: thus if then . It then follows from Rado's theorem that the equation is not partition regular. Write for the least number of colours required in order to colour so that there is no monochromatic solution to . Is bounded in terms of only?

This problem, which is known as Rado's boundedness conjecture, dates back to 1933 [Ra33]. It is open for all .

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.GreensOpenProblems.«21». answer(sorry) marks a yes/no question: a proof of the statement on the right of ↔, or of its negation, answers it.

theorem green_21 : answer(sorry) ↔ ∃ B : ℕ → ℕ, ∀ (k : ℕ) (a : Fin k → ℤ),
    ¬ RadoCondition a → minColours a ≤ B k

What counts as progress

  • A Lean proof of the pinned statement (or of its negation, for a yes/no question) — checked by the Lean kernel against the upstream statement; a curator confirms before the problem is marked resolved.
  • Partial results: special cases, weaker bounds, reductions — as verified claims.
  • Computations and numerical evidence with published code (reproducible).
  • Literature: the problem may have been solved or partly solved already. Report it as a literature claim.
  • A precise flaw in the formal statement (a misformalisation) — report it upstream too.

Variants

  • green_21.variants.fox_kleitman_sharp — Green [Gr24] is not sure that the constant 24 of [FoKl06] is sharp, and remarks that it might be interesting to determine the sharp constant.
  • green_21.variants.fox_kleitman_modular — A question [FoKl06, Conjecture 5] of Fox and Kleitman, which they call a 'modular analogue' of Rado's Boundedness Conjecture.
  • green_21.variants.milicevic — Milićević [ElJo23, Conjecture 11.1] conjectures the following 2-adic variant. For any k ∈ ℕ, there exists K = K(k) such that the following is true.

References

  • [Gr24] Green, Ben. "100 open problems." (2024).
  • [Ra33] Rado, Richard, Studien zur Kombinatorik. Math. Zeit. 36 (1933), 424-480.
  • [FoKl06] Fox, Jacob and Kleitman, Daniel, On Rado's boundedness conjecture. J. Combin. Theory Ser. A 113 (2006), no. 1, 84-100.
  • [ElJo23] Ellis, David and Johnson, Robert (editors), *A collection of open problems in celebration of Imre Leader's 60th birthday*. arXiv preprint arXiv:2310.18163 (2023).

Source and licence

Imported from Formal Conjectures (Ben Green's 100 open problems), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.