green_23

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].

theorem green_23 :
  answer(True) ↔
    -- For every finite colouring of the natural numbers
    ∀ (k : ℕ) (c : ℕ → Fin k),
    -- there exist two numbers of the same colour whose squares sum to a square
    ∃ x y : ℕ,
      0 < x ∧ 0 < y ∧  -- Exclude trivial x^2 + 0^2 = x^2 solution
      c x = c y ∧      -- Same colour
      IsSquare (x^2 + y^2)

Recent Submissions

No submissions yet. Be the first to attempt this problem.