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

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/303.lean

Formal Conjectures

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.

Proof manifests naming this Problem

Jayyhk Erdős Leanjayyhk:erdos:303
PLBY Lean proofsErdosProblems.Erdos303

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Formalization
Erdős AI contributions wiki · 21 Dec, 2025
Machine
Seed Prover
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science