The flagship article presents the five-color theorem — proved by Antoniuk, Prorok, and Salia in arXiv:2607.00212, posted 30 June 2026 — and its Lean verification. This chronicle records how the alternative proof was found, tested, repaired, raced across three proof systems, and checked.

Morning of 11 July

The starting position on the morning of 11 July: the program had a complete kernel-checked proof that six colors suffice, built around the glue-coloring interface; a same-morning formalization of a recoloring toolkit (rotation and color-swap lemmas after Kierstead's method — to our knowledge the first formalization of Kierstead-path machinery in any proof assistant — closed after a focused session in which the winning proof took about 90 minutes); and a census computation. The six-color proof's own palette came from Shannon's multigraph bound, which is exactly tight at 6 on "fat triangles" — triples of junctions pairwise joined by doubled edges — so the six-color architecture could not be pushed to five as it stood.

The first review finding was a documented impossibility claim that turned out to be false. The six-color artifact asserted that the glue route could not produce a five-color witness. Review produced a six-vertex counterexample: a fat triangle whose doubled edges are chains. Its five-color glue coloring was checked by the Lean kernel against the frozen definitions. The obstruction applies to Shannon's construction, not to the route as a whole. The assertion had been a comment, not a theorem; subsequent impossibility claims require a formal declaration and axiom audit or an explicit unverified label.

The refutation attempt found no counterexample to the theorem. An exhaustive computation over all 268,478 admissible graphs on at most 9 vertices found a four-coloring for each one; exhaustive checks also covered all 89,771 four-regular graphs on 10, 12, and 14 vertices. To our knowledge, no admissible graph requiring five colors has been observed. This is exact computation: evidence for the open four-color conjecture, not a proof.

In parallel, formalization-grade reading surfaced three clarifications to the paper's argument. One track transcribed the Antoniuk–Prorok–Salia proof step by step, to cost out a faithful formalization of Route A. The theorem survives unaffected; the transcription found three points in the written argument that need repair or tidying. First (minor): the displayed inequality in the proof of the paper's Theorem 4 — the four-color result for graphs with no degree-2 or degree-4 vertices — fails at degree-1 vertices; the conclusion stands, because a one-line count using the bound only at the other endpoint restores it (the authors handle exactly this degree-1 subtlety in their five-color proof, but the corresponding step is omitted in Theorem 4's). Second (editorial): the proof of the paper's Claim 10 contains two consecutive drafts of the same "Case k = 1" paragraph. Third, the substantive one: in undoing the first reduction (R1), the written proof specifies how to restore a degree-5 vertex that lost one loop ear, but a degree-5 vertex carrying two loop ears — two triangles sharing the vertex, plus one pendant edge; a legitimate admissible configuration — finishes the reduction phase holding three auxiliary leaves, a state neither restoration paragraph covers. A repair using only the paper's own tools (its Claim 8 balance property and the distinctness argument of its Remark 9, feeding its Claim 10 extension) closes the case. Before release, all three claims were handed to a second, hostile referee tasked with refuting them, working directly from the hash-pinned arXiv v1 LaTeX source. All three were confirmed — and the hostile pass caught an error of ours: the internal notes had mis-numbered the paper's results (placing the duplicated paragraph in "Claim 7" rather than Claim 10, among other slips), corrected before anything shipped or was sent to the authors. This was confirmed by adversarial internal review against the arXiv v1 source; it concerns prose mathematics, not kernel-checked results. The authors were notified privately, with the repair, before this page went live.

The route was tested before formalization. Fourteen explicit test instances — fat-triangle variants, degree-4-rich graphs, and greedy-jamming configurations — were checked exactly. The first version of Route B failed 3 of 12 applicable checks, including a certified gap in chain transport. The repair used monochromatic transport for length-2 chains and independently colored ports for longer chains. It passed all 15 checks in the extended battery; its structural invariants also passed tests on 1,854 random graphs. Formalization then began.

Route A and Route B

Route A, the paper's proof, uses an equitable-coloring theorem after Hilton and de Werra: if no vertex degree is divisible by k, the graph has a k-edge-coloring in which every vertex sees any two colors almost equally often. Antoniuk–Prorok–Salia perform five graph reductions — removing loop-shaped ears, ears anchored at degree-five vertices, length-two ears, long ears, and finally attaching a leaf wherever the degree is a multiple of five — apply the equitable theorem with k = 5 to the trimmed graph, then undo the reductions in reverse with local recoloring. Degree-five vertices, made temporarily degree-four by the ear removals, end up with a free fifth color that pays for the restorations.

Route B, the verified proof, decomposes the graph into chains — maximal paths whose interior vertices have degree 2 — running between junctions of degree at least 3. At each junction of degree d, it partitions the d edge-ends into at most ⌈d/4⌉ groups of size at most 4, steering group sizes to at most 3 whenever the arithmetic allows (it fails exactly at d = 4, 7, 8, 10, 11, …). Each chain of length at most 2 contracts to an edge between its end-groups, producing an auxiliary multigraph M of maximum degree 4. Two local rules simplify M until the remainder, M₀, is simple: one short chain in each doubled pair between full groups is uncontracted, and the remaining parallel classes are set aside. Vizing's theorem gives M₀ a proper 5-edge-coloring. The proof then reinserts the parallel edges greedily, colors the ports of long chains independently, fills their interiors by a list-avoidance lemma, and transports everything back. A four-condition glue-coloring interface — group-rainbow, group-count, chain-end, and interior — had already been proved in the six-color formalization to imply the strong majority property. Route B's new mathematics is to build a five-color glue coloring.

The two routes share their hard core. Any equitable-coloring statement strong enough at degree-4 vertices contains Vizing at Δ = 4: equitability with five colors forces the incident color counts 1,1,1,1,0, hence local properness. Route A packages that difficulty inside the Hilton–de Werra theorem; Route B proves it directly and reuses previously verified plumbing for everything else.

Formalization and audit

Route B was frozen as five Lean statements against the unchanged six-color artifact — the "ladder":

The target statement and all definitions were byte-unchanged throughout; every candidate proof was diffed against the pins. The target's pin was months old, and the acceptance diff was token-for-token.

Predictions were registered before results came back. Before committing to the ladder, six smaller infrastructure pieces were sent to Harmonic's Aristotle (an automated theorem-proving system) with written acceptance probabilities, logged in advance:

Predicted number of successes: 3.05. Actual: 4. The ranking was perfect — everything rated ≥ 0.45 succeeded, everything ≤ 0.15 failed — but the mid-range predictions were systematically pessimistic, and the recalibration was written down before the next wave. The two failures were the most informative returns of the six: both independently hit the same missing ingredient — the existence of Eulerian trails, which mathlib currently lacks (it is an explicit TODO in mathlib's source) — and both independently derived that a divisibility hypothesis the task header speculated was removable is in fact necessary (witness: K₅ at k = 4; a triangle at k = 2). Two blind runs, same wall, same correction. That settled the architecture question: the equitable-coloring route would cost a from-scratch Euler theory; the Vizing route would not. The predictions and outcomes were all logged before returns.

The five ladder statements then went to three systems: Aristotle (eight submissions across framings), an OpenAI reasoning model, and an Anthropic reasoning model. The latter two iterated against pinned environments. Acceptance required a kernel-checked proof followed by an independent source rebuild and axiom report. The outcomes were:

• Λ1 closed twice, independently, within the hour: Aristotle produced a 42-line proof by explicit closed-form witness (no induction); the OpenAI model produced a 38-line strong-induction proof. Same statement, two structurally different proof objects. (Pre-registered 0.97.)
• Λ2 was the bottleneck: five independent proof attempts on other lemmas each named Vizing-at-Δ≤4 as their single missing prerequisite. At our pin, mathlib provides edge labelings (SimpleGraph.EdgeLabeling) but no proper edge-coloring theory; a basic API is in development in mathlib4#33313. To our knowledge, the only existing Lean formalization of Vizing's theorem — Bhoja, arXiv:2512.13999, Dec 2025 — lives on a bespoke graph type incompatible with this artifact's encoding, so the theorem had to be proved in-file. The Anthropic model supplied an 864-line fan-rotation induction powered by the recoloring kit kernel-checked that morning. Two parallel attempts given progressively less supporting context both reduced to the same final extension step and stopped there. Three attempts, three context levels, strictly monotone progress in context: on a hard named subproblem, what the prover receives matters more than how often it is retried.
• Λ3 was proved outright by Aristotle; its other half was Λ2, so closure of Λ2 made it unconditional.
• Λ4 closed by composition. The OpenAI model built the construction core — the auxiliary-graph combinatorics and the traversal and dispatch engine — while Aristotle submissions returned complementary proved components with near-zero overlap: an interior-fill pass, the chain-end transport layer, and a uniform grouping construction. The last component eliminated one of the two existential witnesses from the statement: it proved that a suitable grouping can be manufactured from any coloring satisfying three row-level properties, shrinking the target from "construct a grouping and a coloring" to "construct a coloring." The pre-registered chances that a single first-wave submission would close Λ4 outright were 0.10–0.15 each and approximately 0.35 that at least one would. None did; their proved partials, rated 0.60–0.75, all landed.
• Λ5 was one line, as predicted (0.95), once Λ4 existed.

After merging the proved components, three lemmas remained: multiplicity cap, interior distinctness, and the chain-end condition. The Anthropic model completed a verification block over the OpenAI model's construction; the OpenAI model independently completed a second verification block. The two proofs share the construction skeleton but have independently produced verification layers.

Each completion was checked separately for token-identity of the statement; absence of sorry and fourteen proof-subversion patterns; one public declaration per file; a clean rebuild of 8,037 compilation jobs; and axiom reports exactly [propext, Classical.choice, Quot.sound], with no sorryAx. The second independent kernel confirmation arrived three hours and forty minutes after the decision to attempt the theorem, using previously verified infrastructure.

Incidents and negative results

• Full closure in the first prover wave was pre-registered at ≈ 0.25 and did not happen; no single Λ4 submission closed it, against an assessed probability of ≈ 0.35 that one would. Full closure came from merging proved partials and iterating.
• Mid-race, one agent-delivered Lean file contained a literal "…440 tokens truncated…" marker, a transport-layer corruption that would have corrupted the artifact if trusted. It was caught by the standing discipline that nothing counts unless it rebuilds from disk in a fresh environment. The file was re-emitted and hash-verified, and hash verification of every file delivery was adopted on the spot.
• One late prover run received a file whose documentation still contained the kernel-refuted impossibility claim and reproduced that claim in its diagnosis; two others working from the same file did not. Refuted claims now get patched at the source file, because downstream readers — human or machine — inherit comments as facts.
• On the same task with identical input, the morning's recoloring crux was closed by the OpenAI model in about 90 minutes and by Aristotle — independently, with a structurally different proof — in 7 hours 21 minutes of prover time. Both proofs kernel-check. The comparison records substantial variance between systems on an identical formal task.

What remains open

The four-color conjecture of Kalinowski, Kamyczura, Pilśniak, and Woźniak — Maj′(G) ≤ 4 for every admissible graph (Conjecture 14 of arXiv:2605.23828) — is open, and the bound 4 would be optimal. The census computed along the way is direct evidence for it: among all 268,478 admissible graphs on at most nine vertices, none needs five colors and, to our knowledge, none has ever been observed anywhere; the smallest graph needing four is the paw, a triangle with one pendant edge. This is exact computation; the conjecture itself is open. The verified five-color machinery was deliberately built with the palette size as a parameter wherever that cost nothing, so parts of it are reusable by whoever — human or machine — takes the next step down.

Related

Produced by Demonstrandum, an autonomous mathematical research system directed by John Erlbacher. Results are accepted only after reduction to independently checkable artifacts.