Green's Open Problem 22

References:

• [Gr26] Ben Green's Open Problems
• [Mo17] Moreira, Joel. "Monochromatic sums and products in N." Annals of Mathematics 185.3 (2017): 1069-1090.
• [GrSa25] Green, Ben, and Mehtaab Sawhney. "Bounds for monochromatic solutions to $\{x+ y, xy\} $." arXiv preprint arXiv:2511.09365 (2025).
• [Ri25] Richter, Florian K. "Sums and products in sets of positive density." arXiv preprint arXiv:2507.00515 (2025).
• [BoSa24] Bowen, Matt, and Marcin Sabok. "Monochromatic products and sums in the rationals." Forum of Mathematics, Pi. Vol. 12. Cambridge University Press, 2024.
• [Bo25] Bowen, Matt. "Monochromatic products and sums in 2-colorings of N." Advances in Mathematics 462 (2025): 110095.
• [Al23] Alweiss, Ryan. "Monochromatic Sums and Products over $\mathbb {Q} $." arXiv preprint arXiv:2307.08901 (2023).

def Green22.HasMonochromaticSumProduct (N r : ℕ) (coloring : ↥(Finset.Icc 1 N) → Fin r) : Prop

The monochromatic sum-product property: a colouring $c$ of $\{1, \ldots, N\}$ has a pair $(x, y)$ with $x, y \geq 3$ such that $x + y$ and $xy$ are both in $\{1, \ldots, N\}$ and receive the same colour.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Green22.N₀ (r : ℕ) : ℕ

$N_0(r)$ is the smallest $N$ such that every $r$-colouring of $\{1, \ldots, N\}$ has the monochromatic sum-product property.

Equations

• Green22.N₀ r = sInf {N : ℕ | ∀ (c : ↥(Finset.Icc 1 N) → Fin r), Green22.HasMonochromaticSumProduct N r c}

noncomputable def Green22.GreenSawhneyBound (r : ℕ) : ℝ

The upper bound function from [GrSa25].

Equations

• Green22.GreenSawhneyBound r = Real.exp (Real.exp (↑r ^ 50))

theorem Green22.green_22 : have ans := sorry; ∀ᶠ (r : ℕ) in Filter.atTop, ↑(N₀ r) ≤ ans r ∧ ans =o[Filter.atTop] GreenSawhneyBound

If $\{1, \ldots, N\}$ is $r$-coloured then, for $N \geqslant N_0(r)$, there are integers $x, y \geqslant 3$ such that $x + y, xy$ have the same colour.

Find reasonable bounds for $N_0(r)$. The goal is to improve upon the Green-Sawhney bound.

theorem Green22.green_22.variants.green_sawhney_bound : ∀ᶠ (r : ℕ) in Filter.atTop, ↑(N₀ r) ≤ GreenSawhneyBound r

[GrSa25, Theorem 1.1] found a permissible upper bound.

theorem Green22.green_22.variants.moreira_infinite (r : ℕ) (coloring : ℕ → Fin r) : {p : ℕ × ℕ | 0 < p.1 ∧ 0 < p.2 ∧ coloring p.1 = coloring (p.1 * p.2) ∧ coloring p.1 = coloring (p.1 + p.2)}.Infinite

[Mo17, Corollary 1.5] For any finite coloring of $\mathbb{N}$ there exist (infinitely many) $x, y \in \mathbb{N}$ such that $\{xy, x + y\}$ is monochromatic.

This guarantees that $N_0(r)$ is well-defined.

Note: [Mo17] also establishes that $x$ is of the same colour.

theorem Green22.green_22.variants.lower_nine (r : ℕ) : r ≠ 0 → 9 ≤ N₀ r

Since $x, y \geq 3$, we must have $xy \geq 9$, so $N_0(r) \geq 9$ (assuming $N_0(r)$ is well-defined, which follows from [Mo17]).