Classification of finite Euclidean Ramsey configurations

OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:

Classifies finite point configurations that occur monochromatically, at their original scale, in every finite coloring of sufficiently high-dimensional Euclidean space. The characterization is an algebraic condition over the coordinate field. It also disproves the Leader–Russell–Walters conjecture that every such configuration is a subset of a finite transitive set. (OpenAI’s Lean note)

Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.

The independent assessments find that the Lean statements express only part of the result described above, or a narrower statement. Read the assessments

It bears on Erdős problem #174, as listed by Thomas Bloom, erdosproblems.com.

What the papers state

The paper states

Theorem 1.1 (Classification)

In A classification of finite Euclidean Ramsey configurations, 23 September 2026

Possible match to OpenAI’s description, selected from shared wording. No review confirming the selection is recorded.

Let A=\{a_1,\ldots,a_s\}\subset\R^d be a finite set of at least two points with affine span \R^d, and define p_i,F,B,m_F as above. Then A is Ramsey if and only if there is a matrix P\in\operatorname{Mat}_{d+1}(B) such that

\begin{aligned}(p_i\otimes1)^T P(1\otimes p_i)&=0 &&(1\le i\le s),\\ m_F(P_{\alpha\beta})&=\delta_{\alpha\beta} &&(1\le\alpha,\beta\le d).\end{aligned}

Here the entries of p_i\otimes1 and 1\otimes p_i are formed componentwise. There are no separate conditions on the multiplied constant row or constant column of P.

The release does not say which paper theorem its catalogue describes. The statement above shares the most wording with the description; the atlas has not reviewed that choice. Identifying it is listed under Questions awaiting review.

Reported proof verification: Seven Lean statements in the release; independent groups report that Comparator accepted runs for all these files at the version shown here.
Papers and explanations: One current paper, readable here as a page beside its PDF.

Papers

Each paper opens as a reading page in the browser, with the PDF beside it. The statements each paper opens with are on its reading page.

A classification of finite Euclidean Ramsey configurations

23 September 2026, current edition.

Read it here PDF

We classify finite Euclidean Ramsey configurations by a necessary and sufficient tensor condition over their coordinate fields. The Ramsey property here concerns monochromatic congruent copies at the original scale under arbitrary finite colorings. The criterion shows that every nonempty subtransitive set and every nonempty set of at most five points on a circle is Ramsey. In particular, some Ramsey cyclic quadrilaterals are not subtransitive, disproving the necessity direction of the Leader–Russell–Walters conjectured characterization.

Seven Lean statements in this family

Choose one to see it beside the paper theorem it is paired with.

For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.

Tensor-field classification of Ramsey configurations
EuclideanRamsey, main result
Paper theorem
Possible Lean counterpart of Theorem 1.1 in A classification of finite Euclidean Ramsey configurations, found from shared wording; not reviewed.
Proof-verification reports
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.
Ramsey property for at most five circle points
EuclideanRamseyCircle, supporting statement
Paper theorem
Possible Lean counterpart of Corollary 7.4 in A classification of finite Euclidean Ramsey configurations, found from shared wording; not reviewed.
Proof-verification reports
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.
Nine-point non-Ramsey circle configuration
EuclideanRamseyNine, supporting statement
Paper theorem
Possible Lean counterpart of Proposition 7.6 in A classification of finite Euclidean Ramsey configurations, found from shared wording; not reviewed.
Proof-verification reports
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.
Quadratic-independence criterion for spherical configurations
EuclideanRamseyQuadratic, supporting statement
Paper theorem
Possible Lean counterpart of Proposition 7.3 in A classification of finite Euclidean Ramsey configurations, found from shared wording; not reviewed.
Proof-verification reports
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.
Cosphericity of Ramsey configurations
EuclideanRamseySpherical, supporting statement
Paper theorem
Possible Lean counterpart of Proposition 2.4 in A classification of finite Euclidean Ramsey configurations, found from shared wording; not reviewed.
Proof-verification reports
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.
Ramsey property for subsets of finite transitive configurations
EuclideanRamseyTransitive, supporting statement
Paper theorem
Possible Lean counterpart of Corollary 7.2 in A classification of finite Euclidean Ramsey configurations, found from shared wording; not reviewed.
Proof-verification reports
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.
Twelve-point spherical non-Ramsey example
GrahamSpherical, main result
Paper theorem
Possible Lean counterpart of Proposition 7.6 in A classification of finite Euclidean Ramsey configurations, found from shared wording; not reviewed.
Proof-verification reports
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.

`EuclideanRamsey`

The paper states

Theorem 1.1 (Classification)

In A classification of finite Euclidean Ramsey configurations, 23 September 2026

\begin{aligned}(p_i\otimes1)^T P(1\otimes p_i)&=0 &&(1\le i\le s),\\ m_F(P_{\alpha\beta})&=\delta_{\alpha\beta} &&(1\le\alpha,\beta\le d).\end{aligned}

Here the entries of p_i\otimes1 and 1\otimes p_i are formed componentwise. There are no separate conditions on the multiplied constant row or constant column of P.

The words they share: affine, classification, finite, points, ramsey, span.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Tensor-field classification of Ramsey configurations

EuclideanRamsey.lean, the release lists it as a main result.

theorem classification {s d : ℕ} (a : Fin s → Space d)    (hs : 2 ≤ s) (hd : 1 ≤ d) (ha : Function.Injective a)    (hspan : affineSpan ℝ (Set.range a) = ⊤) :    Ramsey a ↔ FieldCriterion a := by  sorry

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program

cert-machine records it as “CERTIFIED”.
MathVet records it as “comparator-sandboxed-pass”.
Neal McBurnett, openai-math-lean-tooling records it as “accepted”.

Read the complete Lean statement

`EuclideanRamseyCircle`

The paper states

Corollary 7.4

In A classification of finite Euclidean Ramsey configurations, 23 September 2026

Every nonempty set of at most five distinct points on a circle is Ramsey. In particular, every cyclic quadrilateral is Ramsey.

The words they share: distinct, five, circle, nonempty, points, ramsey.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Ramsey property for at most five circle points

EuclideanRamseyCircle.lean, the release lists it as a supporting statement.

theorem at_most_five_circle_points_ramsey {s : ℕ} (a : Fin s → Space 2)    (hs : 0 < s) (hs5 : s ≤ 5) (ha : Function.Injective a)    (hsphere : ∃ c : Space 2, ∃ r : ℝ, ∀ i, dist (a i) c = r) : Ramsey a := by  sorry

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program

cert-machine records it as “CERTIFIED”.
MathVet records it as “comparator-sandboxed-pass”.
Neal McBurnett, openai-math-lean-tooling records it as “accepted”.

Read the complete Lean statement

`EuclideanRamseyNine`

The paper states

Proposition 7.6

In A classification of finite Euclidean Ramsey configurations, 23 September 2026

Let t_1,\ldots,t_9 be algebraically independent real numbers over \Q. The nine points

a_i=\left(\frac{1-t_i^2}{1+t_i^2}, \frac{2t_i}{1+t_i^2}\right),\qquad 1\le i\le9,

form a spherical set that is not Ramsey.

The words they share: real, algebraically, nine, independent, points, ramsey, spherical.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Nine-point non-Ramsey circle configuration

EuclideanRamseyNine.lean, the release lists it as a supporting statement.

theorem nine_circle_configuration (t : Fin 9 → ℝ)    (ht : AlgebraicIndependent ℚ t) :    Function.Injective (literalCircleConfig t) ∧      (∀ i, dist (literalCircleConfig t i) 0 = 1) ∧      ¬ Ramsey (literalCircleConfig t) := by  sorry

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program

cert-machine records it as “CERTIFIED”.
MathVet records it as “comparator-sandboxed-pass”.
Neal McBurnett, openai-math-lean-tooling records it as “accepted”.

Read the complete Lean statement

`EuclideanRamseyQuadratic`

The paper states

Proposition 7.3

In A classification of finite Euclidean Ramsey configurations, 23 September 2026

Let A=\{a_1,\ldots,a_s\}\subset\R^d be spherical and affinely span \R^d. Put p_i=(1,a_i)^{\mathsf T} and let F be its coordinate field. If the s row vectors

(p_{i\alpha}p_{i\beta})_{0\le\alpha,\beta\le d} \quad(1\le i\le s)

are linearly independent over F, then A is Ramsey.

The words they share: field, span, coordinate, independent, spherical, ramsey, row.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Quadratic-independence criterion for spherical configurations

EuclideanRamseyQuadratic.lean, the release lists it as a supporting statement.

theorem spherical_quadraticIndependent_ramsey_all {s d : ℕ}    (a : Fin s → Space d) (ha : Function.Injective a)    (hspan : affineSpan ℝ (Set.range a) = ⊤)    (hsphere : ∃ c : Space d, ∃ r : ℝ, ∀ i, dist (a i) c = r)    (hrows : LinearIndependent (Coeff a)      (fun i : Fin s => fun q : Option (Fin d) × Option (Fin d) =>        augmented a i q.1 * augmented a i q.2)) : Ramsey a := by  sorry

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program

cert-machine records it as “CERTIFIED”.
MathVet records it as “comparator-sandboxed-pass”.
Neal McBurnett, openai-math-lean-tooling records it as “accepted”.

Read the complete Lean statement

`EuclideanRamseySpherical`

The paper states

Proposition 2.4

In A classification of finite Euclidean Ramsey configurations, 23 September 2026

If (3) has no solution, then there is an integer r_0\geq2 such that every \R^D admits an r_0-coloring with no monochromatic congruent copy of A. In particular, every Euclidean Ramsey set satisfies the matrix condition of Theorem 1.1.

The words they share: congruent, integer, euclidean, ramsey, tensor, classification.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Cosphericity of Ramsey configurations

EuclideanRamseySpherical.lean, the release lists it as a supporting statement.

theorem ramsey_cospherical {s d : ℕ} (a : Fin s → Space d)    (ha : Function.Injective a) (hR : Ramsey a) :    EuclideanGeometry.Cospherical (Set.range a) := by  sorry

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program

cert-machine records it as “CERTIFIED”.
MathVet records it as “comparator-sandboxed-pass”.
Neal McBurnett, openai-math-lean-tooling records it as “accepted”.

Read the complete Lean statement

`EuclideanRamseyTransitive`

The paper states

Corollary 7.2

In A classification of finite Euclidean Ramsey configurations, 23 September 2026

Every nonempty subset of a finite transitive Euclidean set is Ramsey.

The words they share: transitive, finite, euclidean, ramsey, nonempty.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Ramsey property for subsets of finite transitive configurations

EuclideanRamseyTransitive.lean, the release lists it as a supporting statement.

theorem subset_of_finite_transitive_ramsey {s t D : ℕ}    (a : Fin s → Space D) (y : Fin t → Space D)    (hs : 0 < s) (ha : Function.Injective a) (_hy : Function.Injective y)    (htrans : ∀ i j : Fin t, ∃ σ : Equiv.Perm (Fin t),      (∀ k l : Fin t, dist (y (σ k)) (y (σ l)) = dist (y k) (y l)) ∧ σ i = j)    (hsub : Set.range a ⊆ Set.range y) : Ramsey a := by  sorry

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program

cert-machine records it as “CERTIFIED”.
MathVet records it as “comparator-sandboxed-pass”.
Neal McBurnett, openai-math-lean-tooling records it as “accepted”.

Read the complete Lean statement

`GrahamSpherical`

The paper states

Proposition 7.6

In A classification of finite Euclidean Ramsey configurations, 23 September 2026

Let t_1,\ldots,t_9 be algebraically independent real numbers over \Q. The nine points

a_i=\left(\frac{1-t_i^2}{1+t_i^2}, \frac{2t_i}{1+t_i^2}\right),\qquad 1\le i\le9,

form a spherical set that is not Ramsey.

The words they share: real, points, ramsey, algebraically, nine, independent, spherical.

Possible Lean counterpart

Selected from shared wording. No review of whether the statements mean the same thing is recorded.

Twelve-point spherical non-Ramsey example

GrahamSpherical.lean, the release lists it as a main result.

def FullAuthoredResult : Prop :=  witness.ncard = 12 ∧  witness ⊆ Metric.sphere (0 : Point 2) 1 ∧  (∀ n : ℕ, 0 < n → ∃ color : Point n → Fin 50, AvoidsCopy witness color) ∧  ¬ EuclideanRamsey witness⋮theorem full_main : Specification.FullAuthoredResult := by  sorry

This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.

three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program

cert-machine records it as “CERTIFIED”.
MathVet records it as “comparator-sandboxed-pass”.
Neal McBurnett, openai-math-lean-tooling records it as “accepted”.

Read the complete Lean statement

Other mathematical statements in OpenAI’s Lean library

Atlas found these propositions by scanning the text of the project’s Model.lean file. Each name links to its definition, with any associated statement file beside it. This list does not record running Lean to interpret or verify those definitions.

Congruent Model.lean, line 11
Ramsey Model.lean, line 14
FieldCriterion Model.lean, line 35
AvoidsCopy Model.lean, line 43
EuclideanRamsey Model.lean, line 46
FullAuthoredResult Model.lean, line 58

Independent comparisons and proof-verification reports

Does the Lean express the advertised result?

Neither group finds that the Lean statements express or imply the whole advertised result. They describe what the statements express in different terms.

MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.

MathVet finds that the Lean statements express part of the advertised result (their term: “partial”).

Their note: Classification is only for full-affine-span configurations: classification (hs : 2 ≤ s) (hd : 1 ≤ d) (ha : Injective a) (hspan : affineSpan ℝ (range a) = ⊤) : Ramsey a ↔ FieldCriterion a (docs: ‘for full-affine-span configurations’; the isometric re-embedding reduction to this case is not a challenge statement). The summary’s disproof of the Leader-Russell-Walters conjecture has no statement: only the Ramsey half is present (at_most_five_circle_points_ramsey, nine_circle_configuration, GrahamSpherical.full_main = a 12-point non-Ramsey spherical set), nothing says some Ramsey configuration is not contained in a finite transitive set.

“partial”, in their words: Only a special case is stated, or a co-equal headline claim has no challenge statement.

Their method: An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.

Read the original assessment Read MathVet’s method

cert-machine finds that the Lean statements express a narrower statement than the advertised result (their term: “NARROWER — UNDECLARED”).

The gap they name: The existence of a Ramsey configuration that is not subtransitive — the actual counterexample to the LRW conjecture. Its non-subtransitivity half is a cited prior theorem in the paper, not proved there and not in Lean.

“NARROWER — UNDECLARED”, in their words: The challenge statements state less than the headline, and OpenAI’s Lean note does not say so.

Their method: Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule.

Read the original assessment Read cert-machine’s method

OpenAI’s own note on what its Lean covers

A finite configuration is Euclidean Ramsey if every finite coloring of some sufficiently high-dimensional Euclidean space contains a monochromatic congruent copy at the original scale. The formalization gives the tensor-field classification for full-affine-span configurations, covers singleton and affine-span reductions, and proves that every Ramsey configuration is cospherical. It also proves that every nonempty subset of a finite transitive configuration and every nonempty set of at most five points on a circle is Ramsey. A further sufficient condition uses linear independence of the quadratic evaluation rows of a spherical configuration.
The formalization also gives spherical non-Ramsey examples: the specified twelve-point set on the unit circle has a fifty-color obstruction in every positive dimension, and a nine-point circle configuration built from algebraically independent parameters is non-Ramsey.

AI-drafted comparisons, with no recorded human review

Tensor-field classification of Ramsey configurations EuclideanRamsey
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main classification theorem for configurations of full affine span, with the singleton and affine-span reductions.
Ramsey property for at most five circle points EuclideanRamseyCircle
Unreviewed AI draft: states a consequence of a paper’s theorem. States the corollary that every set of at most five points on a circle is Ramsey, from the paper’s section of geometric consequences and examples of the classification.
Nine-point non-Ramsey circle configuration EuclideanRamseyNine
Unreviewed AI draft: states a consequence of a paper’s theorem. States the nine-point non-Ramsey circle configuration built from algebraically independent parameters, a proposition in the paper’s section of geometric consequences and examples.
Quadratic-independence criterion for spherical configurations EuclideanRamseyQuadratic
Unreviewed AI draft: states a consequence of a paper’s theorem. States the quadratic-independence sufficient condition for spherical configurations to be Ramsey, a proposition in the paper’s section of geometric consequences and examples.
Cosphericity of Ramsey configurations EuclideanRamseySpherical
Unreviewed AI draft: states a consequence of a paper’s theorem. States the corollary that every finite Ramsey configuration is spherical, from the paper’s section of geometric consequences and examples of the classification.
Ramsey property for subsets of finite transitive configurations EuclideanRamseyTransitive
Unreviewed AI draft: states a consequence of a paper’s theorem. States the corollary that every nonempty subset of a finite transitive configuration is Ramsey, from the paper’s section of geometric consequences and examples.
Twelve-point spherical non-Ramsey example GrahamSpherical
Unreviewed AI draft: states a consequence of a paper’s theorem. States the twelve-point spherical non-Ramsey example with a fifty-colour obstruction in every dimension, a proposition in the paper’s section of geometric consequences and examples of the classification.

Who ran the proof-verification program?

These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.

These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.