Green's Open Problem 23

References:

• Green, Ben. "100 open problems." (2024).
• [FrKlMo25] Frantzikinakis, N., O. Klurman, and J. Moreira. "Partition regularity of Pythagorean pairs." Forum of Mathematics, Pi 13. Cambridge University Press (2025).

theorem Green23.green_23 : True ↔ ∀ (k : ℕ) (c : ℕ → Fin k), ∃ (x : ℕ) (y : ℕ), 0 < x ∧ 0 < y ∧ c x = c y ∧ IsSquare (x ^ 2 + y ^ 2)

Suppose that $\mathbb{N}$ is finitely coloured. Are there $x,y$ of the same colour such that $x^2 + y^2$ is a square?

Solved in [FrKlMo25].