Combinatorics·OpenAI Math·Result 172·Lean formalisation listed
Classification of finite Euclidean Ramsey configurations
One of the 372 results in OpenAI's public mathematics catalogue, filed under combinatorics: 1 preprint, the latest dated 23 September 2026. This page quotes OpenAI's own summary of the claim, links the paper and abstract, and will embed the animation.
Latest paper
A classification of finite Euclidean Ramsey configurations
The animation for this result has not been released yet. Subscribe on YouTube to catch it.
What OpenAI claims
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. (Lean)
Paper
A classification of finite Euclidean Ramsey configurations
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.
Status
Preprint. The paper has not been independently reviewed. Treat the result as OpenAI's claim until other mathematicians have checked it. If a video exists, it illustrates the statement; it is not the proof.
Related results in Combinatorics
- 173Seymour’s second-neighborhood conjectureLean
- 174Deterministic construction of strong thin spanning treesLean
- 175Talagrand’s expectation thresholds, discrete convexity, and graph decompositionsLean
- 176The second Kahn–Kalai conjecture with an edge-count boundLean
- 177Bounded-degree coboundary expandersLean
- 178Deterministic nonbipartite Ramanujan graphs in every fixed degree