Classification of finite Euclidean Ramsey configurations

1 paperLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

A classification of finite Euclidean Ramsey configurations

OpenAI · September 23, 2026

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.

Read PDF Download Source

Cite

@misc{OAI:A-classification-of-finite-Euclidean-Ramsey-configurations-September-23-2026,
  author = {{OpenAI}},
  title = {{A classification of finite Euclidean Ramsey configurations}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/A-classification-of-finite-Euclidean-Ramsey-configurations-September-23-2026/paper.pdf}{OAI:A-classification-of-finite-Euclidean-Ramsey-configurations-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

A classification of finite Euclidean Ramsey configurations

Scope

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.

Comparator links

Result	Comparator statement
Tensor-field classification of Ramsey configurations	EuclideanRamsey.lean
Twelve-point spherical non-Ramsey example	GrahamSpherical.lean
Ramsey property for at most five circle points	EuclideanRamseyCircle.lean
Nine-point non-Ramsey circle configuration	EuclideanRamseyNine.lean
Quadratic-independence criterion for spherical configurations	EuclideanRamseyQuadratic.lean
Cosphericity of Ramsey configurations	EuclideanRamseySpherical.lean
Ramsey property for subsets of finite transitive configurations	EuclideanRamseyTransitive.lean

Scope note on GitHub →