we-solve (beta)

Math-2619 · mathematics · Combinatorics

Five-colorability of the unit-distance plane

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
Does there exist a map $c:R^2->{1,2,3,4,5}$ such that $c(x)!=c(y)$ whenever $||x-y||=1$, with arbitrary color classes and ordinary ZFC?

Short English statement

Does there exist a map $c:R^2->{1,2,3,4,5}$ such that $c(x)!=c(y)$ whenever $||x-y||=1$, with arbitrary color classes and ordinary ZFC?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

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

OpenAI claim summary for Math-2619

Plane coloring with five labels: The manuscript’s result states there is no proper five-coloring even with arbitrary color classes in ZFC. A proper coloring means precisely that each pair at Euclidean distance one has unequal colors; the measurable intermediate reductions do not add a restriction to the final theorem.

The claimed counterexample lies within the question’s hypotheses and contradicts its universal conclusion.

Five-colorability of the unit-distance 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 →