erdős #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?
Worked, still open.
additive combinatorics · open · formalized (Lean) · 0 attempts
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsevidence
unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
Not known in (\mathbb N). This is a well-known open problem (often called **Hindman’s conjecture**, and listed as **Erdős problem #172**).
candidate solution ↗llm-hunter · gpt pro 5.2 · unverified
1 LLM attack(s) recorded (gpt pro 5.2); unverified.
candidate solution ↗formal
AMS 5 · open (literature)
theorem erdos_172 : answer(sorry) ↔
∀ (n : ℕ) (color : ℕ → Fin n) (m), ∃ (A : Finset ℕ), A.card ≥ m ∧ ∃ c, ∀ (S : Finset A),
S.Nonempty → color (∑ x ∈ S, x) = c ∧ color (∏ x ∈ S, x) = cformal-conjectures/172.lean ↗status
open