we-solve (beta)

Math-2226 · mathematics · Geometry

Chromatic number of the plane

Status Open · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Shared notation.
$\mathbb N$, $\mathbb Z$, $\mathbb Q$, $\mathbb R$, and $\mathbb C$ denote the natural numbers, integers, rationals, reals, and complex numbers, respectively. All additional parameters and hypotheses are specified in the question.
Statement recorded in the supplied source.
Determine the least number of colors needed to color the Euclidean plane so that points at unit distance receive different colors.

Formulation references: [S1], [S2].

Short English statement

Determine the least number of colors needed to color the Euclidean plane so that points at unit distance receive different colors.

Sources

Catalogue entry

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2226-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2226

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.

Chromatic number of the plane

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

Go to contribution →