Erdős problem 46

Does every finite colouring of the integers have a monochromatic solution to $1=\sum \frac{1}{n_i}$ with $2\leq n_1<\cdots <n_k$ ?

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

46.lean

Retained formal statement3 of 3

In [ErGr80] they also ask for a monochromatic representation of any $\frac{a}{b}>0$ .

FormalConjectures/ErdosProblems/46.leanErdos46.erdos_46.variants.positive_rat3 linesExact file

1True ↔2  ∀ (𝓒 : ℕ → ℕ),3    (Set.range 𝓒).Finite → ∀ (q : ℚ), 0 < q → ∃ S, (∀ n ∈ S, 2 ≤ n) ∧ ∑ n ∈ S, 1 / ↑n = q ∧ (𝓒 '' ↑S).Subsingleton

SolvedStatement only, no proof