The Hadwiger-Nelson Problem

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.

The Hadwiger-Nelson Problem

Definitions and mathematical statement

The unit-distance graph of the plane has vertex set ${\mathbb{R}}^2$, with an edge between $x,y$ precisely when $|x-y|=1$. Its chromatic number is \[ \chi({\mathbb{R}}^2)=\min\{k\in{\mathbb{N}}:\exists c:{\mathbb{R}}^2\to\{1,\ldots,k\}, \ |x-y|=1\Rightarrow c(x)\ne c(y)\}. \] Determine this integer in ordinary ZFC. The coloring is an arbitrary function; its color classes need not be measurable, open, or periodic. Colorings of only a finite set of points provide obstructions but are not by themselves colorings of the whole plane. The exact-value target is separate from merely improving a lower or upper bound.

Formulation and concept references: [S1].

Short English statement

What is the smallest number of colors that can color the entire plane without giving the same color to two points exactly one unit apart?

Research attempt

Current frontier.

De Grey's finite unit-distance obstruction establishes the lower bound five; the ordinary upper bound seven and the remaining exact-value question are recalled in the same work. [S1]. The second catalogue reference concerns regular-polygon Minkowski norms, not a resolution for Euclidean distance. [S2], Abstract. Recent work proving seven colors necessary for specified map-type colorings imposes regularity that is expressly absent here. [E1], Introduction. The present attempt therefore keeps arbitrary ZFC colorings, and pursues exact algebraic finite witnesses rather than assuming color classes are measurable or tiles.

Attack route.

A periodic tiling might improve the upper bound, but rules out most allowable colorings at the outset. A finite graph can improve the lower bound, but must have exact unit edges, not merely visually close ones. The selected route combines compactness with real algebraic geometry to locate all necessary finite obstructions over number fields. We then test whether dense rational-coordinate searches could implement this route; an explicit two-coloring shows why they cannot.

Attempt.

1. Algebraic coordinates lose no finite obstruction. Let $H$ be a finite graph realized by distinct points $p_1,\ldots,p_N$ in the Euclidean plane, with every edge at distance one. Its realization is an existential system over ${\mathbb{Q}}$: \[ (x_i-x_j)^2+(y_i-y_j)^2=1\quad(ij\in E(H)),\qquad (x_i-x_j)^2+(y_i-y_j)^2>0\quad(i\ne j). \] Additional inequalities $\ne1$ may be imposed for nonedges, although they are unnecessary for a coloring obstruction. The real algebraic numbers form a real closed field. Quantifier elimination for real closed fields therefore transfers this finite existential statement from ${\mathbb{R}}$ to ${\mathbb{R}}\cap\overline{\mathbb{Q}}$. Thus every finite real unit-distance obstruction has an exact real-algebraic realization. This use of transfer, and not a numerical perturbation, preserves all required unit lengths. [E2], real-closed-field decision theorem.

For completeness, a graph with possibly infinitely many vertices is $k$-colorable if all its finite subgraphs are. In ZFC this follows by compactness of the product $\{1,\ldots,k\}^{V}$: the closed cylinder conditions forbidding equal colors on an edge have the finite intersection property. If every finite subgraph is colorable, their intersection is nonempty. Apply this to the plane and combine it with the preceding transfer. We obtain \begin{equation}\label{wsref-0-31-30-3a-61-6c-67-65-62-72-61-69-63} \chi({\mathbb{R}}^2)=\chi\left(({\mathbb{R}}\cap\overline{\mathbb{Q}})^2\right). \end{equation} There is even some finite real number field $K$ with $\chi(K^2)=\chi({\mathbb{R}}^2)$. Indeed, since the chromatic number is a finite integer, failure of a coloring with one fewer colors has a finite witness; all the algebraic coordinates of that witness generate one finite extension $K/{\mathbb{Q}}$. Inclusion gives the other inequality. This argument asserts existence, not a degree bound for $K$ or a bound on the number of vertices of the witness.

2. An exact rational-coordinate obstruction to the search strategy. Despite density of ${\mathbb{Q}}^2$ in the plane, its unit-distance graph is bipartite. Here is a proof with the denominator issue included. Put \[ R={\mathbb{Z}}_{(2)}=\{a/b\in{\mathbb{Q}}:b\text{ odd}\}. \] Every rational unit vector $(u,v)$ belongs to $R^2$. Otherwise choose a common denominator with a positive power of two and clear its odd part. After removing the common power of two from the numerators, the equation $u^2+v^2=1$ would say that the sum of two integer squares, at least one odd, is divisible by four. It is congruent to either one or two modulo four, a contradiction. Reducing $u^2+v^2=1$ modulo two now gives \begin{equation}\label{wsref-0-31-30-3a-70-61-72-69-74-79} \overline u+\overline v=1\quad\hbox{in }R/2R\cong{\mathbb{F}}_2. \end{equation}

Choose one representative $r_C$ for each coset $C$ of $R^2$ in ${\mathbb{Q}}^2$. For $p\in C$, color $p$ by the sum modulo two of the coordinates of $p-r_C$. A unit edge stays within one coset, because its displacement is in $R^2$, and (10:parity) says that its endpoint colors differ. This is a well-defined arbitrary two-coloring. Edges exist, so \[ \chi({\mathbb{Q}}^2)=2. \] Consequently no amount of rational-grid refinement can find even a three-chromatic unit-distance graph with exact rational coordinates. Rounding an algebraic realization to rational points necessarily breaks some crucial unit equations. Topological density is not density in the space of exact unit-distance realizations.

3. What an algebraic search can certify. One can enumerate finite graphs, decide their $k$-colorability by finite exhaustion, and decide the existential real realization system above. If $\chi({\mathbb{R}}^2)>k$, compactness guarantees that this search eventually finds a finite obstruction. Alternatively one can enumerate exact algebraic points and test edges using real-algebraic arithmetic. Thus lower-bound witnesses are discoverable in principle.

Neither procedure tells us when to stop searching for a nonexistent witness. The assertion that every finite graph in this geometric class is $k$-colorable is universal over an unbounded family, not a single real-closed-field sentence. Quantifier elimination for each finite graph does not decide the chromatic number of the infinite plane. The number-field observation in (10:algebraic) likewise has no uniform bound on degree, height, or graph size.

Two exact filters are useful but insufficient. Distinct vertices of a unit-distance graph have at most two common neighbors, because two circles of radius one have at most two intersection points. Hence $K_{2,3}$ cannot occur even as a noninduced subgraph. Also, a vertex-critical $k$-chromatic graph has minimum degree at least $k-1$: otherwise a $(k-1)$-coloring after deleting a low-degree vertex extends to it. A hypothetical six-chromatic obstruction can therefore be chosen with minimum degree five and no $K_{2,3}$. These combinatorial restrictions do not establish geometric realizability of the surviving candidates.

An attempted upper-bound transfer fails in the opposite direction: the two-coloring of ${\mathbb{Q}}^2$ has no continuity property and cannot be extended by taking limits along rational points. Even imposing a choice of limiting color would not preserve all unit edges. The exact argument proving (10:algebraic) uses algebraic transfer plus compactness, not density or continuity.

Stress test.

No measure is assigned to color classes. Compactness is used in ordinary ZFC, matching the entry. Algebraic realizations keep vertices distinct; forgetting that condition could collapse a purported graph obstruction. The coloring proof for ${\mathbb{Q}}^2$ treats every denominator through cosets of ${\mathbb{Z}}_{(2)}^2$, rather than assuming that all rational points have odd denominators. The circle-intersection filter concerns distinct centers; coincident centers are excluded by the realization inequalities.

Finite witnesses give lower bounds only. The present argument constructs neither a six-chromatic graph nor a five- or six-coloring of the whole plane. The map-type restrictions in [E1] cannot replace either of these missing objects.

Outcome.

Outcome: Exploratory approach with unresolved gap.

The attempt gives an exact number-field search framework and proves that rational-coordinate searches are structurally incapable of discovering the relevant obstructions. It also identifies necessary critical-graph filters. These deductions are useful diagnostics, not a new numerical bound or a claim of priority for compactness or rational-plane coloring.

A resolution still requires an unrestricted upper coloring or an exact finite obstruction strong enough to close the remaining integer gap. No bounded stopping criterion for the algebraic search has been obtained.

Sources

• S1 de Grey, The chromatic number of the plane is at least 5 $2018$. https://arxiv.org/abs/1804.02385. Catalogue formulation source.
• S2 Status source for Chromatic Number of the Plane (Hadwiger--Nelson Problem). https://arxiv.org/abs/2108.12861. Catalogue research/status reference; not a proof endorsement.
• E1 G. Sokolov and V. Voronov, On the chromatic number of the plane for map-type colorings, arXiv:2502.01958, Introduction and the hypotheses of its map-type coloring theorems. https://arxiv.org/abs/2502.01958. Consulted 27 September 2026; no inference for arbitrary ZFC colorings is made.
• E2 A. Tarski, A Decision Method for Elementary Algebra and Geometry, 2nd ed., University of California Press, 1951, the decision and elimination method for ordered real closed fields. https://www.rand.org/pubs/reports/R109.html. Used for the finite realization transfer, not for a decision procedure for the infinite unit-distance graph.