Erdős Problem #172
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
Attempts
submit one →Read our full write-up →
Hindman asked whether every finite colouring of the positive integers contains arbitrarily large finite sets whose nonempty subset sums and subset products all share one colour. Alweiss proved it over the rationals; over the integers it was open until OpenAI's 23 September 2026 paper claimed it. We read all 70 pages, checked every cited theorem against its current source, ran a hostile machine referee over the whole chain, and found that a third party (Yao Xu) has since written a 6-megabyte Lean 4 proof following the paper, sorry-free, with OpenAI's own library supplying the hardest half. Four sectioned hostile referee seats read the paper as written and found no gap — every cited theorem says what the paper says it says — and our own from-source kernel replay of the Lean proof printed the three standard axioms. The problem is closed.
CLOSED