Ben Green's Open Problem 21

formal-conjectures · greens-open-problems · ams-5 · ams-11

Milićević [ElJo23, Conjecture 11.1] conjectures the following 2-adic variant. For any
$k \in \mathbb{N}$, there exists $K = K(k)$ such that the following is true. Let $r$ be a
positive integer, and let $a_1, \dots, a_k \in \mathbb{Z}/2^r\mathbb{Z}$. Let $d$ be the largest
integer such that $\sum_{i \in I} a_i \equiv 0 \pmod{2^d}$ for some non-empty subset
$I \subset [k]$. Then there is a $K$-colouring of $\mathbb{Z}/2^r\mathbb{Z}$ such that all
monochromatic solutions $x = (x_1, \dots, x_k)$ to the equation
$a_1x_1 + \cdots + a_kx_k = 0$ satisfy $x_i \equiv 0 \pmod{2^{r-d}}$ for all $i = 1, \dots, k$.

Milićević remarks that, if true, this would imply the Rado boundedness conjecture by a
compactness argument.

Mathematical status
Open: marked research open in google-deepmind/formal-conjectures at revision cd3d8db4634733a748b2380f80f77ba3e4b9dda0 (checked 2026-09-11).

Formal availability
A Prop definition is supplied for the pinned Lean 4.33.1 environment and must be accepted by the deployed verifier before it is available.

Sources and provenance
Upstream reference cited by formal-conjectures (checked 2026-09-11): https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#problem.21
Formal statement provenance (Apache-2.0) (checked 2026-09-11): https://github.com/google-deepmind/formal-conjectures/blob/cd3d8db4634733a748b2380f80f77ba3e4b9dda0/FormalConjectures/GreensOpenProblems/21.lean
Local target: Corpus.Green21.green_21.variants.milicevic
Source SHA-256: 5252dbb58e7da7c55e495fd246965fb1e8eebf3d0e96e9b12e7dc8f20b59adc8
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.

Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.

Public JSON record