#174: an exact algebraic test for which finite point sets are Euclidean Ramsey — OpenAI's classification, read by AI seats here and its Lean replayed; Formal Conjectures' open-tagged Graham conjecture refuted in Lean from OpenAI's twelve points, and FC's main statement proved with an explicit answer

The problem. Erdős problem #174 [Er75f, p. 108; ErGr79; ErGr80; Er83c]: "A finite set A ⊂ ℝⁿ is called Ramsey if, for any k ≥ 1, there exists some d = d(A,k) such that in any k-colouring of ℝ^d there exists a monochromatic copy of A. Characterise the Ramsey sets in ℝⁿ." A copy means a congruent copy at the original scale, and the colourings are arbitrary functions. The page was last edited in October 2025 and, like the rest of the site, no longer shows a status; the teorth database still lists #174 as open. The page records two competing conjectures. Graham's says every spherical set is Ramsey. Leader, Russell and Walters' (LRW) says a set is Ramsey exactly when it is a subset of a finite transitive set. Our 11 August entry, #174: every Ramsey base admits a Ramsey pyramid, covered Moore's one-point extension theorem.

Graham's conjecture was refuted first, by Pálvölgyi. Pálvölgyi's arXiv preprint of 20 September (2609.23327, v1, a manuscript he says was written entirely by ChatGPT) takes r transcendental, r > 2, and the seven points (0,0) and (j, ±√(j(2r−j))) for j = 1, 3, 4. These lie on the circle (x−r)² + y² = r², and Theorem 1 says they are not Ramsey. The proof takes a derivation D of ℝ with D(r) = 1 and integer weights λ whose moments Σλ, Σλp, Σλppᵀ, ΣλD(p) and Σλ·D(p)pᵀ all vanish while Σλ‖D(p)‖² does not. With R = (2r−1)(2r−3)(2r−4), the function F(q) = R·Σ D(q_i)² then has the same weighted sum, −24, over every congruent copy in every dimension, and a Rado colouring of its values avoids the set. We recomputed these identities symbolically and they hold as printed. He posted it on the #174 forum on 23 September.

The claim. OpenAI's family 172, "A classification of finite Euclidean Ramsey configurations" (23 September, 26 pp., released 6 October). Let A = {a₁,…,a_s} ⊂ ℝ^d, s ≥ 2, with affine span ℝ^d. Put p_i = (1, a_i), let F be the field generated over ℚ by all the coordinates, B = F ⊗_ℚ F, and m_F : B → F the multiplication map. Theorem 1.1: A is Ramsey if and only if there is a (d+1)×(d+1) matrix P over B with (p_i ⊗ 1)ᵀ P (1 ⊗ p_i) = 0 for every i and m_F(P_αβ) = δ_αβ on the spatial block. Applying m_F to the first condition gives a quadric through the points, and the second condition makes it a sphere. The test asks whether that sphere equation lifts to the tensor ring before multiplying. Theorem 1.1 is an existential algebraic criterion. Whether it is the characterisation Erdős asked for is a judgment; we mark the problem closed on that reading. The paper gives no general procedure for deciding the criterion; its Remark 2.2 shows only that the relevant kernel is finitely generated. Section 7 derives these consequences:

• every Ramsey set is spherical (Cor. 7.1, the 1973 theorem);
• every subset of a finite transitive set is Ramsey (Cor. 7.2, the direction of LRW's conjecture that Pálvölgyi announced and has not posted);
• spherical sets whose quadratic evaluation rows are independent over F are Ramsey (Prop. 7.3);
• every set of at most five points on a circle is Ramsey (Cor. 7.4);
• for transcendental a ∈ (−1,1), the kites (−1,0), (1,0), (a, ±√(1−a²)) are Ramsey, while LRW 2011 proved them not subtransitive, so LRW's characterisation fails (Cor. 7.5);
• nine points (1−t_i², 2t_i)/(1+t_i²) with t₁,…,t₉ algebraically independent are not Ramsey (Prop. 7.6);
• three concentric squares, the coordinate square and its rotations by ±θ with tan(θ/2) = Liouville's constant, form twelve points that are not Ramsey (Prop. 7.7).

The argument. Necessity (§2): if no such matrix exists, a ℚ-linear functional separates the identity from the image of the evaluation map. Its components give functions h_i on ℝ with Σ_i H_i(b_i) = −1 on every congruent copy (b_i) in every dimension, where H_i(z) = Σ_j h_i(z_j), and Σ_i H_i = 0 at every single point. Colour z by where each H_i(z) mod 2 falls among 2s+1 intervals. A monochromatic copy would make −1 equal to an even integer plus an error of size less than 1, which is impossible. That is (2s+1)^s colours in every dimension. Sufficiency (§§3–6) is the harder part. A finite lattice identity (Lemma 3.1, through completion and flatness) and Gaussian smoothing with exact rationalisation (Lemmas 4.2, 4.3) turn the tensor into two lists of affine functions. Evaluated at A, these give two copies of A, one at scale 1 and one with squared distances scaled by an arbitrarily small q, whose corresponding points have the same coordinates in different orders (Lemma 4.1). Paths in a free group record products of scaled copies (§5). Averaging over coordinate permutations makes the two endpoints agree at small extra cost, through a derived-series argument on right fractions (§6). An ultrafilter realisation and the Hales–Jewett theorem then produce the copy (§5.3). One endpoint is prepared with paths of weights 1, ½, …, 1/n before the colouring is seen. Whatever the number t of variable positions in the monochromatic line, the copy then has squared-distance factor t·(1/t) = 1 exactly, with no continuity needed.

The Lean, and our replay. OpenAI's Lean for this family has two parts, and neither imports the other. OAI/Combinatorics/EuclideanRamsey (47 modules) proves the classification and the consequences other than Prop. 7.7 and the cited half of Cor. 7.5. OAI/Combinatorics/SphericalRamsey (18 modules in the closure) proves the twelve-point result directly, without the classification: a derivation D of ℝ with D(t) = (1+t²)/2, the energy Σ D(y_j)², weights 1, 1, −2 on the three squares, a weighted sum of 8 on every copy, and the colouring ⌊3e⌋ mod 50. That is stronger than the paper, which states no colour count. We compiled the 65-module closure (9,589 lines; openai/math @ 1581d4c, Lean v4.34.1, Mathlib d13f23b) lake-free on our machine: 65/65 modules, 0 errors, 6 min 7 s wall, peak per-module memory 6.7 GiB. With --trust=0 the seven comparator theorems depend only on propext, Classical.choice and Quot.sound. Their statements and definitions, 49 blocks in all, match the seven comparator files under pp.all, with sorryAx visible on every challenge. The matcher passed a mutation test seven ways, and a planted sorry surfaces as sorryAx. Seat L read the source: no sorry, axiom, native_decide, extern, unsafe, set_option or notation tricks, and no instance on any type that appears in a statement. The Lean follows the paper's route stage by stage. Four sub-lemmas (Prop. 2.1's descent, Lemma 3.1, Lemma 4.2, Lemma 5.2) are proved there by different arguments, so the kernel checks their statements, not the paper's own proofs of them. Seats O and T, both machine seats, read those proofs line by line. Not formalised: Remarks 2.2–2.3, and the non-subtransitivity half of Cor. 7.5, which is a citation to LRW. An independent kernel re-check, leanchecker --fresh over the whole closure plus our algebraic-coordinates bridge, exited with code 0 after 3,603 s (peak memory 8.2 GiB); a missing-module control exits 1.

The reading. Four seats, all Claude Opus 5.5, were each briefed to refute, to quote the sentence they objected to, and to grade each objection. Seat O took §§1–4, seat T §§5–6 (the sufficiency half), seat L the Lean against the paper, and seat W the sources and the world. All four returned HOLDS AS READ, with exposition notes only. The main seat also read all of §§2–7 line by line and found nothing to add. O ran Lemma 3.1 through Lemma 4.1 end to end in exact arithmetic on the two-point set {0, 1}. It got ‖f₁−f₂‖² = 1 and ‖g₁−g₂‖² = 1/21 with equal coordinate multisets. It also made the necessity functional explicit for non-spherical sets, where it is the classical 1973 invariant. A search over 769,470 copy parameters found no monochromatic copy; with only K = 2 intervals the same search does find them. T simulated §5.3's string realisation with arbitrary common strings in place of the ultrafilter choices, which are not constructive: 30 line realisations for a two-point set, from a genuine equal-endpoint pair, and 27 for an equilateral triangle, from synthetic paths. Every distance came out exactly A's. T also built Lemma 6.2's commutator from real unit triangles and checked the first derived step of Lemma 6.3's averaging with Fox derivatives, which is all s = 3 needs. Its notes: Lemma 5.4's Zorn step does not say the intersection is again a compact left ideal. The product rule (20) is Hindman–Strauss Thm 4.12(b) (second edition), which the paper does not cite. (27) should say "for every x ∈ Z", and in Lemma 6.1 the differences are generated by telescoping, without a normal closure. We recomputed Prop. 7.6's determinant exactly (64 at the paper's grid, nonzero at random rational points, zero on the diagonal) and the moment identities (31) of Prop. 7.7. A fifth, blind seat (B) then checked this page against the files before it went up. Its corrections are applied; one of them reversed a claim in our first draft (see the eight-point paragraph below).

Formal Conjectures, and the bridges (ours). Formal Conjectures (FC) added ErdosProblems/174.lean on 20 October (PR #7469). It tags erdos_174.variants.graham (every finite spherical set is Ramsey) and the LRW equivalence "research open", and it leaves erdos_174.variants.spherical, tagged solved, as a sorry. Our Bridge174FC.lean copies FC's IsRamsey and both statements verbatim, checked by a script whose mutated run fails.

• It derives the negation of FC's graham statement from OpenAI's twelve-point theorem OAI.GrahamSpherical.full_main. The one step that needs care is that ℝ⁰ cannot hold a copy of two distinct points, so FC's "some d" becomes OpenAI's "some d > 0".
• It proves FC's spherical statement from OpenAI's ramsey_cospherical, by enumerating the finite set and translating between FC's set-based copies and OpenAI's indexed ones.
• FC's main statement, erdos_174, is a set equality {A | IsRamsey A} = erdos_174.answer n, with the answer left as sorry. Bridge174Main.lean proves that equality with FC's left-hand side verbatim and an explicit answer built from OpenAI's criterion. The answer is the finite sets that have at most one point, or are congruent, through an explicit labelling, to a full-span configuration satisfying FieldCriterion. As a non-vacuity check it also proves that OpenAI's twelve points are not in that answer. Whether an existential algebraic criterion is the answer FC wants is FC's call.

All of these depend only on the three standard axioms. Five mutants fail to compile, each at the step that uses what it removed:

• the refutation restricted to sets of at most five points;
• the spherical conclusion strengthened to "A has at most one point";
• a changed IsRamsey;
• the criterion dropped from the answer;
• the one-point case dropped from the answer.

A separate leanchecker --fresh over Bridge174Main, which contains the main-statement bridge and imports the other two FC results and OpenAI's closure, exited with code 0 after 3,556 s (peak memory 8.2 GiB). We did not bridge the LRW equivalence. Its "only if" direction is false (Cor. 7.5), but proving that in Lean needs LRW's non-subtransitivity theorem, which we did not find formalised anywhere. An FC issue is drafted and waiting for Patrick, not filed.

Algebraic coordinates (not ours). One consequence follows in a few lines and is in neither the paper nor OpenAI's Lean. If every coordinate is algebraic, F is a number field. Then F ⊗ F splits as a product of fields, the kernel of m_F is generated by an idempotent e, and (1−e)·(H ⊗ 1) satisfies the test, with H the ordinary sphere matrix. So every spherical set with algebraic coordinates is Ramsey, and only transcendental coordinates can break Graham's conjecture. This is consistent with every non-Ramsey example on this page. We derived it, and seat L, asked whether OpenAI's Lean contains it, gave the same proof. We kernel-checked it from OpenAI's classification for configurations with full affine span (Bridge174.lean, standard axioms, three mutants fail). Seat W then found the same statement already public, in four AI-generated repositories built on OpenAI's paper. One is JD-Jones-ASES/six-concyclic-lean, from 7 October; its Lean theorem even has the same name as ours, algebraic_spherical_fieldCriterion. The others are Rogerhu12/openai-math-extensions (7 October, TeX), atimics/math2 (8 October, end to end in Lean) and wstrinz/spherical-ramsey (14 October, in Lean with no affine-span hypothesis). None has had human review, and W found the statement in no arXiv or peer-reviewed source. Ours is an independent replication, not a first.

Deciding the test with one transcendental (an independent implementation, not a first). When F = ℚ(τ) for one transcendental τ, B embeds in ℚ(x, y), m_F is y ↦ x, and B localised at ker m_F is a discrete valuation ring with uniformiser x − y. The test then reduces to linear algebra. We compute the kernel of the evaluation equations over ℚ(x, y), symbolically, and saturate it at x − y. The test holds exactly when some combination of the reduced basis, at y = x, has spatial block I. A saturated basis spans the whole kernel over that ring, so a "fails" is a proof of failure, given Theorem 1.1. wstrinz/spherical-ramsey released an exact decision procedure for one-parameter sets on a circle on 14 October (exact_circle_cert.py), built on the same localisation at the diagonal. Ours was written without reading it. A second, separately written check (exact rationals, no computer algebra) fixes τ at rational values and takes the limit y → x there, through Plücker coordinates. It is a spot check of the symbolic computation at τ = 2/7 and −5/3, not a second proof, and both rest on the same reduction. The controls behave:

• the union of two squares (a transitive set) passes;
• a transcendental kite passes, as does a five-point set (Cor. 7.4);
• three collinear points fail;
• seven rational points on a circle pass.

What it found:

• Prop. 7.7's twelve points fail for a simpler reason than the paper gives. Their 12 × 9 tensor matrix has full rank 9 over ℚ(x, y). One rational point with rank 9 already proves this, and exact elimination finds it at five. So the only P is zero, exactly as in Prop. 7.6's determinant argument. Every one of the 220 nine-point subsets is already full rank, so each is non-Ramsey too. This fits a pattern wstrinz reports: nonzero 9 × 9 determinants for 176 one-parameter nine-point samples on the circle.
• Every subset of the twelve points with at most seven points passes (128 orbits of six-point subsets and 104 of seven-point subsets, under the set's eight symmetries). At eight points, 67 orbits pass and 5 fail. The spot check agrees with the symbolic computation on all 304 orbits. So the smallest non-Ramsey subsets of OpenAI's twelve points have eight points. The "fails" side needs only the necessity half of Theorem 1.1. The minimality, that every seven-point subset is Ramsey, uses the sufficiency half.
• One of the five is the square {(±1,0),(0,±1)} together with the rectangle {(±u,±v)} inscribed in the same circle, with u = cos θ, v = sin θ and tan(θ/2) any transcendental number. Each half is transitive, but the union is not Ramsey. Our procedure says it fails the test: its reduced kernel is one-dimensional with spatial block a multiple of [[0, −τ(τ−1)(τ+1)], [τ(τ−1)(τ+1), 0]], never the identity. It also has an elementary first-order certificate, so its non-Ramseyness does not depend on Theorem 1.1 at all. The weights are −2u² on (±1,0), −2v² on (0,±1) and 1 on each rectangle point. With D = d/dτ, all the moments of Pálvölgyi's Lemma A.1 vanish except Σλ·D(p)pᵀ, which is symmetric (diagonal, nonzero), and that is all his lemma needs. The energy Σλ‖D(p)‖² = 16/(1+τ²)² is nonzero. Seat B found this certificate. Our first draft said no derivation certificate exists, because our script had required Σλ·D(p)pᵀ to vanish, the special case used in Pálvölgyi's Theorem 1 and in Prop. 7.7. All five failing orbits have such certificates, and the passing controls we tried have none, so for these twelve points the test and the first-order certificates agree. We have not found this eight-point example in the paper, Pálvölgyi's preprint, or the READMEs and frontier notes of the four repositories. We did not read wstrinz's note or ledger, which treat one-parameter seven- and eight-point circle sets. It does not contradict wstrinz's conjecture that points in general position on a circle are Ramsey exactly when there are fewer than nine, because a square with a rectangle is not in general position.
• Six and seven points. Random one-parameter configurations of six and seven points on a circle (Möbius images of τ mixed with rational points) all pass: all 40 of the six-point configurations we drew and all 40 of the seven-point ones. This is consistent with the published AI claims that any six concyclic points are Ramsey (JD-Jones for the criterion; wstrinz in Lean, through OpenAI's sufficiency) and that seven is the smallest size of a non-Ramsey concyclic set (wstrinz; Pálvölgyi's heptagon, and his Theorem A.3 for generic seven-point sets). Pálvölgyi's heptagon does not fit the one-parameter census: its coordinate field ℚ(r, √(2r−1), √(6r−9), √(2r−4)) is the function field of a curve of positive genus, not a field ℚ(τ). Whether every seven-point concyclic set with coordinates in some ℚ(τ) is Ramsey is a question this evidence raises but does not settle.

Sources and the world. Seat W read the primary text of nearly every citation, and all were accurate:

• EGMRSS 1973, Theorem 13 ("If K is not spherical, then K is not Ramsey"), Lemma 15 and Proposition 4;
• Graham 1994;
• LRW 2011, Corollary 2 (exactly the paper's kite with a transcendental; W re-derived its reduction) and Conjecture 3, which has an α/a typo in the source;
• LRW 2012, Conjecture A;
• Pálvölgyi's Theorems 1, A.2 and A.3 and his author's note;
• Moore, Mirabi, Behague, Ivan–Leader–Walters, Karamanlis, Ellis and Stacks 00MB;
• Hindman–Strauss, with the numbering checked only against the second edition (the paper cites the first).

Kříž and Cantwell could not be fetched, and secondary sources agree with how the paper uses them. Pálvölgyi's preprint is still v1, and his announced proof that all transitive sets are Ramsey has not appeared. The only arXiv response W found is Axenovich–Liu–Sagdeev (2512.15516 v3, 13 October), which mentions that OpenAI "announced" a characterisation. The teorth database still lists #174 as open, the problem page does not mention OpenAI's paper, and nothing public disputes it. FC's statement of Cor. 7.4 was merged as solved on 21 October (PR #6980), while its 174.lean still calls Graham's conjecture open. openai/math has issues disabled, and no file of this family has changed since release.

What this entry is. A referee report on someone else's theorem. The classification, its proof and its Lean are OpenAI's. Graham's conjecture was refuted first by Pálvölgyi, and the algebraic-coordinates corollary and an exact one-parameter procedure were first published in the repositories named above. Ours: the replay and its controls, the three bridges to Formal Conjectures and their controls, the readings, the twelve-point subset census, and the square-plus-rectangle example with its certificate. Labels, as on every entry here: (a) elementary proof · (b) rigorous modulo a named theorem · (c) plausible, unverified by a human · (d) computer-assisted.

• Theorem 1.1 and its consequences: (d), a Lean proof kernel-replayed here. The non-subtransitivity half of Cor. 7.5 is (b) modulo LRW 2011.
• The paper's own proofs of the four lemmas the kernel does not check (Prop. 2.1's descent, Lemmas 3.1, 4.2 and 5.2): (c). Machine seats read them line by line and found no gap; no human has.
• The bridges: (d).
• The square plus rectangle is not Ramsey: (a)+(d). The certificate is elementary and was verified in exact arithmetic.
• The twelve-point rank observation and the census: (d) computations, whose consequences for Ramsey sets are (b) modulo Theorem 1.1. The "fails" side uses only necessity; the minimality uses sufficiency.
• The seven-point question: (c).

If you are looking for a hole, look first at §6's cost bookkeeping, the most intricate part of the proof that is not in a standard library. Then look at our decision procedure's reduction to a discrete valuation ring. Our own first draft got the derivation-certificate question wrong by testing a special case. The files are in the bundle below; the repository is private at the time of writing, and the files are available on request.