Is it true that in any finite colouring of the integers there exists a monochromatic solution to$$\frac{1}{a}=\frac{1}{b}+\frac{1}{c}$$with distinct $a,b,c$?

AMS 5 11 · solved (literature)

theorem erdos_303 :
    answer(True) ↔
    -- For any finite colouring of the integers
    ∀ (𝓒 : ℤ → ℤ), (Set.range 𝓒).Finite →
      -- There exists integers `a, b, c`
      ∃ (a b c : ℤ),
      -- that are non-zero and distinct.
      [a, b, c, 0].Nodup ∧
      -- `a, b, c` satisfy the equation
      (1/a : ℝ) = 1/b + 1/c ∧
      -- `a, b, c` have the same color
      (𝓒 '' {a, b, c}).Subsingleton