OpenAI claim summary for Math-224
mathematicsTop Open Problemscontributionliterature_reportClaim: literature report
Summary of a claim published in openai/math; not a claim by this platform.
Plane coloring with five labels: The theorem gives 6<=chi(R^2)<=7 for arbitrary colorings in ZFC. It does not decide which of these two integers is the exact chromatic number.
This page records partial support. Complete resolution of the catalogue question is not established by this record.
Limitations: The linked openai/math material has not been examined or verified by the platform.
Manuscript
Contents
The Hadwiger-Nelson Problem
OpenAI's claim
Plane coloring with five labels: OpenAI claims that five colors cannot properly color the planar unit-distance graph, even with arbitrary nonmeasurable color classes. Together with the seven-color construction, this restricts the possible chromatic number to six or seven.Mathematical statement of the claimed result
Mathematical claim 1.
Let the unit-distance graph have vertex set $\mathbb R^2$ and edges between pairs at distance $1$. The manuscript claims \[\nexists c:\mathbb R^2\to\{1,\ldots,5\}\quad\text{with}\quad|x-y|=1\Longrightarrow c(x)\ne c(y).\] Arbitrary, including nonmeasurable, color classes are allowed in ZFC. With the standard seven-color upper bound this gives $6\le\chi(\mathbb R^2)\le7$, leaving the exact value between these two integers undecided.Outline of the argument
Plane coloring with five labels: The first part transfers arbitrary proper colorings to a measurable weakening in which monochromatic unit pairs have product measure zero. The second part uses the geometry of that measurable condition to rule out five labels. This bridge is essential because an obstruction only to measurable colorings would leave the original unrestricted question unanswered.Formal verification
Family 158 describes Lean coverage for the unrestricted obstruction with five labels and the construction using seven labels.Plane coloring with five labels: The manuscript links EuclideanFiveColor.lean (declaration OAI.EuclideanFiveColor.no_proper_five_coloring), PlaneColoring.lean (declaration OAI.Problem160.properColoring_seven).
The documented selection includes this manuscript’s main assertion; that assertion retains the restrictions stated above.
This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.
Status caveat
OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.Sources
- OpenAI, The Euclidean plane is not five-colorable, 2026-09-23; citation key
OAI:The-Euclidean-plane-is-not-five-colorable-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: thm:main; Statement source: thm:transfer; Statement source: thm:weak-five; Statement source: cor:positive-badness. - Family 158: Lean scope.
- Comparator EuclideanFiveColor.json.
- Comparator EuclideanFiveColor.lean.
- Comparator PlaneColoring.json.
- Comparator PlaneColoring.lean.
- OpenAI catalogue entry.