Erdős problem 172
Is it true that in any finite colouring of there exist arbitrarily large finite such that all sums and products of distinct elements in are the same colour?
Sources
FormalConjectures/ErdosProblems/
172.lean
Retained formal statement
Is it true that in any finite colouring of there exist arbitrarily large finite such that all sums and products of distinct elements in are the same colour?
True ↔ ∀ (n : ℕ) (color : ℕ → Fin n) (m : ℕ), ∃ A, A.card ≥ m ∧ ∃ c, ∀ (S : Finset ↥A), S.Nonempty → color (∑ x ∈ S, ↑x) = c ∧ color (∏ x ∈ S, ↑x) = cOpenStatement only, no proof