Classification of finite Euclidean Ramsey configurations
Classification of finite Euclidean Ramsey configurations is the subject of a manuscript dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math). A finite point configuration is Euclidean Ramsey if every finite colouring of a sufficiently high-dimensional Euclidean space contains a monochromatic congruent copy of it. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
The original result
- Claim. Finite Euclidean Ramsey configurations are classified by a necessary and sufficient tensor condition over their coordinate fields, with monochromatic congruent copies at the original scale under arbitrary finite colourings. By the manuscript's summary, every nonempty subtransitive set and every nonempty set of at most five points on a circle is Ramsey, and the classification disproves the Leader–Russell–Walters conjecture that every Ramsey configuration is a subset of a finite transitive set. Source: A classification of finite Euclidean Ramsey configurations.
- Formalization, as described by the repository. The scope note lean/docs/172.md states that the Lean formalization gives the tensor-field classification for configurations of full affine span, covers singleton and affine-span reductions, proves that every Ramsey configuration is cospherical, and proves that every nonempty subset of a finite transitive configuration and every nonempty set of at most five points on a circle is Ramsey. It also gives spherical non-Ramsey examples, including a twelve-point set on the unit circle with a fifty-colour obstruction.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 14 October 2026) |
|---|---|---|---|---|
| 2026-10-07 | J. D. Jones, JD-Jones-ASES/six-concyclic-lean (GitHub; Palomar PALOMAR-2026-10-07-000011, version 1) | Use (formal) | A Lean development, with the criterion's definitions restated from the family's challenge file, proving that every set of six distinct points on a circle satisfies the tensor criterion by an explicit certificate, and that so does every spherical set of at most m + 4 points of affine dimension m and every algebraic spherical set. The Ramsey conclusions are stated as conditional on the classification's sufficiency half. | Registered in the Palomar registry on 7 October 2026. |
| 2026-10-13 | wstrinz/mobius-ramsey (GitHub; Zenodo 10.5281/zenodo.23339522) | Use (formal) | A Lean proof that the tensor condition is transported by the Lorentz group, so that a finite set of distinct points of the unit sphere is Ramsey if and only if its image under a Möbius transformation is; on a circle, the Ramsey property then depends only on cross-ratios. | The README states that the work builds on OpenAI's classification and cites as classical, rather than formalizing, the identification of these maps with the Möbius transformations. |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.