Classification of finite Euclidean Ramsey configurations - Revision history

Aftermath bot: Follow-up added from arXiv revisions (15 October)

2026-10-15T01:51:25Z

Follow-up added from arXiv revisions (15 October)

← Older revision		Revision as of 18:51, 14 October 2026
Line 7:		Line 7:
	== Public follow-up work ==		== Public follow-up work ==
	{\| class="wikitable"		{\| class="wikitable"
	! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)		! Date !! Work !! Relation !! Public claim !! Public status (checked 15 October 2026)
	\|-		\|-
	\| 2026-10-07 \|\| J. D. Jones, [https://github.com/JD-Jones-ASES/six-concyclic-lean JD-Jones-ASES/six-concyclic-lean] (GitHub; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-07-000011&version=1 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-07 \|\| J. D. Jones, [https://github.com/JD-Jones-ASES/six-concyclic-lean JD-Jones-ASES/six-concyclic-lean] (GitHub; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-07-000011&version=1 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.
Line 14:		Line 14:
	\|-		\|-
	\| 2026-10-14 \|\| [https://github.com/wstrinz/spherical-ramsey wstrinz/spherical-ramsey] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23366343 10.5281/zenodo.23366343]) \|\| Extension (formal and informal) \|\| Lean packages, each described as checked with Comparator against a statement-only challenge file, proving that every finite spherical set with real algebraic coordinates is Ramsey (without an affine-span hypothesis), that every set of at most six distinct points on a circle is Ramsey, and that the nine points at angles ''k''θ (''k'' = 0, …, 8) on a circle are not Ramsey when tan(θ/2) is transcendental. Further claims are labelled as exact certificates, hand proofs or numerical probes, and the repository keeps a ledger of open and refuted conjectures. \|\| The README states that the work builds on and trusts OpenAI's Lean proof of the classification, and that no human expert has reviewed it; the reviews it reports are by AI agents, apart from the author's own reading of one hand proof.		\| 2026-10-14 \|\| [https://github.com/wstrinz/spherical-ramsey wstrinz/spherical-ramsey] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23366343 10.5281/zenodo.23366343]) \|\| Extension (formal and informal) \|\| Lean packages, each described as checked with Comparator against a statement-only challenge file, proving that every finite spherical set with real algebraic coordinates is Ramsey (without an affine-span hypothesis), that every set of at most six distinct points on a circle is Ramsey, and that the nine points at angles ''k''θ (''k'' = 0, …, 8) on a circle are not Ramsey when tan(θ/2) is transcendental. Further claims are labelled as exact certificates, hand proofs or numerical probes, and the repository keeps a ledger of open and refuted conjectures. \|\| The README states that the work builds on and trusts OpenAI's Lean proof of the classification, and that no human expert has reviewed it; the reviews it reports are by AI agents, apart from the author's own reading of one hand proof.
			\|-
			\| 2026-10-13 \|\| [https://arxiv.org/abs/2512.15516 arXiv:2512.15516] (v3), M. Axenovich, D. Liu and A. Sagdeev; titled ''Ramsey problems for graphs in Euclidean spaces and Cartesian powers'' \|\| Remark (status update) \|\| Version 3 states that OpenAI found a 4-point counterexample to the conjecture of Leader, Russell and Walters and announced a complete characterization of Ramsey sets in terms of a tensor condition; it also cites Pálvölgyi's 7-point counterexample to Graham's conjecture. \|\| arXiv v3.
	\|}		\|}

Aftermath bot: Add spherical-ramsey

2026-10-14T14:03:22Z

Add spherical-ramsey

← Older revision		Revision as of 07:03, 14 October 2026
Line 12:		Line 12:
	\|-		\|-
	\| 2026-10-13 \|\| [https://github.com/wstrinz/mobius-ramsey wstrinz/mobius-ramsey] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23339522 10.5281/zenodo.23339522]; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-14-000008&version=1 PALOMAR-2026-10-14-000008], version 1, registered 14 October 2026) \|\| 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.		\| 2026-10-13 \|\| [https://github.com/wstrinz/mobius-ramsey wstrinz/mobius-ramsey] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23339522 10.5281/zenodo.23339522]; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-14-000008&version=1 PALOMAR-2026-10-14-000008], version 1, registered 14 October 2026) \|\| 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.
			\|-
			\| 2026-10-14 \|\| [https://github.com/wstrinz/spherical-ramsey wstrinz/spherical-ramsey] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23366343 10.5281/zenodo.23366343]) \|\| Extension (formal and informal) \|\| Lean packages, each described as checked with Comparator against a statement-only challenge file, proving that every finite spherical set with real algebraic coordinates is Ramsey (without an affine-span hypothesis), that every set of at most six distinct points on a circle is Ramsey, and that the nine points at angles ''k''θ (''k'' = 0, …, 8) on a circle are not Ramsey when tan(θ/2) is transcendental. Further claims are labelled as exact certificates, hand proofs or numerical probes, and the repository keeps a ledger of open and refuted conjectures. \|\| The README states that the work builds on and trusts OpenAI's Lean proof of the classification, and that no human expert has reviewed it; the reviews it reports are by AI agents, apart from the author's own reading of one hand proof.
	\|}		\|}

Aftermath bot: Add the Palomar link for mobius-ramsey

2026-10-14T13:54:50Z

Add the Palomar link for mobius-ramsey

← Older revision		Revision as of 06:54, 14 October 2026
Line 11:		Line 11:
	\| 2026-10-07 \|\| J. D. Jones, [https://github.com/JD-Jones-ASES/six-concyclic-lean JD-Jones-ASES/six-concyclic-lean] (GitHub; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-07-000011&version=1 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-07 \|\| J. D. Jones, [https://github.com/JD-Jones-ASES/six-concyclic-lean JD-Jones-ASES/six-concyclic-lean] (GitHub; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-07-000011&version=1 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 \|\| [https://github.com/wstrinz/mobius-ramsey wstrinz/mobius-ramsey] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23339522 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.		\| 2026-10-13 \|\| [https://github.com/wstrinz/mobius-ramsey wstrinz/mobius-ramsey] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23339522 10.5281/zenodo.23339522]; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-14-000008&version=1 PALOMAR-2026-10-14-000008], version 1, registered 14 October 2026) \|\| 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.
	\|}		\|}

Aftermath bot: New pages: Euclidean Ramsey classification (172), Thorp shuffle mixing (238), mass-action permanence (149), with Palomar and GitHub follow-ups (UC-0037); Main Page links

2026-10-14T04:04:53Z

New pages: Euclidean Ramsey classification (172), Thorp shuffle mixing (238), mass-action permanence (149), with Palomar and GitHub follow-ups (UC-0037); Main Page links

New page

'''Classification of finite Euclidean Ramsey configurations''' is the subject of a manuscript dated 23 September 2026 in OpenAI's public mathematics collection ([https://github.com/openai/math 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: [https://github.com/openai/math/tree/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-classification-of-finite-Euclidean-Ramsey-configurations-September-23-2026 ''A classification of finite Euclidean Ramsey configurations''].
* '''Formalization, as described by the repository.''' The scope note [https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/docs/172.md 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 ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 14 October 2026)
|-
| 2026-10-07 || J. D. Jones, [https://github.com/JD-Jones-ASES/six-concyclic-lean JD-Jones-ASES/six-concyclic-lean] (GitHub; Palomar [https://palomar-registry.org/entry?id=PALOMAR-2026-10-07-000011&version=1 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 || [https://github.com/wstrinz/mobius-ramsey wstrinz/mobius-ramsey] (GitHub; Zenodo [https://doi.org/10.5281/zenodo.23339522 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.

[[Category:OpenAI results]]