Erdős problem 46
Does every finite colouring of the integers have a monochromatic solution to with ?
Sources
FormalConjectures/ErdosProblems/
46.lean
Retained formal statement
In [ErGr80] they also ask for a monochromatic representation of any .
True ↔ ∀ (𝓒 : ℕ → ℕ), (Set.range 𝓒).Finite → ∀ (q : ℚ), 0 < q → ∃ S, (∀ n ∈ S, 2 ≤ n) ∧ ∑ n ∈ S, 1 / ↑n = q ∧ (𝓒 '' ↑S).SubsingletonSolvedStatement only, no proof