Erdős problem 172

Is it true that in any finite colouring of $\mathbb{N}$ there exist arbitrarily large finite $A$ such that all sums and products of distinct elements in $A$ are the same colour?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

172.lean

Retained formal statement1 of 1

Is it true that in any finite colouring of $\mathbb{N}$ there exist arbitrarily large finite $A$ such that all sums and products of distinct elements in $A$ are the same colour?

FormalConjectures/ErdosProblems/172.leanErdos172.erdos_1723 linesExact file

1True ↔2  ∀ (n : ℕ) (color : ℕ → Fin n) (m : ℕ),3    ∃ A, A.card ≥ m ∧ ∃ c, ∀ (S : Finset ↥A), S.Nonempty → color (∑ x ∈ S, ↑x) = c ∧ color (∏ x ∈ S, ↑x) = c

OpenStatement only, no proof