Contributor workspace
Sign in to claim tasks, verify results and earn reputation. Browsing is open to everyone.
Sign inThe preprint claims that every colouring of the Euclidean plane with five colours has a monochromatic unit-distance pair, with no regularity assumption on the colour classes (in ZFC), so 6 ≤ χ(ℝ²) ≤ 7. The proof (i) transfers any proper k-colouring of the plane to a weak measurable k-colouring, a Lebesgue-measurable colouring whose monochromatic unit pairs have product measure zero, and back, for every k; and (ii) shows no weak measurable 5-colouring exists, via palettes of labels seen along unit directions, Fourier decay of the circle measure and a topological argument on disk maps, finishing with Moser-spindle constraints. No explicit finite non-5-colourable graph is given; one exists by de Bruijn–Erdős compactness. A Lean 4 proof of the unrestricted statement (OAI.EuclideanFiveColor.no_proper_five_coloring, colourings of ℂ) is public. It does not settle the problem: whether χ(ℝ²) is 6 or 7 remains open.
Unrefereed, AI-produced preprint (dated 23 Sep 2026, released in openai/math in October 2026). The Lean proof is public and uses only the standard axioms. Formal Conjectures marks Erdos508.HadwigerNelsonAtLeastSix solved with a link to it, and one independent third-party audit (13 Oct 2026) restated the theorem in a Mathlib-only file and accepted the proof with the Lean kernel, Comparator and the nanoda kernel. The audit also showed that OpenAI's published Comparator configuration would accept a fake proof, because it leaves ProperColoring as an unchecked definition hole; the real definition is correct. Not yet rebuilt by DARC, no expert assessment of the paper and no refereeing found as of 17 Oct 2026.
Verification broken into steps anyone can take. Pick an open one, do it, and submit what you found below. Matching how a check is settled earns +8; catching a failure earns +20.
Third-party audit (13 Oct 2026) at openai/math commit fd4aeeb: lake build with Mathlib v4.34.1, Comparator against a Mathlib-only challenge, and the independent nanoda kernel all accept no_proper_five_coloring; axioms are propext, Quot.sound and Classical.choice only; no sorry, native_decide or metaprogramming in the 78-file import closure.
The audited statement is ¬ ∃ c : ℂ → Fin 5, ∀ x y, ‖x - y‖ = 1 → c x ≠ c y, with c an arbitrary function; the audit transports it to EuclideanSpace ℝ (Fin 2) and adds controls (7 colours satisfiable, 2 colours ruled out) so it is not vacuous.
The Combinatorics committee has no members yet, so this claim can be machine-checked and verified by anyone but not committee-reviewed.
No verifications yet.
Sign in to verify.
Build the proof at the pinned openai/math commit, run Comparator with ProperColoring checked (not a definition hole), and prove the transport to Erdos508.HadwigerNelsonAtLeastSix (6 ≤ chromaticNumber of UnitDistancePlaneGraph) at the pinned Formal Conjectures commit.
Check Theorem 1.3 (proper k-colouring exists iff a weak measurable k-colouring exists, in ZFC), which carries the step from arbitrary colour classes to measurable ones; earlier work shows measurable and unrestricted colourings can differ for other graphs.
Check Theorem 1.4 (no weak measurable 5-colouring): the palette bound of at most two labels, the transition-graph and cycle-set analysis, and the final disk-map and Moser-spindle contradiction.
No journal submission or expert assessment of the paper found as of 17 Oct 2026.