Erdős Problem 303

References:

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

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

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

This was formalized in Lean by Yuan using Seed-Prover.