Erdős Problem #174
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).
A finite set `A ⊆ ℝⁿ` is Ramsey if for every number `k ≥ 1` of colours there is a dimension `d` such that every colouring of `ℝᵈ` with `k` colours has a monochromatic copy of `A`. A copy of `A` is the image of a map `p : A → ℝᵈ` that preserves all distances.
A finite set `X ⊆ ℝᵐ` is transitive if its symmetry group acts transitively: any point of `X` is mapped to any other point of `X` by an isometry of `ℝᵐ` that maps `X` onto itself [LRW12].
A set `A ⊆ ℝⁿ` is subtransitive if it is congruent to a subset of a finite transitive set in some `ℝᵐ`; the dimension `m` may be larger than `n` [LRW12].
Attempts
submit one →Read our full write-up →
A finite point set A is Ramsey if, for every number of colours, some Euclidean space is so large that every colouring of it contains a one-coloured congruent copy of A. Erdős asked which sets these are. In 1973 Erdős, Graham, Montgomery, Rothschild, Spencer and Straus showed they lie on a sphere; Graham conjectured the converse, and Leader, Russell and Walters conjectured instead that they are exactly the subsets of finite transitive sets. On 20 September Pálvölgyi, with a proof written by ChatGPT, refuted Graham's conjecture with seven points on a circle. OpenAI's preprint of 23 September (released 6 October) gives an exact test: A is Ramsey if and only if a certain matrix exists over the ring F ⊗ F, where F is the field generated by A's coordinates. Four AI seats briefed to refute it found nothing wrong, and neither did our own line-by-line read. OpenAI's Lean (65 modules) compiles here on the three standard axioms, and its seven statements match their comparator files. Ours: a Lean refutation of Formal Conjectures' "graham" statement, which FC still tags open, a Lean proof of its "spherical" statement, and a Lean proof of its main set equality with an explicit answer built from OpenAI's test. With an independently written procedure that decides the test when the coordinates involve one transcendental number, we also found that the smallest non-Ramsey subsets of OpenAI's twelve points have eight points. One of them is a square and a rectangle inscribed in one circle. None of this has been reviewed by a human expert.
CLOSEDRead our full write-up →
A preprint posted on 10 August proves that adjoining any point outside the affine hull of a finite Euclidean Ramsey set preserves the Ramsey property. This resolves Ivan-Leader-Walters Conjecture 8 and extends their earlier subsoluble-base result to arbitrary Ramsey bases. An independent proof audit found no gap; the full characterization in Problem 174 remains open.
PARTIAL