---
id: "2026-10-06-openai-plane-not-five-colourable-hadwiger-nelson-claim"
url: "https://postcutoff.com/e/2026-10-06-openai-plane-not-five-colourable-hadwiger-nelson-claim/"
as_of: "2026-10-30T13:42:00+01:00"
date: "2026-10-06"
date_precision: day
category: science
importance: 5
confidence: medium
status: [Awaiting review]
verification: Peer-reviewed
sources: 10
editor: human editor
human_review: null
version: "2026-10-29"
---

As of: 2026-10-30 13:42 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-10-06-openai-plane-not-five-colourable-hadwiger-nelson-claim/

# Chromatic number of the plane is 6 or 7, OpenAI claims (Lean)

Full title: OpenAI's math release claims the plane cannot be 5-coloured without two points at distance one sharing a colour, so its chromatic number is 6 or 7 (Hadwiger–Nelson problem); Lean-formalized, but no finite unit-distance graph is exhibited

"The Euclidean plane is not five-colorable" (OpenAI, 23 Sept 2026, 62 pages; family 158 of the 6 Oct release): "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." The argument transfers any proper colouring with finitely many colours to a "weak measurable" one (readers point to its use of amenable groups, Pontryagin duality and ergodic theory), then gives a geometric obstruction to five colours. Lean challenges EuclideanFiveColor (no proper 5-colouring) and PlaneColoring (a proper 7-colouring) were accepted in the oai-math-revised comparator run; an audit that compared definition bodies also certified the five-colour statement. Koshelev, Kupavskii and Voronov already used the transfer theorem in three dimensions (arXiv 2610.18907).

## Key facts
- Manuscript (abstract, verbatim): '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.' 62 pages, dated 23 Sept 2026. Theorem 1.1 is proved in ZFC; 'The remaining alternatives six and seven are unresolved'
- Structure (paper): 'a transfer from unrestricted proper colorings to a measurable condition, and a geometric obstruction to five labels under that condition. The transfer holds for every finite number of colors.' Because of the de Bruijn–Erdős compactness theorem, 'an unrestricted lower bound can also be established without first displaying a finite graph witnessing it'; the final step reuses the Moser spindle
- Before: Nelson (1950) and Isbell gave the bounds 4 and 7; Aubrey de Grey's 2018 finite unit-distance graph (1,581 vertices after correction) raised the lower bound to 5, later shrunk by Heule (553 vertices) and Parts (509); for measurable colour classes Falconer had proved at least 5 colours (as recounted in the paper)
- Lean (OpenAI scope note lean/docs/158.md): 'The formalized results prove that five colors do not suffice and that seven colors do suffice. The lower bound applies to arbitrary colorings, with no measurability or continuity assumption.' Both challenges 'accepted' in the oai-math-revised comparator run (25–26 Oct). Caveat recorded there: the EuclideanFiveColor configuration let the comparator check the definition ProperColoring by type only; OpenAI emptied that list on 26 Oct. Carlos Toledo's audit had flagged that this one definition 'carries the whole conclusion', ran a strict body-by-body comparison, and later lists EuclideanFiveColor as certified after the change
- No explicit witness: Toledo's audit notes that 'the finite non-5-colorable unit-distance graph is obtained by compactness and never displayed', while certifying the paper's finite Moser-spindle certificate in exact arithmetic
- Reactions: Joshua Zelinsky (Bluesky, 6 Oct): 'it doesn't look like the method is a direction that the prior lit used to my knowledge. This is far beyond merely building on existing methods'. Dmitry Rybin (X, 7 Oct, about 261k views): 'I was trying to read the OpenAI proof that chromatic number of a plane is >= 6. But it is totally unbelievable alien math?', adding that the model found that any K-colouring is equivalent to a 'weakly measurable' one. Gabriel Gaster (X, 9 Oct) pointed to its mix of 'Pontryagin duality, ergodic theory, and amenable groups'. Gil Kalai (7 Oct): 'The new manuscript raises the lower bound to six'. Thomas Bloom lists it under Erdős problem #508, noting 'This proof has been formalised'
- Follow-ups: Koshelev, Kupavskii and Voronov (arXiv 2610.18907, 11 Oct): 'Using the planar character-law rigidity theorem of OpenAI, we prove that every finite proper coloring of R³ can be replaced by a proper Lebesgue-measurable coloring with the same number of colors', so the ordinary and measurable chromatic numbers of R³ are equal; they used ChatGPT 6 Astra to extract the main ideas of OpenAI's preprint. Henry Bass's GitHub repository extends the transfer theorem to R^n with AI-assisted preprints and Lean

## What happened

The Hadwiger–Nelson problem asks how many colours are needed to colour the plane so that points at distance exactly one always get
different colours. Since 1950 the answer was known to lie between 4 and 7. In 2018 the amateur mathematician Aubrey de Grey raised the
lower bound to 5 with a finite graph of unit distances that cannot be 4-coloured.

OpenAI's 6 Oct release claims 6, so that only 6 and 7 remain. Instead of a larger finite graph, the 62-page manuscript proves that any
proper colouring with finitely many colours can be replaced by one with a weak measurability property. It then shows that five colours
are impossible under that property. Compactness implies that a finite non-5-colourable unit-distance graph exists, but the paper does not
construct one. Both bounds are formalized in Lean. A comparator caveat about how one definition was checked was closed by an
independent audit and by OpenAI's 26 Oct configuration fix.

## Why it matters

The chromatic number of the plane is one of the best-known open problems in combinatorics, and this would be the first step since
2018. Readers note that the method is new rather than a heavier version of de Grey's approach, and other authors have already reused
it in three dimensions. The claim is formally checked, so the open questions are whether the formal definitions match the classical
problem and what the finite witness looks like.

## What is disputed or not yet verified

- Verification: Lean formalization accepted by an independent comparator run and certified by a stricter definition-body check after OpenAI's 26 Oct configuration fix; unrefereed manuscript; finite witness graph not exhibited

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 159 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 98 days after its cutoff
- Gemini 4 Argon (training cutoff March 2026): 189 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 128 days after its cutoff

## Sources

1. [OpenAI (PDF): The Euclidean plane is not five-colorable (23 Sept 2026)](https://github.com/openai/math/blob/main/preprints/The-Euclidean-plane-is-not-five-colorable-September-23-2026/paper.pdf) (github.com, paper)
2. [OpenAI Lean scope note for family 158](https://github.com/openai/math/blob/main/lean/docs/158.md) (github.com, code)
3. [oai-math-revised comparator results and LEAN_CHECKS (EuclideanFiveColor, PlaneColoring accepted; definition caveat)](https://github.com/mathcommunity/oai-math-revised/blob/main/docs/LEAN_CHECKS.md) (github.com, code)
4. [arXiv 2610.18907: Koshelev, Kupavskii & Voronov, Ordinary and measurable colorings of Euclidean three-space](https://arxiv.org/abs/2610.18907) (arxiv.org, paper)
5. [GitHub: outsidetext/euclidean-chromatic-transfer (Henry Bass, extensions to R^n)](https://github.com/outsidetext/euclidean-chromatic-transfer) (github.com, code)
6. [Carlos Toledo: OpenAI's math release, what it claims beyond what it checks (findings G7, G10)](https://carlostoledo.co/reports/openai-math.html) (carlostoledo.co, discussion)
7. [Dmitry Rybin on X: 'totally unbelievable alien math?' (7 Oct)](https://x.com/DmitryRybin1/status/2107852898617229724) (x.com, discussion)
8. [Joshua Zelinsky on Bluesky (6 Oct)](https://bsky.app/profile/joshuazelinsky.bsky.social/post/3mxak2f4ywk24) (bsky.app, discussion)
9. [Thomas Bloom: Erdős problems in the OpenAI proofs (problem #508)](https://www.erdosproblems.com/forum/thread/blog:10) (erdosproblems.com, discussion)
10. [Gil Kalai: Updates: Sharing AI progress on mathematics (amazing!) (7 Oct)](https://gilkalai.wordpress.com/2026/10/07/updates-sharing-ai-progress-on-mathematics-amazing-and-my-lecture-plans/) (gilkalai.wordpress.com, discussion)

## Changes

- 2026-10-29 (filed): Created (CONTENTS entry, PDF (62 pp), Lean scope note, comparator results and LEAN_CHECKS, Bloom, Kalai, posts on X and Bluesky fetched via fxtwitter and the public Bluesky API, Koshelev–Kupavskii–Voronov abstract)

## Related

- 2026-10-24: [oai-math-revised: mathematicians launch a community hub to revise OpenAI's AI-written math manuscripts (guest post on Tao's blog)](https://postcutoff.com/e/2026-10-24-oai-math-revised-community-hub/index.md)
- 2026-10-14: [Mid-October 2026: arXiv results with disclosed AI help](https://postcutoff.com/e/2026-10-14-ai-assisted-results-mid-october-2026/index.md)
- 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/index.md)
- 2026-10-06: [Hadwiger's conjecture disproved? (OpenAI, Lean)](https://postcutoff.com/e/2026-10-06-openai-hadwiger-conjecture-counterexample-claim/index.md)
- People: [Thomas Bloom](https://postcutoff.com/person/thomas-bloom/)
- Archived: 1 post, listed in https://postcutoff.com/e/2026-10-06-openai-plane-not-five-colourable-hadwiger-nelson-claim/index.json