---

Claim. OpenAI, A classification of finite Euclidean Ramsey configurations, OpenAI Math Release preprint, 23 September 2026, linked above at the pinned revision and carded at openai_2026_classification_finite_euclidean_ramsey_configurations, with its main theorem paged at Theorem 1.1. The paper answers Problem 174 with an algebraic criterion. Let $A=\{a_1,\dots,a_s\}$ be a finite set of $s\ge2$ points; every such set is congruent to a representative in $\mathbb R^d$ whose affine span is $\mathbb R^d$, where $d$ is its affine dimension, and the criterion is stated for that representative. Let $F$ be the field generated over $\mathbb Q$ by the $sd$ coordinates, let $B=F\otimes_{\mathbb Q}F$, let $m_F:B\to F$ be the multiplication map $x\otimes y\mapsto xy$, and let $p_i=(1,a_i)\in F^{d+1}$ with its entries indexed by $0,1,\dots,d$. The paper's Theorem 1.1 states that $A$ is Ramsey if and only if there is a $(d+1)\times(d+1)$ matrix $P$ with entries in $B$ such that

$$(p_i\otimes1)^{\mathsf T}\,P\,(1\otimes p_i)=0\quad(1\le i\le s) \qquad\text{and}\qquad m_F(P_{\alpha\beta})=\delta_{\alpha\beta}\quad(1\le\alpha,\beta\le d).$$

A one-point set is Ramsey, and so is the empty set, so the theorem covers every finite set. Applying $m_F$ to the first family of equations gives an ordinary sphere equation through the points, so the criterion refines the sphericity condition of Erdős, Graham, Montgomery, Rothschild, Spencer and Straus by asking that the identities hold in $B$ before multiplication. The condition depends only on the congruence class of $A$. The paper proves necessity by turning a separating functional into a finite coloring that avoids $A$ in every dimension, and sufficiency by converting the tensor identities into a monochromatic congruent copy at scale one. No decision procedure for the criterion is proved: the test uses exact relations among the coordinates in $F$, and the paper says it is not a procedure for recovering those relations from numerical approximations.

The same paper bears on both conjectured characterizations, in different standings. Its twelve-point set, three rotated coordinate squares on the unit circle with a transcendental rotation parameter, is spherical and not Ramsey, so Graham's conjecture that every spherical set is Ramsey is false; this refutation is built in Lean (GrahamSpherical.full_main below) and is part of the accepted record. The first claimed disproof of that conjecture, unreviewed, is Pálvölgyi's seven-point set of 20 September 2026, which has its own claim page. The paper further claims, through its Corollary 7.4, that every nonempty set of at most five concyclic points is Ramsey, which would make the cyclic kites of Leader, Russell and Walters Ramsey while Corollary 2 of their 2011 paper records that those kites are not subtransitive; the Leader–Russell–Walters conjecture that the Ramsey sets are exactly the subtransitive sets would then be false in the necessity direction, together with their conjecture that the kites are not Ramsey. That corollary is not among the declarations the corpus built, and the corpus has not reviewed the step, so this refutation is the release's claim and not part of the accepted record. The paper also claims that every subtransitive set satisfies the criterion and that nine concyclic points with algebraically independent parameters fail it, in the same standing.

Formal verification. The release's Lean development, the lean/ folder at the pinned revision linked above, states the result as follows. OAI.EuclideanRamsey.classification, in OAI/Combinatorics/EuclideanRamsey/Main.lean, proves Ramsey a ↔ FieldCriterion a for an injective family a : Fin s → EuclideanSpace ℝ (Fin d) with 2 ≤ s, 1 ≤ d and full affine span; FieldCriterion is the displayed matrix condition over Coeff a ⊗[ℚ] Coeff a, where Coeff a is the intermediate field of $\mathbb R$ adjoining the coordinates. OAI.EuclideanRamsey.classification_nonempty, in the same file, removes the span hypothesis: for every injective nonempty family in any dimension, Ramsey a holds exactly when s = 1 or some congruent full-span representative satisfies FieldCriterion. OAI.EuclideanRamsey.quadratic_empty_ramsey, in OAI/Combinatorics/EuclideanRamsey/Quadratic.lean, covers the empty family. Ramsey asks, for every r ≥ 2, for a dimension D ≥ 1 in which every coloring EuclideanSpace ℝ (Fin D) → Fin r has a congruent monochromatic copy, congruence meaning equal pairwise distances; the problem's count of $k\ge1$ colors differs only in the trivial one-color case. OAI.GrahamSpherical.full_main, in OAI/Combinatorics/SphericalRamsey/Main.lean, proves that the twelve-point witness set has twelve points on the unit circle, that for every positive dimension a coloring with fifty colors has no monochromatic isometric copy of it, and that it is not Ramsey. The corpus's verification built these four declarations and checked their axioms: each uses only propext, Classical.choice and Quot.sound. The comparator challenges lean/ComparatorChallenges/EuclideanRamsey.lean and lean/ComparatorChallenges/GrahamSpherical.lean pin the statements of classification and full_main, and the pinned fingerprints were identical at the build; classification_nonempty and quadratic_empty_ramsey are not comparator-pinned and were axiom-checked directly. The kite corollary rests on the manuscript and on Leader, Russell and Walters's published non-subtransitivity result; the release lists further comparator files for the five-point, transitive, spherical and nine-point statements, which are not part of this record.

Depends on. No page of this wiki.

Acceptance. The evidence is formalized: the kernel-checked proof whose statement the corpus audited against the problem and built as described above. The standing is answered because the question asks for a characterization and the answer is an algebraic test, neither a yes nor a no. What the test does not supply is a decision procedure or a geometric description of the Ramsey sets, and the corpus records that limit without treating it as a gap in the theorem. No referee and no outside reviewer has examined the manuscript as recorded here; the site's page labels the problem open, was last edited on 16 October 2025, and its proof-claims thread carried no claim as of 6 October 2026. The release's README says its manuscripts were produced by an internal OpenAI model and that the collection includes results at different stages of verification.