Module 3
Formal Proofs
A read-only viewer for the formal proof artifacts that machine-check the Four-Color Theorem. The local adapter replays cached verification states; swapping in a remote Coq / Lean service is a one-file change to ProverAdapter.
Proof skeleton: every minimal counterexample must contain at least one of an unavoidable set of reducible configurations. Discharging gives unavoidability; Kempe-chain extensions give reducibility. The artifacts below are the mechanical certificates.
COQ-2005
39
Replayed via Gonthier's Coq script.
LEAN-VERIFIED
13
Lean 4 community port (in progress).
COMP-1976
12
Original Appel–Haken assembly trace.
UNVERIFIED
0
No cached certificate yet.
Configurations · 64/64
Discharging rule R1 · ring size 6 · interior 2 · edges 14
(* RSST-R-0001-COQ-2005 — adapted from G. Gonthier, "A computer-checked proof of
the four-colour theorem", Notices AMS 55(11), 2008. Coq sources: github.com/coq-community/fourcolor *)
From fourcolor Require Import job color cfgreducible discharge.
(* Each reducible configuration is a small planar near-triangulation.
Reducibility = every coloring of the surrounding ring extends inward,
possibly after Kempe-chain inversions. *)
Lemma reducible_RSST_R_0001_COQ_2005 : reducible_config RSST-R-0001-COQ-2005.
Proof.
apply: cfg_red.
by exact: ring_kempe_extension.
Qed.
(* The discharging argument shows the union of reducible configurations
is unavoidable in any minimal counterexample. *)
Theorem four_color_theorem :
forall G : planar_graph, chromatic_number G <= 4.
Proof. exact: four_color_planar. Qed.Configuration graph
Outlined nodes are the ring; the artifact certifies that any 4-coloring of the ring extends to the interior.