Erdős Problem 303

Reference: erdosproblems.com/303

theorem erdos_303 : (∀ (𝓒 : ℤ → ℤ), (Set.range 𝓒).Finite → ∃ (a : ℤ) (b : ℤ) (c : ℤ), [a, b, c, 0].Nodup ∧ 1 / ↑a = 1 / ↑b + 1 / ↑c ∧ (𝓒 '' {a, b, c}).Subsingleton) ↔ True

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$?

This is true, as proved by Brown and Rödl [BrRo91].

[BrRo91] Brown, Tom C. and Rödl, Voijtech, Monochromatic solutions to equations with unit fractions. Bull. Austral. Math. Soc. (1991), 387-392.