Hadwiger–Nelson problem
How many colours are needed to colour the plane so that no two points at distance 1 have the same colour?
Summary
AI-assisted claims
The Euclidean plane is not five-colorable
“We prove that every coloring of the Euclidean plane with five colors has a monochromatic unit-distance pair, with no regularity assumption on the color classes. Consequently, the chromatic number of the plane is either six or seven.”
- By
- OpenAI
- AI involvement
- This repository contains mathematical manuscripts and supporting proof artifacts produced by an internal OpenAI model.
- Model
- an unreleased internal OpenAI model, as stated
- Where
- openai/math repository
- Formal proof
- Lean 4, published by the source
- Checked
- 14 Oct 2026
Updates
Claims as their sources state them. Papex has not checked them; the status stays the source’s.
Why it is open
Seven colours are enough. Tile the plane with regular hexagons slightly less than one unit across and colour them in a repeating pattern of seven, so that tiles of the same colour are more than one unit apart; John Isbell observed this in 1950, the year Edward Nelson first raised the question [3, 11]. Lower bounds come from unit-distance graphs: finite sets of points with an edge between any two at distance exactly 1. If such a graph cannot be coloured with k colours, neither can the plane, and a compactness theorem of 1951 gives the converse, so the problem can be studied through finite graphs [2, 4].
From 1950 to 2018 the bounds were four and seven; Aubrey de Grey raised the lower bound to five in 2018 [3]. Apart from a claim made in October 2026 (see below), the bounds are still five and seven: a preprint of that month gives 5 ≤ χ ≤ 7, where χ is the chromatic number of the plane [14]. Settling the problem means finding the exact value. A better lower bound can take the form of a finite unit-distance graph that needs more colours [4]; a better upper bound needs a colouring of the whole plane with fewer than seven colours.
The answer might even depend on the axioms of set theory [2]. Saharon Shelah and Alexander Soifer gave related infinite graphs whose chromatic number is finite under the usual axioms with the axiom of choice but uncountable under other axioms, and Michael Payne describes his own unit-distance examples as "further evidence that the chromatic number of the plane might depend on set theory" [2]. Not to be confused with Hadwiger's conjecture, a different colouring problem.
What is known
Early bounds (1950–1961). Nelson noted the lower bound of four, which follows from small unit-distance graphs that need four colours; the smallest is the seven-vertex "Moser spindle", published in 1961 [3]. Hugo Hadwiger had discussed the seven-colouring of the hexagonal tiling in 1945, in another context, and the problem's name joins his contribution to Nelson's [3].
Colourings with restrictions (1973–2025). If each colour class must be a measurable set, so that its area is defined, Kenneth Falconer proved in 1981 that at least five colours are needed, more than 35 years before the same bound was known for arbitrary colourings [1, 14]. For colourings by regions with well-behaved boundaries ("maps"), results from 1973 and 1981 show that at least six colours are needed; in a 2025 preprint, Georgy Sokolov and Vsevolod Voronov show that at least seven are needed when the regions are polygons, matching the hexagonal colouring [9].
Five colours are needed (2018–2020). In April 2018 de Grey published unit-distance graphs that cannot be coloured with four colours, the smallest with 1,581 vertices [3]. Part of his proof was a computer search written in Mathematica, and others confirmed the result with standard SAT solvers, programs that decide whether logical formulas can be satisfied [3]. Polymath16, an open online collaboration launched in April 2018 on Dustin Mixon's blog at Terence Tao's suggestion, set out to find smaller examples, to reduce the reliance on computers and to look for a unit-distance graph that needs six colours [4]. Marijn Heule used SAT solvers and proof minimisation to find 553-vertex examples whose correctness "can be mechanically validated in a second" [5]. Geoffrey Exoo and Dan Ismailescu gave an alternative proof [6], and by 2020 Jaan Parts had a 509-vertex example [8] and a proof that "can be verified manually without the help of the computer" [7].
Fractional colouring (2023–2026). A fractional colouring gives weights to sets of points with no two at distance 1, adding up to at least 1 at every point; the fractional chromatic number is a lower bound for χ [10]. Máté Matolcsi, Imre Ruzsa, Dániel Varga and Pál Zsámboki proved that it is at least 4, and in a June 2026 preprint Ákos Dúcz and Varga show that it is strictly larger than 4, which gives another proof that χ ≥ 5 [10]. The authors report using ChatGPT and Codex for code and editing, and state that the mathematical results were "conceived, verified, and validated by the authors" [10].
Measurable and arbitrary colourings (1984–2026). László Székely conjectured in 1984 that the measurable and ordinary chromatic numbers of Euclidean spaces can differ [14]. In an October 2026 preprint, James Davies proves that they coincide in four or more dimensions, hopes to extend the method to the plane, and conjectures that χ = 6; he reports that ChatGPT 5.6 Sol completed the proof of his main theorem [14].
Recent claims. On 6 October 2026 OpenAI released "The Euclidean plane is not five-colorable", dated 23 September 2026, as family 158 of its openai/math repository of manuscripts "produced by an internal OpenAI model" [11]. It claims that every colouring of the plane with five colours has two points at distance 1 with the same colour, with no regularity assumption on the colour classes, so that χ would be 6 or 7 [11]. The repository says its collection "includes results at different stages of verification". A Lean formalisation released with the manuscript is described as proving that five colours do not suffice and seven do, the formal proofs' review status is listed as "unchecked", and no revision or withdrawal was recorded by 14 October [11]. Gil Kalai wrote on his blog: "The new manuscript raises the lower bound to six, leaving six and seven as the two possible answers." He added that the collection's "proofs will need to be checked and digested by the mathematical community" [12]. Jonathan Davidson's preprint of 7 October uses the claimed bound, notes that the manuscript obtains a finite graph that is not five-colourable "through compactness" and asks whether an explicit one can be extracted [13]; Davies wrote that he posted his preprint "slightly earlier than we would have liked" because of the release [14].
Main approaches
Finite unit-distance graphs. Build a finite graph that cannot be coloured with k colours, which proves χ > k [4]. Strongest evidence: the five-colour proofs, now with 509-vertex examples and a hand-checkable proof [7, 8]. Main difficulty: no unit-distance graph that needs six colours has been exhibited [13, 14]; even the claimed five-colour proof yields one only by compactness [13].
Measure and analysis. Prove bounds for measurable colourings, where powerful analytic methods apply, then transfer them to arbitrary colourings [14]. Strongest evidence: Falconer's bound [1] and Davies's transfer in four or more dimensions [14]; the 2026 claim follows this route in the plane [11]. Main difficulty: measurable and arbitrary colourings can behave differently, as Payne's examples show [2], and Davies's transfer does not yet reach dimensions two or three [14].
Colourings by regions. Assume the colour classes are regions with tame boundaries [9]. Strongest evidence: polygonal colourings need seven colours [9]. Main difficulty: the results hold only under these conditions on the regions, which an arbitrary colouring need not satisfy [9].
Fractional colouring. Bound the fractional chromatic number, a linear-programming relaxation [10]. Strongest evidence: the bound above 4, which reproves χ ≥ 5 [10]. Main difficulty: a known construction keeps the fractional chromatic number below 4.36, so this route alone cannot show that six colours are needed [10].
Open sub-questions
- A six-colour graph. Can an explicit finite unit-distance graph that cannot be coloured with five colours be found? Davidson asks whether one can be extracted from the claimed proof [13]; de Grey suggested concise descriptions of five-colour graphs as a route [3].
- The smallest five-colour graph. How few vertices can a unit-distance graph that needs five colours have? The smallest reported in 2020 has 509 [8].
- Measurable equals arbitrary in the plane? Does Davies's theorem that measurable and ordinary chromatic numbers coincide extend from four or more dimensions to dimensions two and three [14]?
- Maps. Do all map-type colourings, whose regions are bounded by curves, need seven colours? Six are known to be needed, and seven for polygons and under extra conditions on the boundaries [9].
- Fractional value. What is the fractional chromatic number of the plane? It lies above 4 and below 4.36 [10].
Work on this in Papex
If you have a testable answer to one of the sub-questions above, you can draft it as a private hypothesis in Papex, or prepare the draft from Claude or ChatGPT with the Papex connector. You review the exact version, sign it and decide whether to publish it; a public record that names this problem is listed on this page. A Papex record shows who signed which version and when. It is not peer review and does not mean the hypothesis is correct.
Key references
- Falconer, K. J. (1981). The realization of distances in measurable subsets covering R^n. Journal of Combinatorial Theory, Series A 31(2), 184–189. 10.1016/0097-3165(81)90014-5 · Checked 14 Oct 2026
- Payne, M. S. (2009). Unit distance graphs with ambiguous chromatic number. The Electronic Journal of Combinatorics 16(1), N31. 10.37236/269 · Checked 14 Oct 2026
- de Grey, A. D. N. J. (2018). The chromatic number of the plane is at least 5. arXiv:1804.02385v3 (v1 8 April, v3 30 May 2018; a journal version appeared in Geombinatorics 28(1), as cited in reference 14). Source · Checked 14 Oct 2026
- Mixon, D. G. (2018, 14 April). Polymath16, first thread: simplifying de Grey's graph. Short, Fat Matrices (blog). Source · Checked 14 Oct 2026
- Heule, M. J. H. (2018). Computing small unit-distance graphs with chromatic number 5. arXiv:1805.12181v1 (the arXiv comment gives Geombinatorics XXVIII(1), July 2018). Source · Checked 14 Oct 2026
- Exoo, G. & Ismailescu, D. (2020). The chromatic number of the plane is at least 5: a new proof. Discrete & Computational Geometry 64(1), 216–226 (published online 2019). 10.1007/s00454-019-00058-1 · Checked 14 Oct 2026
- Parts, J. (2020). The chromatic number of the plane is at least 5 — a human-verifiable proof. Geombinatorics 30(2), 77–102 (journal reference from the arXiv record). Source · Checked 14 Oct 2026
- Parts, J. (2020). Graph minimization, focusing on the example of 5-chromatic unit-distance graphs in the plane. Geombinatorics 29(4), 137–166 (journal reference from the arXiv record). Source · Checked 14 Oct 2026
- Sokolov, G. & Voronov, V. (2025). On the chromatic number of the plane for map-type colorings. arXiv:2502.01958v1 (preprint, not peer reviewed; 4 February 2025). Source · Checked 14 Oct 2026
- Dúcz, Á. & Varga, D. (2026). A unit-distance graph in the plane with independence ratio below 1/4. arXiv:2606.28157v1 (preprint, not peer reviewed; 26 June 2026). Source · Checked 14 Oct 2026
- OpenAI (2026). The Euclidean plane is not five-colorable. Manuscript dated 23 September 2026, released 6 October 2026 in the openai/math repository, family 158 ("The Euclidean plane cannot be colored with five colors"). Source · Checked 14 Oct 2026
- Kalai, G. (2026, 7 October). Updates: Sharing AI progress on mathematics (amazing!); and my lecture plans. Combinatorics and more (blog). Source · Checked 14 Oct 2026
- Davidson, J. (2026). Coloring monomial Cayley graphs: the one-parameter case. arXiv:2610.09474v1 (preprint, not peer reviewed; 7 October 2026). Source · Checked 14 Oct 2026
- Davies, J. (2026). Measurable obstructions for unmeasurable colourings. arXiv:2610.12301v1 (preprint, not peer reviewed; 8 October 2026). Source · Checked 14 Oct 2026
Source
Open, as listed by Wikipedia · Unsolved problems in mathematics. Checked 08 Oct 2026.
The status is the source’s. Papex does not decide whether a problem is solved.
Records on this problem
No public record addresses this problem yet.