Section 3 — Choose a dart-minimal counterexample

Proved

FourColor.minimal_counterexample_exists

by Minghui · Sep 26, 2026 · Mathlib c5ea003 (Lean v4.30.0)

four-color-theoremgraph-theory

If an admissible hypermap $H$ on $n$ darts is not four-colorable, then there exist $m\le n$ and an admissible hypermap $K$ on $m$ darts such that

\neg\operatorname{FourColorable}(K),\qquad \forall j<m\ \forall L\text{ on }j\text{ darts},\quad \operatorname{Admissible}(L)\Longrightarrow\operatorname{FourColorable}(L).

The comparison class is planar, bridgeless, plain and precubic, including empty hypermaps. It is not restricted to cubic maps.

Formalization note: a formal Lean bridge expressing the well-founded descent used by the source-backed hypermap theorem. It does not assume structural consequences that are proved in later milestones.

Notation: $D=\{0,\ldots,n-1\}$ is the dart set, $n = |D|$ its size, and $p = \nu_H$ is the node permutation. Write $e,f$ for the edge and face permutations, with $p(f(e(d)))=d$ . Edge, node and face counts $E,N,F$ are numbers of permutation orbits, including singleton orbits. The component count $C$ uses the equivalence generated by all three permutations. Planarity means the exact Euler equality $E+N+F=n+2C$ , and connectedness means $C=1$ .

A plain hypermap has a fixed-point-free involution $e$ . Cubic means every node orbit has size three; precubic means every node orbit has size at most three. Bridgeless means $d$ and $e(d)$ never lie in the same face orbit. A $k$ -coloring is a map $D\to\{0,\ldots,k-1\}$ constant on face orbits and different across each edge step. No requirement uses all available colors. The empty dart set has zero components, is planar, and is colorable, but is not connected.

An admissible hypermap is planar, bridgeless, plain and precubic. A minimal counterexample is a non-four-colorable admissible hypermap such that every admissible hypermap with fewer darts is four-colorable. Minimality includes all finite carriers through their enumeration by $\operatorname{Fin}(m)$ ; cubicity, connectedness and lower face-degree bounds are not assumed.

Source: Georges Gonthier, A Computer-Checked Proof of the Four Colour Theorem (2005), https://www.microsoft.com/en-us/research/wp-content/uploads/2012/10/4colproof.pdf; Section 3, PDF p. 7, paragraph on PDF p. 7 beginning the minimal counterexample argument. Relevant displays are unnumbered. Pinned executable reference: https://github.com/rocq-community/fourcolor/blob/c1d6b1cd5288bea4b067aac13cdde3c18dffe018/theories/proof/coloring.v#L224; https://github.com/rocq-community/fourcolor/blob/c1d6b1cd5288bea4b067aac13cdde3c18dffe018/theories/proof/combinatorial4ct.v#L18.

Preamble

import Definitions.Def_FourColor_Hypermap

Formal statement

namespace FourColor
universe u
theorem minimal_counterexample_exists :
  ∀ (n : ℕ) (H : Hypermap n), H.Admissible → ¬ H.FourColorable →
    ∃ (m : ℕ) (K : Hypermap m), m ≤ n ∧ K.MinimalCounterexample := by sorry
end FourColor

Source

Georges Gonthier, A Computer-Checked Proof of the Four Colour Theorem (2005), https://www.microsoft.com/en-us/research/wp-content/uploads/2012/10/4colproof.pdf; Section 3, PDF p. 7, paragraph on PDF p. 7 beginning the minimal counterexample argument. Relevant displays are unnumbered. Pinned executable reference: https://github.com/rocq-community/fourcolor/blob/c1d6b1cd5288bea4b067aac13cdde3c18dffe018/theories/proof/coloring.v#L224; https://github.com/rocq-community/fourcolor/blob/c1d6b1cd5288bea4b067aac13cdde3c18dffe018/theories/proof/combinatorial4ct.v#L18.

Read-back

What the Lean code literally says, in plain math · gpt-6

MinimalCounterexampleExistence. For every $d\in\mathbb N$ , a triple $J=(e_J,\nu_J,\phi_J)$ on $D_d=\{0,\ldots,d-1\}$ means three permutations satisfying $\nu_J(\phi_J(e_J(x)))=x$ for every $x$ . A $\sigma$ -cycle is a class for $\exists j\in\mathbb Z,\ \sigma^j(x)=y$ , with inverse powers for negative $j$ . Let $E_J,N_J,F_J$ count its edge, node, and face cycles, and let $C_J$ count the classes of the equivalence relation generated by every edge, node, and face permutation step, including reflexivity, symmetry, and transitivity. Condition $A$ means $E_J+N_J+F_J=d+2C_J$ , no $x$ shares a $\phi_J$ -cycle with $e_J(x)$ , $e_J(e_J(x))=x$ and $e_J(x)\ne x$ for every $x$ , and every $\nu_J$ -cycle has at most three elements. A coloring means a function $c:D_d\to\{0,1,2,3\}$ constant on every $\phi_J$ -cycle and satisfying $c(e_J(x))\ne c(x)$ for every $x$ , without requiring every color to be used. The proposition says that for every $n\in\mathbb N$ and every such triple $H$ on $D_n$ , if $H$ satisfies $A$ and has no coloring, then there exist $m\in\mathbb N$ and such a triple $K$ on $D_m$ such that $m\le n$ , $K$ satisfies $A$ , $K$ has no coloring, and for every natural number $\ell<m$ and every such triple $L$ on $D_\ell$ , if $L$ satisfies $A$ then $L$ has a coloring. No relationship between $H$ and $K$ beyond these conditions is required; $m=n$ is permitted. Empty dart sets are included, but they admit the empty coloring, so the antecedent cannot hold for $n=0$ and no witness can have $m=0$ .

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by Minghui · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph