A different route to the five-color bound, checked from definitions to final theorem.

How evenly can five colors be distributed around every edge of a graph? In a strong majority edge-coloring, no color may occupy more than half of the edges adjacent to any given edge. The only local obstruction is an edge joining vertices of degrees 1 and 2; graphs without one are called admissible. Kalinowski, Kamyczura, Pilśniak, and Woźniak introduced the problem in 2026, proved that eight colors suffice, and conjectured the optimal bound of four. Antoniuk, Prorok, and Salia proved in June 2026 that every admissible graph has such a coloring with five colors. Here that theorem receives a different proof and a complete Lean 4 verification: the statement was accepted by the Lean kernel on 11 July, eleven days after the original was posted.

The problem

For an edge uv, count all edges incident to u or v, excluding uv itself. A coloring is strong majority when each individual color appears on at most the integer floor of half that number. Admissibility — no adjacent degree pair summing to 3 — is equivalent to excluding a degree-1 vertex adjacent to a degree-2 vertex.

The conjectured universal bound is four, and four would be optimal: some admissible graphs need four colors, including the star K_1,4 and subdivided snarks. The result proved by Antoniuk, Prorok, and Salia in Theorem 2 of arXiv:2607.00212, posted 30 June 2026, establishes the next bound: five.

The formal theorem

Every admissible graph admits a strong majority edge-coloring with five colors. In the artifact this is the declaration SMaj.Synthesis.maj_le_five:

def Admissible : Prop :=
  ∀ u v, G.Adj u v → G.degree u + G.degree v ≠ 3

def IsStrongMajority (c : Sym2 V → C) : Prop :=
  ∀ u v, G.Adj u v → ∀ α : C,
    nColor G c u v α ≤ (G.degree u + G.degree v - 2) / 2

theorem maj_le_five (G : SimpleGraph V) [DecidableRel G.Adj]
    (hadm : Admissible G) :
    ∃ c : Sym2 V → Fin 5, IsStrongMajority G c

Here nColor G c u v α is the adjacent-edge count for color α. The theorem was checked on leanprover/lean4:v4.28.0 with mathlib pinned.

The proof in brief

The verified proof builds a five-color glue coloring, a four-condition interface already shown in the program's earlier six-color formalization to imply the strong majority property. Its stages are:

1. Decompose the graph into chains, whose interior vertices have degree 2, running between junctions of degree at least 3.
2. At each junction of degree d, bundle its incident edge-slots into at most ⌈d/4⌉ groups of size at most 4.
3. Contract every short chain to an edge between groups, producing an auxiliary multigraph of maximum degree 4.
4. Use two local simplifications to set aside parallel edges until the remaining graph is simple. Vizing's theorem then gives it a proper five-edge-coloring.
5. Reinsert the set-aside edges greedily, transport the colors back to the original graph, and fill the interiors of long chains by a list-avoidance lemma.

The construction and its final dispatch are kernel-checked end to end.

Relation to the original proof

The posted proof follows a different route. It trims the graph by five reductions, applies the Hilton–de Werra equitable coloring theorem, then reverses the reductions with local recoloring. The verified proof instead uses chain contraction and Vizing's theorem.

The routes nevertheless share the same hard core at degree 4. Any equitable-coloring statement strong enough there contains Vizing at Δ = 4 as a special case: with five colors, equitability forces the incident color counts 1,1,1,1,0. The work here is an alternative proof, found with the original statement known — not an independent discovery.

What formalization clarified

Formalization-grade reading of the posted proof surfaced three points in the written argument, none affecting the theorem. They were confirmed against the hash-pinned arXiv v1 LaTeX source by a second internal review pass and communicated privately to the authors, with a repair, before this page went live. The full memo sent to the authors is public: read the memo. These are claims about the prose mathematics, not kernel-checked results.

• Substantive: 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 — 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.
• 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: a one-line count using the bound only at the other endpoint restores it — the authors handle exactly this subtlety in their five-color proof, but the corresponding step is omitted in Theorem 4's.
• Editorial: the proof of the paper's Claim 10 contains two consecutive drafts of the same "Case k = 1" paragraph. The count both drafts rely on is correct.

Verification, provenance, and limits

The final declaration's #print axioms output is exactly [propext, Classical.choice, Quot.sound], so no sorryAx occurs anywhere in its transitive dependency closure; the sources use no native_decide. Two independently produced verification blocks were rebuilt from source in separate clean environments. They share one prover's construction skeleton, so they are independent as verifications, not as top-to-bottom proofs. One auxiliary lemma (Λ1) was proved and confirmed but is not a dependency of the shipped theorem, which uses equivalent in-file machinery.

The kernel guarantees the Lean statement. The correspondence between its definitions and the paper's conventions — integer floors, admissibility, and adjacency — is documented with itemized quotations and small-case decide demonstrations in the reading kit; that bridge is necessarily human-audited. The work passed adversarial internal review, an adversarial instance battery, and independent rebuilds, but it has not received external review. Corrections will be logged, dated, and never silent.

Demonstrandum is an autonomous mathematical research system directed by John Erlbacher. It coordinates reasoning systems for problem selection, sustained attack, internal review, and machine verification; in this project, an OpenAI reasoning model built the construction core, an Anthropic reasoning model proved the Vizing lemma, and Harmonic's Aristotle supplied several lemmas and components. The endgame was fast: the final theorem reached its second kernel confirmation about three hours and forty minutes after the decision to attempt it, eleven days after the source paper was posted. The architecture is proprietary; Erlbacher directed the work, audited every acceptance, and takes responsibility for the claims. The artifact includes Vizing at Δ ≤ 4 in its own multigraph encoding, not in full generality. Upstreaming this in-project edge-coloring infrastructure to mathlib is planned; the artifact is standalone by design.

The theorem is Antoniuk–Prorok–Salia's; the contributions here are its verification and the alternative proof route. Bhoja's prior Lean formalization of Vizing's theorem (arXiv:2512.13999) uses a bespoke graph type. At our pin, mathlib provides edge labelings (SimpleGraph.EdgeLabeling) but no proper edge-coloring theory — no properness predicate, chromatic-index results, or Vizing; a basic edge-coloring API is in development in mathlib4#33313. To our knowledge, the only prior mathlib-based edge-coloring development found in the recorded search was a 2023 course project proving the easy lower bound. To our knowledge, the Kierstead-path recoloring machinery appears to be the first formalization of its kind in a proof assistant; that search covered mathlib, GitHub Lean code, Isabelle AFP, Coq/MathComp, Mizar MML, Metamath, the 100/1000+ theorem lists, and arXiv.

Artifacts

Open: four colors

The conjecture of Kalinowski, Kamyczura, Pilśniak, and Woźniak — Maj′(G) ≤ 4 for every admissible graph (Conjecture 14 of arXiv:2605.23828) — remains open. Exact computation supplies evidence, not proof: every one of the 268,478 admissible graphs on at most nine vertices satisfies the bound, as do the 89,771 connected 4-regular graphs at orders 10, 12, and 14 in the released census. The smallest graph requiring four is the paw, a triangle with a pendant edge. To our knowledge, no admissible graph requiring five colors has ever been observed.

To our knowledge, the four-color program now gives the first machine-checked strong-majority results: kernel-complete re-proofs of the published cubic and 4-regular bounds; the genuinely new mixed degree-{3,4} improvement from five colors to four is one open descent lemma from complete; the full conjecture remains open.