Erdős problem 303 · problems.science

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

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

303.lean

Retained formal statement1 of 1

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.

FormalConjectures/ErdosProblems/303.leanErdos303.erdos_3033 linesExact file

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

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science