Erdős problem 46 · problems.science

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

No current result

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

FormalConjectures/ErdosProblems/46.lean

Formal Conjectures

FormalConjectures/ErdosProblems/46.leanErdos46.erdos_461 lineExact file

1True ↔ ∀ (𝓒 : ℕ → ℕ), (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.