#508: The plane is not five-colourable — χ(ℝ²) is 6 or 7 — OpenAI's 62-page proof: Lean kernel-replayed here (70 modules, standard axioms, the comparator's statement proved verbatim), seven hostile seats find no gap; if it holds, the first move on Hadwiger–Nelson's lower bound since de Grey, and χ equals the weak-measurable chromatic number of the plane

The problem (erdosproblems.com/508; Erdős 1961, 1975, 1981). What is the chromatic number χ of the plane — the fewest colours that colour ℝ² so that no two points at distance exactly 1 share one? The Hadwiger–Nelson problem (Nelson 1950). The page's bounds are 5 ≤ χ ≤ 7 — the hexagonal seven-colouring, and de Grey's 2018 finite unit-distance graph that is not four-colourable, which ended a sixty-eight-year stand at four (1,581 vertices, later cut to 553 by Heule and 509 by Parts, per the paper's introduction). The page also records the fractional bound ≥ 4 (Matolcsi–Ruzsa–Varga–Zsámboki) and Croft's upper bound 4.359, and says nothing of the measurable problem, where Falconer proved in 1981 that colour classes required to be Lebesgue measurable need at least five colours — thirty-seven years before anyone could say so without the measurability. Zero proof claims; one comment (BorisAlexeev, October 2025, noting that Erdős's 1975 "F(2) ≤ 6" was almost certainly a slip for 7); last edited 22 January 2026. The teorth database says open (last updated 31 August 2025).

The claim. OpenAI's 23 September 2026 preprint "The Euclidean plane is not five-colorable" (62 pages, family 158 of the 6 October release; on Bloom's 8 October list of 25 as "This proof has been formalised. The PDF is 62 pages long.", and marked "(partial)" on the FrontierMath Erdős list because the page asks for the exact value). Theorem 1.1: every colouring of the plane with five colours, with no regularity assumption whatever on the colour classes, has two points at distance one of the same colour; so 6 ≤ χ(ℝ²) ≤ 7. If this holds it is the first movement of the lower bound since de Grey, and it decides the problem up to one colour. The proof has two parts, and the first answers, in its weak form, a question open since Falconer. Theorem 1.3 (transfer): for every k, in ZFC, a proper k-colouring of ℝ² exists if and only if a weak measurable k-colouring exists — a Lebesgue-measurable c with ∑_i ∫_B(0,R) ∫_S¹ 1_Ai(x) 1_Ai(x+u) dσ(u) dx = 0 for every R, i.e. monochromatic unit pairs of product measure zero, exceptional pairs allowed. Theorem 1.4: no weak measurable five-colouring exists. The paper is explicit that the two notions cannot be identified for free: it cites Payne's example of the graph on ℝ² whose edges join points whose displacement is a unit vector with rational coordinates, which is two-colourable but needs at least five colours measurably — so the transfer must use something the rational directions lack.

The architecture runs in two halves that meet at Definition 1.2, and the first half is where the novelty sits. Transfer (§2–4). Let F be the real algebraic numbers, E = F(i) the countable algebraic plane, K = {u ∈ E : |u| = 1} the countable group of algebraic rotations — dense in the circle and divisible. Restrict the given five-colouring (any colouring at all) to E; the group E ⋊ K is amenable, so Følner averaging of a point mass on the compact space of proper labelings of E gives an invariant probability law µ on proper labelings (Proposition 4.2's first paragraph — a Følner sequence and a weakly convergent subsequence, a textbook construction; the axiom of choice enters elsewhere, through the invariant mean on F/ℤ of §2.2, and in the converse direction through its compactness step and de Bruijn–Erdős). Let f_i be the indicator that the origin has label i; properness says ⟨f_i, T_u f_i⟩ = 0 for every algebraic unit u. Lemma 4.1: the vectors on which the translation action is norm-continuous form L² of a factor, so projection onto them is a conditional expectation (it keeps 0 ≤ p_i ≤ 1 and ∑ p_i = 1), and on that factor the E-translations extend to a strongly continuous unitary action of all of ℝ². The remainder b_i = f_i − p_i has a K-invariant spectral measure on the dual group D of E_disc giving zero mass to the Borel subgroup C ≅ ℝ² of continuous characters — a wild law — and the paper's central new statement, Theorem 2.3 (rigidity), says every wild K-invariant probability on D is Haar measure, whose Fourier coefficients vanish at every nonzero point of E. So the remainder is orthogonal to all its nonzero algebraic translates, the cross terms vanish, and ⟨p_i, T_u p_i⟩ = 0 survives for algebraic u, hence by strong continuity and density for every unit direction, hence by unitarity for every pair (x, x+u). Jointly measurable versions of x ↦ T_xp_i, Tonelli, one sample ω, and "take the least label with positive field" give a weak measurable five-colouring. Theorem 2.3 itself is proved in §2–3 by the Furstenberg–Zimmer compact-extension method: along a compact tower of an ergodic K-system the difference of two conditionally independent characters stays wild (Lemma 2.7, relative singularity); its Fourier coefficient is nonnegative and radial; two identities among sums of algebraic unit directions (Lemma 3.3) give a difference inequality for that coefficient; a number-field general-position lemma (3.4) and an "addition under a cap" lemma (3.5) turn any positive value at one nonzero radius into a uniform positive lower bound on a whole interval of algebraic radii, which the vanishing line averages of Lemma 2.5 forbid.

Why this cannot be a free lunch is the first thing a reader checks, and the paper names the obstacle itself: Payne's rational-direction graph is two-colourable yet measurably needs five colours, so the same words cannot work for Q(i) in place of F(i). They don't, and one can see where without opening the proof: the rational analogue of Theorem 2.3 is false. Every rational point of the unit circle has a reduced denominator whose prime factors are all ≡ 1 (mod 4), so the ring the rational rotations generate is R = ℤ[1/p : p ≡ 1 (mod 4)][i], a proper subring of Q(i) (1/3 is not in it) with infinite index. Its annihilator in the dual of Q(i)_disc is an infinite closed subgroup H, invariant under rational rotations; Haar measure on H is a rotation-invariant probability, gives the continuous characters mass zero (a continuous character trivial on the dense set R is trivial), and is not Haar on the whole dual. For E = F(i) no such subgroup exists: every real algebraic x with |x| ≤ 2 is 2cos θ for an algebraic unit e^iθ, so the ring generated by K is all of E and a K-invariant subgroup is an ideal of the field — zero or everything. That is where square roots in F do their work — they make the ring generated by K all of E; density of the directions is not it (the rational directions are dense too), nor is divisibility of K on its own — and it is also why the theorem is a statement about the plane and not about a lucky countable graph.

Obstruction (§5–8), for five labels and a weak measurable colouring. At a fixed centre x, weak-* limits of the typical circle samples e ↦ (1_Ai(y + re))_i as y → x and r → 1 define traces; the palette at (x, e) collects the labels with positive weight at e in some trace. Smooth transport of two unit directions gives exclusions between palettes (Lemma 5.2, Corollary 5.4's sixty-degree exclusion), a separation constant for centres whose palettes meet a fixed pair (Lemma 5.5), and Proposition 5.6: at every centre almost every palette has at most two labels. §6 records label transitions in a finite graph at each centre and proves (Theorem 6.5) that the centres whose graph contains a cycle form a closed locally finite set — the estimates run on the decay of the Fourier transform of circle measure, with no assumption of finite perimeter or smooth boundaries. §7 smooths the indicators by disk averages, thresholds and renormalizes, obtaining outside disks of vanishing total radius a continuous map into the complete graph K₅ as a one-complex (at most two positive coordinates), fills the holes continuously in the forest regions, and uses a planar cover obstruction (Lemma 7.5: a closed square of side ten has no relatively open cover of mesh at most two and multiplicity at most two — the Lean's PlanarCover.compact_open_cover_impossible states it for any compact set containing the open disk of radius 5, by a winding argument where the paper uses Brouwer) to force a nontrivial loop around one cyclic-centre disk; a simple cycle in its reduced edge path, a connected component of each edge midpoint's preimage crossing the annulus, and limits give Proposition 7.1: compact connected sets K_j with a common point x, forming a cycle of labels, with both labels of K_j absent almost everywhere from Δ(K_j) = {z : min_q∈Kj |z − q| < 1 < max_q∈Kj |z − q|} (the interface mechanism of Sokolov–Voronov, here derived from measure rather than assumed from polygons). §8 kills the three possible cycle lengths: five because six equal steps around a rotation orbit cannot close modulo five (Proposition 8.2), four by the parity of the six-position angular words of Lemma 8.3 together with the arc geometry of Lemma 8.4 (Proposition 8.5), three by six alternating sectors that leave an open region using only the three cycle labels almost everywhere (Lemma 8.8), into which a rational placement puts all seven vertices of the Moser spindle (Lemma 8.9, Proposition 8.10) — the spindle has no proper three-colouring, and typical points — density-one points of their own class, which Lemma 4.3 shows contain no unit pair, the one piece of §4 that Theorem 1.4 itself needs — are properly coloured.

The Lean, and what the kernel certifies. This one is catalogued: lean/formalization.yaml lists OAI.EuclideanFiveColor.no_proper_five_coloring in OAI/Geometry/PlaneColoring/Five.lean against the comparator config ComparatorChallenges/EuclideanFiveColor.json (challenge EuclideanFiveColor.lean, permitted axioms propext, Quot.sound, Classical.choice), and lean/docs/158.md says the lower bound "applies to arbitrary colorings, with no measurability or continuity assumption". The comparator is nine lines: a colouring is a function ℂ → Fin 5, ProperColoring 5 c says ‖x − y‖ = 1 → c x ≠ c y for all x, y, and the theorem is ¬ ∃ c, ProperColoring 5 c — the problem page's lower-bound statement with nothing added and nothing weakened (‖·‖ on ℂ is the Euclidean modulus, Fin 5 is five colours, the colouring is an arbitrary function). The proof's import closure from Five.lean is 70 modules and 30,336 lines — 37 under PlaneColoring/, 19 under OAI/Analysis/PlaneSpectrum/ (the character group, invariant means, the spectral representation, ergodicity) and 14 under OAI/MeasureTheory/CompactFactors/ (the Furstenberg–Zimmer tower) — importing nothing but Mathlib (pinned at d13f23b7, the v4.34.1 tag), with no sorry, admit, axiom, native_decide, implemented_by, @[extern], unsafe or set_option anywhere in the closure by grep (the decide calls are kernel-evaluated finite case splits on Fin 5 and Fin 6 data, plus a few numeral side conditions). Five.lean follows the paper's two halves exactly: proper_to_borel_weak (BorelTransfer.lean, 451 lines, and the chain behind it: the label model and the invariant law in PlaneSpectrum/Representations, the projection onto continuous vectors, residual_fourier in PlaneSpectrum/Ergodicity, the orbit extension to all of ℂ, the measurable field, the sampled colouring) turns any proper k-colouring into a Measurable WeakColoring k — AEMeasurable, and c x ≠ c(x + e^it) for (volume ⊗ Haar)-almost every (x, t) on ℂ × AddCircle(2π), which is Definition 1.2 with the angular Haar probability in place of σ and the product null set in place of the vanishing integrals; no_measurable_weak_five_coloring then runs §5–8 (FullApprox, graph_map_large_positive, PlanarCover.compact_open_cover_impossible, FullApprox.no_large_positive_sequence). Unlike the unit-distance proof of #90 this closure IS catalogued, so OpenAI's own release machinery vouched for it; and now so has ours. We cloned the repository sparse at its current revision (1581d4c of 12 October; the build was launched at fd4aeeb, the 8 October merge, and every closure file is byte-identical between the two — the sources seat finds these files have exactly one commit, adc7f124 of 6 October), fetched Mathlib's cache at the pinned d13f23b7, and compiled the 70 modules one at a time, lake-free, with a single thread at nice 19 and a memory gate that never evicts a live solver: all 70 built in 1,263 s with 0 errors. Under --trust=0, #print axioms reported exactly [propext, Classical.choice, Quot.sound] for no_proper_five_coloring, for no_measurable_weak_five_coloring, for proper_to_borel_weak and for proper_to_weak — #print axioms is transitive, so the first line already covers everything the theorem rests on (and --trust=0 governs what lean compiles in that process, not the cached Mathlib .oleans — re-checking those is what leanchecker --fresh is for); the comparator module compiled against Mathlib alone and its copy of the theorem showed sorryAx, as it must. The statement matches the challenge two ways: the pp.all prints of the definition and the theorem are identical once the comparator's binder names (colorCount, coloring, point, otherPoint) are renamed to the solution's (k, c, x, y) — the solution did not paste the challenge text, it restated it — and, decisively, a probe that copies the comparator's ProperColoring and theorem statement verbatim into a fresh namespace and proves it by OAI.EuclideanFiveColor.no_proper_five_coloring compiles with standard axioms, while the same probe with the distance changed to 2 is rejected with a type mismatch. The page's lower-bound statement compiled as a probe from scratch, with no OpenAI definition in the statement: ∀ c : ℂ → Fin 5, ∃ x y, dist x y = 1 ∧ c x = c y; the same in EuclideanSpace ℝ (Fin 2), transported along the linear isometry ℂ ≃ ℝ²; and the chromatic form — any proper colouring by k colours has k ≥ 6 — each closes from the theorem in a few lines. The wrong-shape control (six colours) fails with a type mismatch, the planted-sorry control reports sorryAx. leanchecker --fresh OAI.Geometry.PlaneColoring.Five — the whole import closure re-checked from the .olean files, Mathlib included — exited 0 after 3,765 s (63 minutes; an empty log is the pass), and the missing-module control exited 1.

What the seats found. Seven tool-equipped referee seats, each briefed to refute — five on disjoint stretches of the paper (§2–3 · §4 with the Lean's transfer · §5–6 · §7 · §8), one on the whole paper as a dependency graph with the Lean statement, one on sources and the world — between them covered all 62 pages from the rendered PDF, each scoped seat line by line through its stretch, and every one returned HOLDS AS READ: no FATAL, no GAP, a short list of cosmetic and exposition notes. Each seat rebuilt something and made it fail on purpose. The §2–3 seat verified the two unit-direction identities of Lemma 3.3 exactly in sympy (controls L → 2L, u → 2u fail), Lemma 3.4 exactly over ℚ(√2, i), Lemma 3.5 on 596 grid cases (the stronger bound w ≤ M fails in 109 of them), every constant in Lemma 2.7, and found the ergodic decomposition the brief suspected was missing written out on p. 22 — and it put its finger on the sentence that separates the algebraic plane from Payne's rational one: p. 13, in the proof of Lemma 2.7, "Each |x_j| < 1 is a sum of two elements of K … The square roots belong to F", which is what forces ℤ[K] = E and fails for ℚ (1 − x²/4 must be a rational square; it is for 5 of 1,101 small rationals), with the same property used again on pp. 18, 19 and 21 and the divisibility of K only for the power maps of §3.2–3.3; it then built a 3-adic counterexample (3 is inert in ℤ[i], so rational rotations act isometrically on ℚ₃(i); Haar measure on the closure of the rotation orbit of 1 there is invariant, ergodic, gives C mass zero and has Fourier coefficient 1 at z = 1) on which Lemma 2.7 fails at exactly that sentence and nowhere earlier, and noted Payne's two-colouring is 2-adic (colour by x + y mod 2; every rational unit step flips it, 1,260 vectors checked). The §4 seat checked Lemma 4.1 and Proposition 4.2 line by line, read the Lean's transfer end to end — measure k ω is the invariant law built from the actual colouring by iterated invariant means and Riesz–Markov; the interface is ProperColoring k c and nothing more; the Lean reaches positivity of the projection by a contraction argument instead of identifying a factor, formalises only the easy half of the spectral claim and never uses Bochner, gets a jointly measurable version correct at every point x rather than almost every x, and calls Theorem 2.3 at exactly one place, residual_fourier → wild_fourier, including the ergodic decomposition — and produced its own rational counterexample: run §4 itself on the proper two-colouring of the rational graph and the measure it manufactures is rotation-invariant, misses the continuous characters and is not Haar (its correlation is ½ or 0 by a parity that is discontinuous everywhere; exact fractions, 2,556 rational units, five controls). The §5–6 seat found where five enters (Proposition 5.6: a third label in a palette leaves the complementary pair, 5 − 3 = 2 — the bound is k − 3, so the argument is tight at five and breaks first there at six), checked the sixty-degree exclusion on the hexagonal 7-colouring (0 of 163,840 angles overlap; an improper colouring overlaps 2.9–4.2%), the expansions of Lemma 5.5 (remainder/d² at 0.70–0.72; a wrong-phase control grows like 1/d), the circle-measure Fourier decay (|J₀(r)|(1+r)^1/2 bounded, ≈ 1.15) and the five-cycle combinatorics (no solution once Lemma 6.7's bans apply, 40 without them). The §7 seat verified the planar cover obstruction by an exact SAT encoding of covers of discretised domains (UNSAT at multiplicity ≤ 2 and mesh ≤ 2 for disks of inradius 2.5 and 2.13; SAT, as it must be, at multiplicity 3, at mesh 5, and for a thin rectangle), corrected two things in our own brief (the obstruction is the paper's Lemma 7.5 on a square of side ten, and Lemma 4.3's first assertion is on Theorem 1.4's critical path — verified), and recorded that the Lean takes a different route through §7 (an acyclic crossing graph and fixed-radius centre disks instead of Lemmas 7.7–7.8 as written) so the kernel proves the theorem without certifying those paper steps. The §8 seat redid the Moser placement in exact arithmetic over ℚ(√3, √11) — all eleven edges of squared length exactly 1, the graph with no proper three-colouring, all seven vertices strictly inside the region of Lemma 8.8 with the tightest margin at vertex B, P′ − P ≈ 7·10⁻⁴ (certified ≥ 6.96·10⁻⁴), the paper's own §8.6 residuals reproduced to the digit, seven corruptions rejected — which agrees with our own exact check (the one finite piece we re-derived ourselves, with the region test failing at z = i/2 and z = 1 as controls), enumerated the 34 six-position words of Lemma 8.3, exhausted the five-cycle sign system (0 of 32,768 patterns) and noted that Proposition 8.2 does not actually need the palette bound it cites. The whole-paper seat built the dependency graph, confirmed that nothing in the 70 modules weakens the statement (no instance touches the norm or the measure on ℂ; the Fact instances — 0 < 2π, and on our own grep also 2 ≠ ⊤ in ℝ≥0∞ — are true; WeakColoring is equivalent to Definition 1.2, whose verbatim transcription sits in Basic.lean, which Five.lean does not import; the seven-colouring is formalised separately as Problem160.properColoring_seven), produced two more rational counterexamples by exact arithmetic (Haar measure on the annihilator of the span of the rational units, which excludes 1/3 — the one reasoned out above — and laws built from the parity character, −1 on all 3,820 rational units tested), found that divisibility of K is not the deciding property (roots of unity are divisible and still give a counterexample), stated the general theorem the method proves (a real algebraic field closed under square roots, rotations divisible by 2 and 3), located where the hexagonal seven-colouring escapes the §5–8 chain (§8.4, as it must), and raised one flag that is not an error: Proposition 4.2's proof never uses that the forbidden distance is 1, so read verbatim for any set of real-algebraic distances, together with Furstenberg–Katznelson–Weiss, it would settle Soifer's 2ⁿ-distance problem and Kahle's n!-distance problem, which Davies–McCarty–Pilipczuk listed as open in 2023 — the distance-set transfer behind it is one Sergi Galán had already stated publicly on 10 October ("This is OpenAI's transfer, run with several distances and for fractional colourings": for every set D of algebraic distances, χ(ℝ², D) ≥ 1/m_D(ℝ²)), without naming Soifer's or Kahle's problems — consistent with everything known, clear of Bukh's conjecture on algebraically independent distances, and a reason to keep the scrutiny on Theorem 2.3. It also caught the trap we had walked into ourselves: the text at (8.6) says "a rotation followed by a translation", the displayed formula is translate-then-rotate, and read literally three Moser vertices fall outside the region — the formula and Table 1 are right (our own check now carries that literal reading as a logged control: it puts exactly those three vertices, 0, uB and uT, outside the region). The sources seat checked 24 of the 33 references at the cited locators and found no mismatch (Falconer, Hadwiger and Woodall through secondary sources behind publisher walls, Zimmer's two by abstract, three by metadata only, Furstenberg 1977 closed access and not load-bearing), confirmed footnote 1 against Reed's May manuscript (his Lean takes the false π/3 density bound as a hypothesis; the half-open arc is a counterexample, and a unit-pair-free subset of the circle can in fact have measure π), and found the most material of the citations the paper is missing (the others being Székely 1984 and Shelah–Soifer on whether χ and χ_m can differ): Definition 1.2 is the independent-set notion for the circle-convolution operator of Bachoc–DeCorte–de Oliveira Filho–Vallentin (2014, Definition 2.1 and §3.4), as JoshuaZ had also pointed out.

The world, 14 October. The problem page records nothing of this: "5 ≤ χ ≤ 7", de Grey credited for the lower bound, the proof-claims tab empty, commenting suspended site-wide, last edited 22 January. The teorth database says open (last updated 31 August 2025). Bloom's 8 October post lists #508 ("This proof has been formalised. The PDF is 62 pages long.") and marks it "(partial)" on the FrontierMath list, with his caveat that he has "not yet looked at in any serious way" any of the proofs; none of the comments under it touches #508. Our brief assumed nobody had rebuilt the Lean, and that had been out of date for a week. Formal Conjectures merged HadwigerNelsonAtLeastSix as research solved on 11 October (PR #6898, by source inspection, a sorry grep and the comparator config — not a rebuild), while the exact-value statement stays open. Five third parties record machine checks: plasma-ai's claim card (7 October: "kernel-checked Lean proofs were built and axiom-audited here"); Sergi Galán's repository (decalion89, 9–10 October), which reports all 70 modules built and kernel-replayed and goes further — patches that run the same proof over the constructible, origami and radical fields, with notes listing the same four uses of square roots and the same uses of divisibility our seats found; cert-machine's comparator run (10 October, two GitHub Actions runs: the default Lean kernel and the nanoda kernel both accept the solution, with a control that fails); AI-hard's Comparator run at fd4aeeb (10–11 October, pass); and Li–Su (arXiv:2610.15424, 11 October), who rebuild the transfer half because they build a theorem on it: a single-class version of the transfer gives the first half of the Dúcz–Varga conjecture on the independence ratio of unit-distance graphs (#1070), "its only non-classical input" being Theorem 2.3. James Davies (arXiv:2610.12301, 8 October, two days after the release) proves by a different lattice method that, for finite distance sets with rational squares, χ(ℝ⁴) = χ_m(ℝ⁴) and, for d ≥ 5, χ(ℚ^d) = χ(ℝ^d) = χ_m(ℝ^d) — the full measurable coincidence in high dimension, stronger than Theorem 1.3's weak-measurable one — and conjectures χ(ℝ²) = 6; so Theorem 1.3 is new in the plane, with Davies's as the concurrent high-dimensional statement. Ying Xie's survey of the release (arXiv:2610.17090, 12 October) classifies the transfer as new ("the initial literature comparison found no matching transfer theorem"), and Davidson (arXiv:2610.09474, 7 October) already uses the result as an input. Public reaction is real and thin: Zelinsky on Bluesky the night of the release ("it doesn't look like the method is a direction that the prior lit used to my knowledge"), JoshuaZ on LessWrong (the Bachoc et al. citation gap), Dmitry Rybin on X ("totally unbelievable alien math?", 260,000 views), Gil Kalai's 7 October round-up (a report), and a MathOverflow question of 13 October asking for an explicit finite unit-distance graph that is not 5-colourable (score 22, no answer; the proof is existential by de Bruijn–Erdős, and the smallest known non-4-colourable graph has 509 vertices). We found no mention of it in Tao's or Aaronson's posts on the release; Hacker News has nothing on it at all (five queries, with positive controls). What no one has published in eight days is a referee reading of the human-readable argument; the closest public engagement with Payne's obstruction — without naming it — is Galán's field notes, which list the same uses of square roots our seats found, publish the same 3-adic counterexample over ℚ(i) that our §2–3 seat built, and re-run the Lean over smaller fields. One consequence the paper never states, found by the sources seat: Theorem 1.4 on its own gives χ_m(ℝ²) ≥ 6 — a measurable proper five-colouring is a weak measurable one — the first improvement on Falconer's 1981 measurable bound, and it does not depend on the transfer at all. The paper is unchanged since the repository's first commit (6 October 21:58Z); the 8 October revision of other manuscripts did not touch family 158.

Labels. Theorem 1.1 — no proper five-colouring of the plane, arbitrary colour classes, hence 6 ≤ χ(ℝ²) ≤ 7 — (d) computer-assisted: OpenAI's own Lean, kernel-replayed here with the statement matched to the challenge (by α-renamed pp.all print and, decisively, by proving the comparator's verbatim statement from the solution), the page's lower-bound statement compiled from scratch in three forms, standard axioms for the theorem and everything it rests on, the six-colour and distance-2 controls rejected and the sorry control visible; the same comparator independently accepted by cert-machine on two kernels, with four other parties recording machine checks. The leanchecker --fresh pass over the whole closure, Mathlib included, is what completes the (d). The 62-page human-readable proof: (c) plausible/unverified by a human — seven tool-equipped machine seats covered it, each scoped seat line by line through its stretch, each briefed to refute, and found no gap; no human has reviewed it publicly. The finite pieces re-derived here with controls — the Moser placement certificate, the unit-direction identities, the planar cover obstruction on discretised domains, the six-position words and the five-cycle sign system, the sixty-degree exclusion on the hexagonal colouring — are (a) elementary; the rational-field counterexamples to Theorem 2.3's analogue are hand arguments about infinite objects, supported by finite checks. What the kernel certifies is Theorem 1.1, Theorem 1.4 for Borel colourings in the product-null form of Definition 1.2 (no_measurable_weak_five_coloring; the equivalence of that form with the paper's integrals and the step from Lebesgue to Borel, modifying on a null set, are one-liners not formalised) and the forward half of Theorem 1.3; what it does not certify is the paper's route through §7 (the Lean takes another), Corollary 1.5's constant, any finite 6-chromatic unit-distance graph (none is known), or the value of χ. Scoreboard: #508 stays open — the exact value — with the lower bound moved from 5 to 6 by a theorem that is OpenAI's; the replay, the statement probes and the audit are ours.