Skip to content

Erdős problem 46

Start work

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

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

46.lean

Retained formal statement1 of 3

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

The answer is yes, as proved by Croot [Cr03] - indeed, there are infinitely many disjoint such monochromatic solutions.

FormalConjectures/ErdosProblems/46.leanErdos46.erdos_461 lineExact file
True ↔ ∀ (𝓒 : ℕ → ℕ), (Set.range 𝓒).Finite → ∃ S, (∀ n ∈ S, 2 ≤ n) ∧ ∑ n ∈ S, 1 / ↑n = 1 ∧ (𝓒 '' ↑S).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.