The Euclidean plane cannot be colored with five colors
OpenAI groups related papers into a “family”. OpenAI’s catalogue describes this one:
Proves that every five-coloring of the Euclidean plane has a monochromatic pair at distance one, with no restriction on the color classes. This advances the Hadwiger–Nelson problem: together with the classical seven-coloring, only six and seven remain possible chromatic numbers of the plane. (OpenAI’s Lean note)
Lean is a language for mathematical statements and proofs that a computer can verify. The assessments below ask whether those statements express the result OpenAI describes here.
Both independent assessments find that the Lean statements express or imply the whole result described above.Read the assessments
Possible match to OpenAI’s description, selected from the papers’ main statements because it shares the most wording. No review confirming the selection is recorded.
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.
Two Lean statements in this family
Choose one to see it beside the paper theorem it is paired with.
For a configured theorem, the Comparator program tests whether OpenAI’s separate proof proves the exact Lean statement using only the allowed axioms. Some statement files instead configure definitions for comparison by name and type. Acceptance does not establish that a formal statement means the same thing as the paper’s theorem.
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
Comparator compares one definition by its name and type only: ProperColoring.
This file states the theorem with sorry, a placeholder, in place of its proof. OpenAI supplies a separate proof file. Comparator tests whether that proof proves the statement here.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling. Who ran the proof-verification program
cert-machine records it as “CERTIFIED”.
MathVet records it as “comparator-sandboxed-pass”.
Neal McBurnett, openai-math-lean-tooling records it as “accepted”.
Independent comparisons and proof-verification reports
Does the Lean express the advertised result?
MathVet and cert-machine agree on how much of the advertised result the Lean statements express.
MathVet and Carlos Toledo’s cert-machine independently assessed whether this family’s Lean statements express the whole result OpenAI describes in its catalogue. These are assessments of the family as a whole, not of each paper theorem separately.
MathVet finds that the Lean statements express or imply the whole advertised result (their term: “full”).
Their note:no_proper_five_coloring : ¬ ∃ coloring : ℂ → Fin 5, ∀ p q, ‖p - q‖ = 1 → coloring p ≠ coloring q is the headline for arbitrary colorings (no measurability or color-class hypothesis), and properColoring_seven gives the classical seven-coloring of EuclideanSpace ℝ (Fin 2) (so only 6 or 7 remain). The two statements use different plane models (ℂ with its norm vs EuclideanSpace ℝ (Fin 2), namespace Problem160), both genuinely the Euclidean plane; no lemma identifies them, which does not matter for either claim.
“full”, in their words: The challenge statements imply the headline claim after unpacking definitions or one routine step.
Their method: An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
The Hadwiger–Nelson problem asks for the fewest colors needed to color the plane so that points at distance one have different colors. 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; the upper bound includes every boundary point of the coloring regions.
AI-drafted comparisons, with no recorded human review
No proper five-coloringEuclideanFiveColor
Unreviewed AI draft: states a paper’s theorem as the paper does. States the main theorem that the plane has no proper five-colouring, with arbitrary colour classes. The one Comparator hole, the definition of a proper colouring, has the same body in the library up to the names of bound variables.
Proper seven-coloringPlaneColoring
Unreviewed AI draft: states part of a paper’s theorem. States the classical upper bound χ(R²) ≤ 7, the upper half of the main theorem’s displayed consequence 6 ≤ χ(R²) ≤ 7; the lower half is EuclideanFiveColor.
Who ran the proof-verification program?
These groups report running Comparator with the release’s Lean statement files. For a configured theorem, it verifies OpenAI’s separate proof against the exact statement; some files instead configure definitions for comparison by name and type. Each row is the named group’s report. Atlas has not repeated the runs.
These reports do not list the software versions, proof-verification programs, axioms, time or memory in separate fields. Any such details in a report’s prose are reproduced below.
No proper five-coloringEuclideanFiveColor
Two reports, all at the release’s recorded version.
Reported by
Their word
Their account
Date
Original report
cert-machine
“CERTIFIED”
Re-run through Comparator with the independent nanoda kernel switched on: Lean’s kernel and nanoda both accept OpenAI’s solution.
Other people’s accounts of running proof-verification software, with links to their reports.
Jack McCarthy, Re-running Comparator with the definition holes pinned, 9 October 2026. Source
With the definition holes pinned so the solver’s definitions must match the challenge, Comparator reports the solution is okay for this challenge, so the hole was not being abused by OpenAI’s own solution.
Jack McCarthy, OpenAI math: Comparator fixes (mirror of openai/math at fd4aeeb), 9 October 2026. Source
With all 1 definition hole removed from the configuration, so that Comparator compares the definition bodies too, the release’s solution still passes; run with the Lean kernel only, on macOS without Comparator’s sandbox.
From github.com/yforster/own-your-specs, 9 October 2026. Source
Minimal reproduction that a definition listed in definition_names can be freely overwritten without Comparator noticing.
Ben Knill, BenKnill/openai-math-hol-cards: HOL Light proof cards for eleven families, 8 October 2026. Source
Strict Comparator re-check with the definition holes removed, so hole bodies are compared too, accepted the solution with the three standard axioms. Its one hole, ProperColoring, matched, and a control changing the statement to Fin 6 was rejected. Run at adc7f124; the challenge file is unchanged at fd4aeeb2.
Alex Meiburg, Several of the comparator challenges in the OpenAI release are broken and hackable, 8 October 2026. Source
Comparator accepted a proof of the five-colouring challenge in which the colouring predicate was redefined to False, so the challenge file does not pin the statement.
GasStationManager, GasStationManager/SafeVerifyAgent: audit log including a corpus look and a read-through of family 107, 7 October 2026. Source
PlaneColoring challenge statement read against the paper (5 of 5 clauses paired) as part of the corpus look.
Ben Knill, BenKnill/openai-math-hol-cards: HOL Light proof cards for eleven families, 7 October 2026. Source
Exact-arithmetic HOL Light card for the Moser spindle used in the plane-colouring result.
Robert Joseph George, Do the Lean statements in openai/math match their papers?, 7 October 2026. Source
The review reports that Comparator accepted OpenAI’s solution for this challenge, run end to end on Lean 4.34.1 with the default kernel and only the three standard axioms.
Other proofs and exact calculations
These reports examine claims in the papers using HOL Light, a different proof assistant and exact calculations for finite claims, independently of the release’s Lean proofs. Read each report for the exact claim it covers.
The seven placed Moser vertices lie in the three-label region, the 11 edges have length exactly 1, and no proper 3-labelling exists; exact arithmetic in ℚ(√3,√11)
HOL Light card 158
Reported by
Ben Knill, openai-math-hol-cards
Method
Proof of a selected step in HOL Light
Their verdict
“PASS” The report records a proof of a supporting fact.
Lemma 8.9 of The Euclidean plane is not five-colorable, 23 September 2026
Reported by
cert-machine
Method
Exact computation
Their verdict
“CERTIFIED” Exact code written independently from the paper confirms that the published object has the claimed property.
What it covers
“a finite component: Lemma angular-certificate (all seven placed Moser-spindle vertices strictly in the region 0<l<4, P<P'), the eleven unit edges and non-3-colourability, and every number of the paper’s rational verification. NOT the headline (the plane is not 5-colourable), which rests on the transfer theorem and the measurable/angular theory.”
Reports of errors and corrections from outside readers, as they state them. The atlas has not judged them.
Jack McCarthy, OpenAI math: Comparator fixes (mirror of openai/math at fd4aeeb), 9 October 2026. Source
Per the mirror’s commit message, the EuclideanFiveColor challenge accepted a solution that redefined ProperColoring as False because the name sat in definition_names.
Alex Meiburg, Several of the comparator challenges in the OpenAI release are broken and hackable, 8 October 2026. Source
A reader replaced the proper-colouring definition by false and Comparator accepted a trivial proof, because that definition is listed as a hole.
Raemon, Are OpenAI’s math results “creative” in an important way?, 7 October 2026. Source
JoshuaZ: weakly measurable colourings are not new (Bachoc, DeCorte, de Oliveira Filho and Vallentin 2014 and others should be cited); the key new idea is the theorem that proper colourings correspond to weakly measurable ones.
Lean community, OpenAI releases solutions to hundreds of problems (117 messages, 6-10 Oct 2026), 6 October 2026. Source
Meiburg shows the five-colour challenge accepts a trivial proof when the colouring predicate is redefined; the same hole affects Brenier (374), LogspaceEquality (103), KServer (110), Naimark (297), OccupiedOverlap and SpinAngle (238) and Rokhlin (145).
Explanations by others
Explanations of this family written elsewhere, by the people named. Each is their own reading of the mathematics.
Gil Kalai, Updates: Sharing AI progress on mathematics (amazing!); and my lecture plans, 7 October 2026. Source
Records the release’s claim that five colours do not suffice for the plane, leaving six or seven.
Dmitry Rybin, Posts on the plane-colouring (chromatic number at least 6) proof, 7 October 2026. Source
Equivalence of proper K-colourings and weakly measurable K-colourings is the key step, followed by amenable-group and ergodic-theoretic machinery.
Missing or incomplete source records
The program that collects Atlas’s source records, Statement Map, could not obtain or interpret some source material. These notes describe those limits; they do not identify mathematical errors.
PlaneColoring: Tracked source lean/OAI/Geometry/PlaneColoring/Main.lean unavailable: bytes were not captured at fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb
What these papers cite in the release, and what cites them
These links come from the papers’ bibliographies. A citation records that one paper cites another; how each cited result is used has not been examined here.
Papers elsewhere in the release that this family’s papers cite
This family’s papers cite no paper elsewhere in the release.
Papers elsewhere in the release that cite this family’s papers
No paper elsewhere in the release cites this family’s papers.
Follow-up work by others
Sergi Galán, decalion89/chromatic-number-of-the-plane: Hadwiger-Nelson over number fields, rebuilding OpenAI’s formal proof, 9 October 2026. Source
The points constructible with ruler and compass cannot be 5-coloured, checked in Lean (and so any Euclidean field).
Hexagon, Hexagon: a repository for research in the mathematical sciences and theoretical computer science, 9 October 2026. Source
hexagon:2610.00171v1 (Ákos Dúcz) shows planar measurable independence density equals the finite independence-ratio infimum using the spectral rigidity theorem in OpenAI’s no-five-colouring proof.
Jack McCarthy, OpenAI math: Comparator fixes (mirror of openai/math at fd4aeeb), 9 October 2026. Source
Five pull requests (#1 to #7) in the fork remove the overwritable definition lists and fix OccupiedOverlap, SpinAngle, ElementaryPositivity and DefocusingNLS; all ten affected challenges pass Comparator afterwards.
Jonathan Davidson, Coloring Monomial Cayley Graphs: The One-Parameter Case, 7 October 2026. Source
Davidson records that OpenAI’s no-5-colouring theorem forces the monomial Cayley graph parameter M(r) to be at least 6 for some finite r, and poses finding the least such r as a concrete problem.
References outside the release
Each paper’s outside references are listed with it on its reading page, where each citation is placed. Every outside work cited in the release: References outside the release
Explain a result, compare statements or propose a correction
Atlas has no contributed explanation for this family yet. You can offer one with a GitHub account. You receive named credit and disclose any AI assistance.
Each button opens a GitHub form with this page and its source version filled in. Opening the form does not reserve the work.
Commentary on this family by others, dated and credited. It is commentary, not a finding.
An unsigned public tier list, the OpenAI Math Tier List, classes it as a proof and rates its significance, if it holds up, as “Career-defining publication”. The page says that nothing on it is verified.
Moritz Firsching, anxkhn, Paul Lezeau, Formal Conjectures: mark problems solved in the OpenAI math release and link formal proofs, 11 October 2026. Source
A Formal Conjectures maintainer, after source inspection, links the five-colour result for the plane to the chromatic number of the plane problem, leaving the full value open.
OfficeChai (byline not recorded), OpenAI Has Also Included Proofs For 23 Erdos Problems In Its Latest Math Proof Drop, 9 October 2026. Source
Erdos #508: any 5-colouring of the plane has two same-coloured points at distance one, so the chromatic number of the plane would be 6 or 7.
Thomas Bloom, Erdős problems in the OpenAI proofs, 8 October 2026. Source
Bloom lists Erdős 508, the five-colour impossibility for the plane, marks it formalised but gives no link, and notes it implies the chromatic number is 6 or 7.
Leah Crane, The most interesting mathematical discoveries in OpenAI’s 722 new papers, 8 October 2026. Source
Notes new work that seems to eliminate five colours for colouring the plane, leaving six or seven.
Dmitry Rybin, Posts on the plane-colouring (chromatic number at least 6) proof, 7 October 2026. Source
Zelinsky (Bluesky, 6 Oct): the method does not look like a direction the prior literature used.
Questions awaiting review
Each item identifies a statement, definition or report that needs further review. Its link opens a GitHub form with the source version already recorded.
Read the Lean statement against the paper
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
An AI agent drafted an assessment of which part of the paper this Lean statement expresses. No named human review is recorded.Open the form
Read the definitions the solution supplies
OpenAI’s proof file supplies some definitions. Atlas records no comparison confirming that they mean the same objects as the paper’s definitions.ProperColoringOpen the form
Identify the theorem the catalogue describes
Family 158The theorem shown was selected from shared wording with OpenAI’s description. Atlas records no review confirming that it is the theorem the description means.Open the form
Compare the proposed paper and Lean matches
Family 158Atlas records no review of whether each linked Lean statement and paper theorem mean the same thing.Open the form
Investigate a calculation that did not decide the claim
Family 158An independent calculation did not decide the claim, or needs data absent from its source.Open the form
Why this passage is shown
Theorem 1.1
In The Euclidean plane is not five-colorable, 23 September 2026
How it was found
Its words were compared with the words of OpenAI’s catalogue description.
Words they share
classes, color, coloring, euclidean, five, plane
Review
Atlas records no review confirming that this is the theorem OpenAI’s description refers to.
The challenge statements imply the headline claim after unpacking definitions or one routine step.
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge. Its protocol describes a planned error-rate study; this import does not establish that the study has been completed.
The challenge statements state the headline as OpenAI wrote it.
Their method
Every Comparator challenge re-run on Linux with nanoda switched on, decided by a preregistered rule; every family’s challenge statements read against OpenAI’s headline, clause by clause. Decider: Comparator (leanprover/comparator d03acab1 = tag v4.34.0, built with the release’s toolchain v4.34.1), lean4export 076e8e57, landrun 811cfff5, nanoda_lib 3a240721 — on GitHub’s Linux runners…
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
Re-run through Comparator in a sandboxed virtual machine: accepted.
Date
8 October 2026
Version
at the release’s recorded version
Their method
An independent, model-assisted, pre-referee reading of each family’s challenge statements against its headline claim under a published rubric (PROTOCOL.md), with its own Comparator runs per challenge.
Re-run through Comparator with Lean’s kernel: accepted (the check took 54 s; peak memory 6.1 GiB).
Date
10 October 2026
Version
at the release’s recorded version
Their method
Each challenge’s solution is built and checked by Comparator at the pinned release, on Lean leanprover/lean4:v4.34.1, recording the verdict, the check time and the peak memory.
The seven placed Moser vertices lie in the three-label region, the 11 edges have length exactly 1, and no proper 3-labelling exists; exact arithmetic in ℚ(√3,√11)
Proofs of selected steps in HOL Light, Ben Knill, openai-math-hol-cards
Their verdict
“PASS”
Claim tested or proved
The seven placed Moser vertices lie in the three-label region, the 11 edges have length exactly 1, and no proper 3-labelling exists; exact arithmetic in ℚ(√3,√11)
Lemma 8.9 of The Euclidean plane is not five-colorable, 23 September 2026
Exact calculations for finite claims, cert-machine
Their verdict
“CERTIFIED”
Claim tested or proved
Exact code written independently from the paper confirms that the published object has the claimed property.
What it covers
“a finite component: Lemma angular-certificate (all seven placed Moser-spindle vertices strictly in the region 0<l<4, P<P'), the eleven unit edges and non-3-colourability, and every number of the paper’s rational verification. NOT the headline (the plane is not 5-colourable), which rests on the transfer theorem and the measurable/angular theory.”
Exact calculations for finite claims, cert-machine
Their verdict
“NEEDS DATA”
Claim tested or proved
Cannot be decided from the release: the specific object the argument relies on is not published.
Detail
NOT PUBLISHED. build/sections/introduction.tex lines 31-36 ('an unrestricted lower bound can also be established without first displaying a finite graph witnessing it') and lines 309-313 ('Theorem~\ref{thm:main} and graph compactness ... give a finite unit-distance graph H that is not five-colorable'). The proof goes through weak measurable colorings (build/sections/transfer.tex) and spectral/ergodic arguments.
three independent groups report that Comparator accepted runs for this Lean statement file: cert-machine; MathVet; Neal McBurnett, openai-math-lean-tooling.