Lean-27 : coloration d’arêtes et conjecture de Tutte — compagnon formel
Compagnon formel du notebook Python App-22-EdgeColoring-Tutte (même mandat, issue #13031) : ici, les définitions sont écrites en Lean 4 sur Mathlib.Combinatorics.SimpleGraph et interrogées par le compilateur (#check, #eval, decide). Les sorties de ce notebook sont des sorties du compilateur Lean, pas de la prose à propos de Lean.
Le théorème (arXiv 2608.22870, 2026) : tout graphe cubique apex sans pont est 3-arête-colorable. Ce compagnon en livre la partie formalisable aujourd’hui :
les définitions — cubique, 3-arête-colorable, apex — sur SimpleGraph ;
le graphe de Petersen construit en Lean (Kneser KG(5,2)) avec ses faits décidables prouvés (decide) : 10 sommets, 15 arêtes, cubique ;
une vérification exécutable (backtracking en #eval) que le Petersen n’admet aucune 3-coloration d’arêtes ;
l’ancrage Mathlib du fil « couplages » : le théorème de Tutte sur les couplages parfaits, déjà présent dans Mathlib, que le théorème de 2026 généralise côté colorations.
Ce qui est explicitement hors périmètre : la formalisation de la preuve (réductibilité + déchargement) — c’est l’échelle du théorème des quatre couleurs (années-homme, cf. Gonthier) ; et l’énoncé formel de « planaire », que Mathlib n’a pas à cette date.
-- TOUTES les importations de la session viennent ici (tete de session) :
import Mathlib.Combinatorics.SimpleGraph.Basic
import Mathlib.Combinatorics.SimpleGraph.Tutte
import Mathlib.Combinatorics.SimpleGraph.Matching
import Mathlib.Combinatorics.SimpleGraph.DegreeSum
-- L'ancrage Mathlib du fil couplages : le theoreme de Tutte (couplages parfaits).
#check @SimpleGraph.tutte
-- Le coeur du lien coloration <-> couplages :
#check @SimpleGraph.Subgraph.IsPerfectMatching
-- TOUTES les importations de la session viennent ici (tete de session) :
importMathlib.Combinatorics.SimpleGraph.Basic
importMathlib.Combinatorics.SimpleGraph.Tutte
importMathlib.Combinatorics.SimpleGraph.Matching
importMathlib.Combinatorics.SimpleGraph.DegreeSum
-- L'ancrage Mathlib du fil couplages : le theoreme de Tutte (couplages parfaits).
Raw input{"cmd": "-- TOUTES les importations de la session viennent ici (tete de session) :\nimport Mathlib.Combinatorics.SimpleGraph.Basic\nimport Mathlib.Combinatorics.SimpleGraph.Tutte\nimport Mathlib.Combinatorics.SimpleGraph.Matching\nimport Mathlib.Combinatorics.SimpleGraph.DegreeSum\n\n-- L'ancrage Mathlib du fil couplages : le theoreme de Tutte (couplages parfaits).\n#check @SimpleGraph.tutte\n\n-- Le coeur du lien coloration <-> couplages :\n#check @SimpleGraph.Subgraph.IsPerfectMatching"}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 8, "column": 0},
"endPos": {"line": 8, "column": 6},
"data":
"@SimpleGraph.tutte : ∀ {V : Type u_1} {G : SimpleGraph V} [Finite V],\n (∃ M, M.IsPerfectMatching) ↔ ∀ (u : Set V), ¬G.IsTutteViolator u"},
{"severity": "info",
"pos": {"line": 11, "column": 0},
"endPos": {"line": 11, "column": 6},
"data":
"@SimpleGraph.Subgraph.IsPerfectMatching : {V : Type u_1} → {G : SimpleGraph V} → G.Subgraph → Prop"}],
"env": 0}
Lecture.SimpleGraph.tutte énonce l’équivalence de Tutte : un graphe admet un couplage parfait si et seulement s’il ne viole pas la condition de Tutte (aucun sous-ensemble u de sommets tel que le graphe obtenu en contractant u ait un nombre impair de composantes de taille impaire — un IsTutteViolator). C’est le même fil mathématique que notre coloration : une 3-coloration d’arêtes d’un cubique sans pont partitionne les arêtes en 3 couplages parfaits, et le théorème apex de 2026 dit que la suppressibilité d’un sommet garantit cette partition.
-- Definitions formelles sur SimpleGraph (Mathlib n'a ni cubicite ni
-- coloration d'aretes : c'est exactement ce que ce compagnon ajoute en session).
universe u
variable {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj]
/-- Un graphe est **cubique** (3-regulier) si tous ses sommets ont degre 3. -/
def SimpleGraph.IsCubic (G : SimpleGraph V) [DecidableRel G.Adj] : Prop :=
∀ v : V, G.degree v = 3
/-- Un graphe est **3-arete-colorable** s'il existe une coloration de ses aretes
par 3 couleurs telle que deux aretes distinctes partageant un sommet different. -/
def SimpleGraph.Edge3Colorable (G : SimpleGraph V) : Prop :=
∃ f : G.edgeSet → Fin 3, ∀ e e' : G.edgeSet, e ≠ e' →
(∃ v : V, v ∈ (e : Sym2 V) ∧ v ∈ (e' : Sym2 V)) → f e ≠ f e'
/-- Un graphe est **apex relativement a un predicat `P`** (pensez : la planarite)
si retirer UN sommet rend `P` vrai. La planarite n'etant pas dans Mathlib, `P`
reste un parametre : c'est la formulation honnete du concept. -/
def SimpleGraph.IsApexRelativeTo (G : SimpleGraph V)
(P : ∀ {W : Type u} [Fintype W] [DecidableEq W], SimpleGraph W → Prop) : Prop :=
∃ v : V, P (G.induce {w | w ≠ v})
#check @SimpleGraph.IsCubic
#check @SimpleGraph.Edge3Colorable
#check @SimpleGraph.IsApexRelativeTo
-- Definitions formelles sur SimpleGraph (Mathlib n'a ni cubicite ni
-- coloration d'aretes : c'est exactement ce que ce compagnon ajoute en session).
Raw input{"cmd": "-- Definitions formelles sur SimpleGraph (Mathlib n'a ni cubicite ni\n-- coloration d'aretes : c'est exactement ce que ce compagnon ajoute en session).\nuniverse u\nvariable {V : Type u} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj]\n\n/-- Un graphe est **cubique** (3-regulier) si tous ses sommets ont degre 3. -/\ndef SimpleGraph.IsCubic (G : SimpleGraph V) [DecidableRel G.Adj] : Prop :=\n \u2200 v : V, G.degree v = 3\n\n/-- Un graphe est **3-arete-colorable** s'il existe une coloration de ses aretes\npar 3 couleurs telle que deux aretes distinctes partageant un sommet different. -/\ndef SimpleGraph.Edge3Colorable (G : SimpleGraph V) : Prop :=\n \u2203 f : G.edgeSet \u2192 Fin 3, \u2200 e e' : G.edgeSet, e \u2260 e' \u2192\n (\u2203 v : V, v \u2208 (e : Sym2 V) \u2227 v \u2208 (e' : Sym2 V)) \u2192 f e \u2260 f e'\n\n/-- Un graphe est **apex relativement a un predicat `P`** (pensez : la planarite)\nsi retirer UN sommet rend `P` vrai. La planarite n'etant pas dans Mathlib, `P`\nreste un parametre : c'est la formulation honnete du concept. -/\ndef SimpleGraph.IsApexRelativeTo (G : SimpleGraph V)\n (P : \u2200 {W : Type u} [Fintype W] [DecidableEq W], SimpleGraph W \u2192 Prop) : Prop :=\n \u2203 v : V, P (G.induce {w | w \u2260 v})\n\n#check @SimpleGraph.IsCubic\n#check @SimpleGraph.Edge3Colorable\n#check @SimpleGraph.IsApexRelativeTo", "env": 0}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 23, "column": 0},
"endPos": {"line": 23, "column": 6},
"data":
"@SimpleGraph.IsCubic : {V : Type u_1} → [Fintype V] → (G : SimpleGraph V) → [DecidableRel G.Adj] → Prop"},
{"severity": "info",
"pos": {"line": 24, "column": 0},
"endPos": {"line": 24, "column": 6},
"data":
"@SimpleGraph.Edge3Colorable : {V : Type u_1} → SimpleGraph V → Prop"},
{"severity": "info",
"pos": {"line": 25, "column": 0},
"endPos": {"line": 25, "column": 6},
"data":
"@SimpleGraph.IsApexRelativeTo : {V : Type u_1} →\n [Fintype V] →\n [DecidableEq V] → SimpleGraph V → ({W : Type u_1} → [Fintype W] → [DecidableEq W] → SimpleGraph W → Prop) → Prop"}],
"env": 1}
Lecture des signatures.
SimpleGraph.IsCubic (G : SimpleGraph V) : Prop — « tout sommet a degré 3 ». Mathlib fournit G.degree (cardinalité du voisinage), la définition est littérale.
SimpleGraph.Edge3Colorable — une fonction f des arêtes (G.edgeSet, des Sym2 V) vers Fin 3, avec la contrainte : arêtes distinctes partageant un sommet ⇒ couleurs différentes. C’est la coloration d’arêtes usuelle, en un énoncé.
SimpleGraph.IsApexRelativeTo G P — « il existe un sommet v tel que le graphe induit sur V \ {v} satisfait P ». Un point de typage mérite l’attention : G.induce {w | w ≠ v} rend un graphe sur le sous-type↥{w | w ≠ v} (de cardinal n − 1), pas sur V — d’où la signature polymorphe de P (il s’applique à un graphe sur n’importe quel type de sommets fini). Pour le théorème de 2026, P serait la planarité — absente de Mathlib à cette date, d’où le paramètre.
Ces trois définitions ne sont pas dans Mathlib (vérifié : Unknown constant SimpleGraph.IsCubic en tête de session) : le mandat #13031 tranche B les pose en session plutôt qu’en lake neuf.
-- Le graphe de Petersen comme graphe de Kneser KG(5,2) :
-- sommets = paires de Fin 5, aretes = paires DISJOINTES (union de cardinal 4).
/-- Sommets du Petersen : les 2-sous-ensembles de Fin 5. -/
abbrev PetersenVertex := {s : Finset (Fin 5) // s.card = 2}
/-- Adjacence Bool du Petersen : |s union t| = 4, autrement dit paires disjointes
(deux 2-sous-ensembles verifient |s union t| = 4 - |s inter t|). -/
def petersenAdjB (s t : PetersenVertex) : Bool :=
(s.1 ∪ t.1).card = 4
/-- Symetrie : l'union commute. -/
theorem petersenAdjB_symm (x y : PetersenVertex) :
petersenAdjB x y = petersenAdjB y x := by
simp [petersenAdjB, Finset.union_comm]
/-- Anti-reflexivite : |s union s| = 2, different de 4 (le temoin x.2 ferme le but). -/
theorem petersenAdjB_irrefl (x : PetersenVertex) : ¬ petersenAdjB x x := by
simp [petersenAdjB, x.2]
/-- Le graphe de Petersen, via le constructeur `SimpleGraph.mk'` : il exige
l'adjacence Bool AVEC ses deux preuves (symetrie, anti-reflexivite). -/
def petersen : SimpleGraph PetersenVertex :=
SimpleGraph.mk' ⟨petersenAdjB, petersenAdjB_symm, fun x => petersenAdjB_irrefl x⟩
/-- L'instance decisoire : rend l'adjacence decidable, donc tout le graphe executable
(l'equivalence est transparente, Iff.rfl suffit : Adj EST l'adjacence Bool cocee). -/
instance : DecidableRel petersen.Adj := fun s t =>
decidable_of_iff (petersenAdjB s t = true) Iff.rfl
-- Faits decidables PROUVES par decide (pas par la prose) :
example : Fintype.card PetersenVertex = 10 := by decide
#eval petersen.edgeFinset.card
example : petersen.edgeFinset.card = 15 := by decide
example : petersen.IsCubic := by
show ∀ v, petersen.degree v = 3
decide
-- Le graphe de Petersen comme graphe de Kneser KG(5,2) :
-- sommets = paires de Fin 5, aretes = paires DISJOINTES (union de cardinal 4).
/-- Sommets du Petersen : les 2-sous-ensembles de Fin 5. -/
abbrevPetersenVertex:={s:Finset(Fin5)//s.card=2}
/-- Adjacence Bool du Petersen : |s union t| = 4, autrement dit paires disjointes
-- Faits decidables PROUVES par decide (pas par la prose) :
example:Fintype.cardPetersenVertex=10:=bydecide
15
example:petersen.edgeFinset.card=15:=bydecide
example:petersen.IsCubic:=by
show∀v,petersen.degreev=3
decide
--% env 2
Raw input{"cmd": "-- Le graphe de Petersen comme graphe de Kneser KG(5,2) :\n-- sommets = paires de Fin 5, aretes = paires DISJOINTES (union de cardinal 4).\n/-- Sommets du Petersen : les 2-sous-ensembles de Fin 5. -/\nabbrev PetersenVertex := {s : Finset (Fin 5) // s.card = 2}\n\n/-- Adjacence Bool du Petersen : |s union t| = 4, autrement dit paires disjointes\n(deux 2-sous-ensembles verifient |s union t| = 4 - |s inter t|). -/\ndef petersenAdjB (s t : PetersenVertex) : Bool :=\n (s.1 \u222a t.1).card = 4\n\n/-- Symetrie : l'union commute. -/\ntheorem petersenAdjB_symm (x y : PetersenVertex) :\n petersenAdjB x y = petersenAdjB y x := by\n simp [petersenAdjB, Finset.union_comm]\n\n/-- Anti-reflexivite : |s union s| = 2, different de 4 (le temoin x.2 ferme le but). -/\ntheorem petersenAdjB_irrefl (x : PetersenVertex) : \u00ac petersenAdjB x x := by\n simp [petersenAdjB, x.2]\n\n/-- Le graphe de Petersen, via le constructeur `SimpleGraph.mk'` : il exige\nl'adjacence Bool AVEC ses deux preuves (symetrie, anti-reflexivite). -/\ndef petersen : SimpleGraph PetersenVertex :=\n SimpleGraph.mk' \u27e8petersenAdjB, petersenAdjB_symm, fun x => petersenAdjB_irrefl x\u27e9\n\n/-- L'instance decisoire : rend l'adjacence decidable, donc tout le graphe executable\n(l'equivalence est transparente, Iff.rfl suffit : Adj EST l'adjacence Bool cocee). -/\ninstance : DecidableRel petersen.Adj := fun s t =>\n decidable_of_iff (petersenAdjB s t = true) Iff.rfl\n\n-- Faits decidables PROUVES par decide (pas par la prose) :\nexample : Fintype.card PetersenVertex = 10 := by decide\n\n#eval petersen.edgeFinset.card\n\nexample : petersen.edgeFinset.card = 15 := by decide\n\nexample : petersen.IsCubic := by\n show \u2200 v, petersen.degree v = 3\n decide", "env": 1}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 33, "column": 0},
"endPos": {"line": 33, "column": 5},
"data": "15"}],
"env": 2}
Lecture. Le Petersen est encodé comme le graphe de Kneser KG(5,2) : les sommets sont les paires d’un ensemble à 5 éléments (il y en a 10), et deux paires sont adjacentes quand elles sont disjointes — l’adjacence Bool (s.1 ∪ t.1).card = 4 le dit en une ligne. La structure SimpleGraph est construite via le constructeur SimpleGraph.mk', qui exige l’adjacence Bool avec ses deux preuves — la symétrie (commutativité de l’union) et l’anti-réflexivité (|s ∪ s| = 2 ≠ 4) : impossible de construire un « graphe » dont la relation ne serait pas symétrique. L’instance DecidableRel (via decidable_of_iff, l’équivalence étant définitionnelle) est ce qui rend le graphe exécutable.
Les trois faits qui suivent sont prouvés par decide — le compilateur énumère et tranche, la prose n’intervient pas : Fintype.card PetersenVertex = 10, petersen.edgeFinset.card = 15, et petersen.IsCubic (chaque paire est disjointe des C(3,2) = 3 paires portées par les 3 éléments restants). Pour ce dernier, le show ∀ v, petersen.degree v = 3 déplie d’abord la définition : decide synthétise son instance sur la forme ∀-sur-Fintype, pas sur le nom IsCubic.
-- Verification EXECUTABLE : backtracking exhaustif des 3-colorations propres.
-- Representation : chaque arete est une PAIRE ORDONNEE fixee a la construction.
-- (Decomposer computablement un Sym2 en ses extremites exigerait Multiset.toList,
-- noncomputable ; fixer le representant a la construction est le prix honnete de
-- l'executabilite -- sans perte : une liste d'aretes bien construite contient
-- chaque arete exactement une fois, avec un seul representant.)
/-- `true` ssi les aretes (paires ordonnees) e et e' partagent une extremite. -/
def sharesVertexB {W : Type u} [DecidableEq W] (e e' : W × W) : Bool :=
e.1 == e'.1 || e.1 == e'.2 || e.2 == e'.1 || e.2 == e'.2
/-- Deux aretes sont adjacentes : distinctes et partageant une extremite. -/
def edgesAdjacentB {W : Type u} [DecidableEq W] (e e' : W × W) : Bool :=
decide (e ≠ e') && sharesVertexB e e'
/-- Coloration partielle : liste de (arete, couleur) propres deux a deux. -/
abbrev Partial (W : Type u) := List ((W × W) × Fin 3)
/-- Les 3 couleurs, de facon computable (List.range + garde de borne). -/
def fin3List : List (Fin 3) :=
(List.range 3).filterMap fun n => if h : n < 3 then some ⟨n, h⟩ else none
/-- Etendre une coloration partielle par l'arete e avec chaque couleur sans conflit. -/
def extendPartial {W : Type u} [DecidableEq W] (e : W × W) (p : Partial W) : List (Partial W) :=
fin3List.filterMap fun c =>
if p.all (fun q => !(edgesAdjacentB e q.1) || q.2 != c) then
some ((e, c) :: p)
else none
/-- Toutes les 3-colorations propres de la liste d'aretes (backtracking). -/
def searchProper {W : Type u} [DecidableEq W] (es : List (W × W)) : List (Partial W) :=
match es with
| [] => [[]]
| e :: rest => (searchProper rest).flatMap (extendPartial e)
-- Les 15 aretes du Petersen, en LITTERAUX (chaque preuve `by decide` tranche
-- card = 2 sur des litteraux ; sur des variables, decide ne pourrait pas).
-- Lecture : chaque ligne est une arete {a,b} -- {c,d} avec les paires DISJOINTES,
-- chaque arete listee exactement une fois.
def petersenEdges : List (PetersenVertex × PetersenVertex) :=
[ (⟨{0, 1}, by decide⟩, ⟨{2, 3}, by decide⟩)
, (⟨{0, 1}, by decide⟩, ⟨{2, 4}, by decide⟩)
, (⟨{0, 1}, by decide⟩, ⟨{3, 4}, by decide⟩)
, (⟨{0, 2}, by decide⟩, ⟨{1, 3}, by decide⟩)
, (⟨{0, 2}, by decide⟩, ⟨{1, 4}, by decide⟩)
, (⟨{0, 2}, by decide⟩, ⟨{3, 4}, by decide⟩)
, (⟨{0, 3}, by decide⟩, ⟨{1, 2}, by decide⟩)
, (⟨{0, 3}, by decide⟩, ⟨{1, 4}, by decide⟩)
, (⟨{0, 3}, by decide⟩, ⟨{2, 4}, by decide⟩)
, (⟨{0, 4}, by decide⟩, ⟨{1, 2}, by decide⟩)
, (⟨{0, 4}, by decide⟩, ⟨{1, 3}, by decide⟩)
, (⟨{0, 4}, by decide⟩, ⟨{2, 3}, by decide⟩)
, (⟨{1, 2}, by decide⟩, ⟨{3, 4}, by decide⟩)
, (⟨{1, 3}, by decide⟩, ⟨{2, 4}, by decide⟩)
, (⟨{1, 4}, by decide⟩, ⟨{2, 3}, by decide⟩) ]
-- Le temoin attendu : AUCUNE 3-coloration propre (le Petersen est un snark).
#eval (searchProper petersenEdges).length
-- Controle positif : K4 (graphe complet sur Fin 4) est cubique et 3-arete-colorable --
-- le chercheur doit trouver ses 3! = 6 1-factorisations.
def ke (a b : Fin 4) : Fin 4 × Fin 4 := (a, b)
def k4Edges : List (Fin 4 × Fin 4) :=
[ ke 0 1, ke 0 2, ke 0 3, ke 1 2, ke 1 3, ke 2 3 ]
#eval (searchProper k4Edges).length
-- Verification EXECUTABLE : backtracking exhaustif des 3-colorations propres.
-- Representation : chaque arete est une PAIRE ORDONNEE fixee a la construction.
-- (Decomposer computablement un Sym2 en ses extremites exigerait Multiset.toList,
-- noncomputable ; fixer le representant a la construction est le prix honnete de
-- l'executabilite -- sans perte : une liste d'aretes bien construite contient
-- chaque arete exactement une fois, avec un seul representant.)
/-- `true` ssi les aretes (paires ordonnees) e et e' partagent une extremite. -/
-- Le temoin attendu : AUCUNE 3-coloration propre (le Petersen est un snark).
0
-- Controle positif : K4 (graphe complet sur Fin 4) est cubique et 3-arete-colorable --
-- le chercheur doit trouver ses 3! = 6 1-factorisations.
defke(ab:Fin4):Fin4×Fin4:=(a,b)
defk4Edges:List(Fin4×Fin4):=
[ke01,ke02,ke03,ke12,ke13,ke23]
6
--% env 3
Raw input{"cmd": "-- Verification EXECUTABLE : backtracking exhaustif des 3-colorations propres.\n-- Representation : chaque arete est une PAIRE ORDONNEE fixee a la construction.\n-- (Decomposer computablement un Sym2 en ses extremites exigerait Multiset.toList,\n-- noncomputable ; fixer le representant a la construction est le prix honnete de\n-- l'executabilite -- sans perte : une liste d'aretes bien construite contient\n-- chaque arete exactement une fois, avec un seul representant.)\n\n/-- `true` ssi les aretes (paires ordonnees) e et e' partagent une extremite. -/\ndef sharesVertexB {W : Type u} [DecidableEq W] (e e' : W \u00d7 W) : Bool :=\n e.1 == e'.1 || e.1 == e'.2 || e.2 == e'.1 || e.2 == e'.2\n\n/-- Deux aretes sont adjacentes : distinctes et partageant une extremite. -/\ndef edgesAdjacentB {W : Type u} [DecidableEq W] (e e' : W \u00d7 W) : Bool :=\n decide (e \u2260 e') && sharesVertexB e e'\n\n/-- Coloration partielle : liste de (arete, couleur) propres deux a deux. -/\nabbrev Partial (W : Type u) := List ((W \u00d7 W) \u00d7 Fin 3)\n\n/-- Les 3 couleurs, de facon computable (List.range + garde de borne). -/\ndef fin3List : List (Fin 3) :=\n (List.range 3).filterMap fun n => if h : n < 3 then some \u27e8n, h\u27e9 else none\n\n/-- Etendre une coloration partielle par l'arete e avec chaque couleur sans conflit. -/\ndef extendPartial {W : Type u} [DecidableEq W] (e : W \u00d7 W) (p : Partial W) : List (Partial W) :=\n fin3List.filterMap fun c =>\n if p.all (fun q => !(edgesAdjacentB e q.1) || q.2 != c) then\n some ((e, c) :: p)\n else none\n\n/-- Toutes les 3-colorations propres de la liste d'aretes (backtracking). -/\ndef searchProper {W : Type u} [DecidableEq W] (es : List (W \u00d7 W)) : List (Partial W) :=\n match es with\n | [] => [[]]\n | e :: rest => (searchProper rest).flatMap (extendPartial e)\n\n-- Les 15 aretes du Petersen, en LITTERAUX (chaque preuve `by decide` tranche\n-- card = 2 sur des litteraux ; sur des variables, decide ne pourrait pas).\n-- Lecture : chaque ligne est une arete {a,b} -- {c,d} avec les paires DISJOINTES,\n-- chaque arete listee exactement une fois.\ndef petersenEdges : List (PetersenVertex \u00d7 PetersenVertex) :=\n [ (\u27e8{0, 1}, by decide\u27e9, \u27e8{2, 3}, by decide\u27e9)\n , (\u27e8{0, 1}, by decide\u27e9, \u27e8{2, 4}, by decide\u27e9)\n , (\u27e8{0, 1}, by decide\u27e9, \u27e8{3, 4}, by decide\u27e9)\n , (\u27e8{0, 2}, by decide\u27e9, \u27e8{1, 3}, by decide\u27e9)\n , (\u27e8{0, 2}, by decide\u27e9, \u27e8{1, 4}, by decide\u27e9)\n , (\u27e8{0, 2}, by decide\u27e9, \u27e8{3, 4}, by decide\u27e9)\n , (\u27e8{0, 3}, by decide\u27e9, \u27e8{1, 2}, by decide\u27e9)\n , (\u27e8{0, 3}, by decide\u27e9, \u27e8{1, 4}, by decide\u27e9)\n , (\u27e8{0, 3}, by decide\u27e9, \u27e8{2, 4}, by decide\u27e9)\n , (\u27e8{0, 4}, by decide\u27e9, \u27e8{1, 2}, by decide\u27e9)\n , (\u27e8{0, 4}, by decide\u27e9, \u27e8{1, 3}, by decide\u27e9)\n , (\u27e8{0, 4}, by decide\u27e9, \u27e8{2, 3}, by decide\u27e9)\n , (\u27e8{1, 2}, by decide\u27e9, \u27e8{3, 4}, by decide\u27e9)\n , (\u27e8{1, 3}, by decide\u27e9, \u27e8{2, 4}, by decide\u27e9)\n , (\u27e8{1, 4}, by decide\u27e9, \u27e8{2, 3}, by decide\u27e9) ]\n\n-- Le temoin attendu : AUCUNE 3-coloration propre (le Petersen est un snark).\n#eval (searchProper petersenEdges).length\n\n-- Controle positif : K4 (graphe complet sur Fin 4) est cubique et 3-arete-colorable --\n-- le chercheur doit trouver ses 3! = 6 1-factorisations.\ndef ke (a b : Fin 4) : Fin 4 \u00d7 Fin 4 := (a, b)\n\ndef k4Edges : List (Fin 4 \u00d7 Fin 4) :=\n [ ke 0 1, ke 0 2, ke 0 3, ke 1 2, ke 1 3, ke 2 3 ]\n\n#eval (searchProper k4Edges).length", "env": 2}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 58, "column": 0},
"endPos": {"line": 58, "column": 5},
"data": "0"},
{"severity": "info",
"pos": {"line": 67, "column": 0},
"endPos": {"line": 67, "column": 5},
"data": "6"}],
"env": 3}
Lecture — la vérification exécutable. Un point de représentation d’abord : le chercheur travaille sur des paires ordonnées — une par arête, fixée à la construction — plutôt que sur des Sym2. Décomposer computablement un Sym2 en ses deux extrémités exigerait Multiset.toList, marquée noncomputable dans Mathlib ; fixer le représentant à la construction est le prix honnête de l’exécutabilité, et il est sans perte : la liste d’arêtes contient chaque arête exactement une fois.
#eval (searchProper petersenEdges).length rend 0 : le backtracking a énuméré l’espace des colorations propres partielles des 15 arêtes et n’en a complété aucune. Le chercheur n’est pas une heuristique : il étend une coloration partielle seulement par des couleurs sans conflit (extendPartial filtre les trois candidats par arête), donc une coloration complète sortie de searchProper serait une vraie 3-coloration — il n’y en a pas, et le 0 en est le témoin exécutable.
Le contrôle positif sur la même cellule : sur K4 (les 6 arêtes du graphe complet sur Fin 4, cubique et 3-arête-colorable), le même chercheur rend 6 — les 3! 1-factorisations, une par permutation des couleurs. Le chercheur n’est donc pas aveuglément nul : il trouve quand il y a à trouver, et son 0 sur le Petersen a une valeur de témoin.
Ce 0 est une vérification, pas une preuve : la différence de nature avec decide (qui produit un terme de preuve) est assumée ici. La preuve formelle que le Petersen n’est pas 3-arête-colorable existe dans la littérature et serait formalisable ; la preuve du théorème apex complet (réductibilité + déchargement) est un programme de recherche à l’échelle du théorème des quatre couleurs — hors périmètre du mandat #13031.
Pourquoi le théorème de 2026 ne s’énonce pas encore formellement ici
Deux murs, de natures différentes :
La planarité n’est pas dans Mathlib. Notre IsApexRelativeTo prend le prédicat de planarité comme paramètreP — honnête, mais tant que P n’est pas instancié, l’énoncé « cubique + sans pont + apex ⇒ 3-colorable » reste un schéma. Formaliser la planarité (via les embeddings combinatoires ou les matroïdes graphiques) est un sous-projet en soi.
La preuve est un programme, pas un lemme. Même avec la planarité, la preuve du papier combine un ensemble de réductibilité vérifié par ordinateur et une phase de déchargement — exactement la structure de la preuve des quatre couleurs, dont la formalisation (Gonthier, 2005) a pris des années-homme.
Ce que ce compagnon laisse au lecteur est donc la grammaire du théorème : IsCubic, Edge3Colorable, IsApexRelativeTo, un Petersen exécutable, et l’équivalence de Tutte (SimpleGraph.tutte) comme racine Mathlib du fil couplages. Le notebook Python compagnon (App-22) porte, lui, la vérification empirique à large échantillon (48 graphes, 0 violation).
Exercices
Un snark plus grand. Construisez le blow-up du Petersen (remplacez chaque sommet par un triangle) et relancez searchProper : il n’est pas 3-colorable non plus. Que dit la taille de l’espace exploré ?
Couplages. Montrez par #eval que chaque couleur d’une coloration du prisme couvre tous les sommets — c’est-à-dire que Edge3Colorable sur un cubique revient à partitionner en couplages parfaits (Subgraph.IsPerfectMatching).
Sans pont. Énoncez IsBridgeless sur SimpleGraph (indice : G.deleteEdges {e} reste connexe pour toute arête e — SimpleGraph.Connected existe dans Mathlib).
Conclusion
Le compagnon a fait exécuter au compilateur : l’équivalence de Tutte (racine Mathlib du fil couplages), la structure du Petersen (10 sommets, 15 arêtes, cubique — trois decide), et l’absence de 3-coloration du Petersen par backtracking exhaustif (0). Les définitions IsCubic / Edge3Colorable / IsApexRelativeTo restent en session : elles vivent dans ce notebook, disponibles pour toute future formalisation quand Mathlib aura la planarité.