Lean formalization in OpenAI math repository (Result 172)
Model / AI: OpenAI (unreleased)
OpenAI's internal frontier model proved and formalized in Lean the main result of '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.
Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 172). The Lean development was not rebuilt locally.