A classification of finite Euclidean Ramsey configurations

Follow-up works

• JD Jones, Six concyclic points satisfy the Euclidean Ramsey tensor criterion, as does every spherical set of at most m + 4 points of affine dimension m and every algebraic spherical set (GitHub six-concyclic-lean; Palomar entry PALOMAR-2026-10-07-000011, 2026-10-07). Lean development showing that six concyclic points, and spherical sets of at most m + 4 points, satisfy the manuscript's tensor criterion; the Ramsey conclusions take the sufficiency half of Theorem 1.1 as an explicit hypothesis.
• Will Strinz, Möbius invariance of the Ramsey property for finite spherical sets (GitHub mobius-ramsey; Palomar entry PALOMAR-2026-10-14-000008, 2026-10-14). Lean development deriving from the classification that the Ramsey property of finite unit-sphere sets is invariant under Möbius maps (modelled by the Lorentz group), reusing the release's Lean proof; the README states no human expert has reviewed it. [AI-generated per source]
• Will Strinz, Algebraic points on a circle plus at most three arbitrary points are Euclidean Ramsey (GitHub; Palomar entry PALOMAR-2026-10-16-000018, 2026-10-16). Lean result, built on the release's sufficiency theorem and Möbius invariance, that a finite circle set is Ramsey when all but at most three points have algebraic coordinates. [AI-generated per source]
• Will Strinz, The radian nine-gon is Euclidean Ramsey iff e^(i theta) is algebraic (GitHub; Palomar entry PALOMAR-2026-10-18-000020, 2026-10-18). Adapts the manuscript's nine-point non-Ramsey example (Proposition 7.6, algebraically independent parameters) to the one-parameter family of points at angles 0, θ, …, 8θ. [AI-generated per source]
• Will Strinz, spherical-ramsey (GitHub, 2026). Umbrella repository with Lean proofs, exact certificates, numerical probes and a conjecture ledger on which finite spherical sets are Ramsey; it explicitly trusts the release's Lean proof of the classification. [AI-generated per source]

Formalization

• OpenAI, Lean scope note for family 172 (openai/math release, 2026-10-06). The release's Lean development covers the tensor-field classification for full-affine-span configurations, cosphericity, the subtransitive and at-most-five-circle-points cases, the quadratic-independence criterion, and the nine- and twelve-point non-Ramsey circle configurations, with links to seven comparator statements. [family-level]
• Erdős Problems AI library, Openai 2026 classification finite euclidean ramsey configurations (verification report, accessed 2026-10-21). The site reports rebuilding three classification declarations and the twelve-point theorem and finding only propext, Classical.choice, and Quot.sound in their axiom dependencies, while excluding the other comparator statements from its build and audit.
• anxkhn, feat(Paper): add the five-point circle Ramsey result (google-deepmind/formal-conjectures PR #6980, merged 2026-10-21; issue #6975). Adds a Lean statement of the manuscript's Corollary 7.4 (at most five circle points are Ramsey), sourced to its Section 7, without a formal_proof attribute; reviewers checked the statement against the pinned manuscript.
• veljjanoski, feat(ErdosProblems/174): add Erdős Problem 174 (google-deepmind/formal-conjectures PR #7469, merged 2026-10-20). Formalizes the characterization problem with Graham's spherical conjecture and the Leader–Russell–Walters subtransitivity conjecture as open variants; it does not cite the manuscript, which claims to settle both.

Related prior literature mentioned by others

• Dömötör Pálvölgyi, A cyclic non-Ramsey heptagon (arXiv:2609.23327, 2026-09-20). Seven-point non-Ramsey circle set via weighted field-derivation identities, cited by the manuscript, which relies on its appendix Theorem A.3 for generic seven-point circle sets; the six-concyclic-lean README notes that this appendix is marked by its author as unverified language-model output.

Possibly relevant literature (found by the agent, not checked)

• Erdős Problems, Problem #174 (erdosproblems.com, last edited 2025-10-16; discussion thread). Asks to characterise the Ramsey sets in R^n, which is what Theorem 1.1 claims, and records Graham's spherical and the Leader–Russell–Walters subtransitive conjectures; the page and thread do not mention the manuscript.
• L. Milićević, Section 12 "A boundedness conjecture for Ramsey sets", in R. Baber et al., A collection of open problems in celebration of Imre Leader's 60th birthday (arXiv:2310.18163, 2023). Conjecture 12.1 asks whether the dimension D can be chosen depending only on the number of colours and the size of the Ramsey set, which concerns the dimension D in the manuscript's definition and Theorem 1.1.
• Gábor Damásdi, Nóra Frankl, János Pach, Dömötör Pálvölgyi, Monochromatic configurations on a circle (arXiv:2504.10687, 2025). Studies monochromatic inscribed configurations under colourings of a circle, a related setting for the manuscript's circle configurations.

Digests and expositions

• Latent Seminar, Exact-scale Euclidean Ramsey configurations (2026-10-07). Exposition of the tensor criterion, the five-point circle consequence, and the cancellation and path-weight synchronization mechanisms; it states that it has not independently verified the complete proofs or audited the Lean code. [family-level]