Five_Color_Theorem

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result Five_Color_Theorem is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

A planar graph G can be assigned a proper vertex k-coloring such that k <= 5.

Why this node was retired

The posted statement is

theorem Five_Color_Theorem : ∀ (V : Type _) (E : V → V → Prop) (_ : DecidableRel E), True := by sorry

The goal is ∀ (V : Type _) (E : V → V → Prop) (_ : DecidableRel E), True, closed by fun _ _ _ => trivial. Neither planarity nor a colouring appears anywhere.

What a faithful statement would require

A real planarity hypothesis on the graph and a conclusion producing a proper vertex colouring with five colours are both required.

No corrected replacement node exists yet.