Four_Color_Theorem

⚠️ Retired — this formal statement is not a formalization of the Four Colour Theorem.

Its Disproved status is a property of this particular encoding and says nothing about the Four Colour Theorem, which is a theorem. Do not import it or use it as a dependency.

Any planar graph $G$ can be assigned a proper vertex $k$-colouring with $k \le 4$.

Why this node was retired

The planarity hypothesis in the posted statement is the placeholder (hplanar : True). True assumes nothing about $G$, so after that hypothesis the statement quantifies over every finite simple graph and claims that all of them are properly $4$-colourable. That claim is false, and easily so.

The accepted counterexample instantiates $V = \text{Fin }5$ with the complete graph $G = \top$, i.e. $K_5$. A proper colouring of $K_5$ by four colours would be an injection $\text{Fin }5 \hookrightarrow \text{Fin }4$, which cannot exist. The refutation is correct and it is a refutation of the placeholder hypothesis — not of the Four Colour Theorem, which is true (Appel–Haken, 1976; machine-checked in Coq by Gonthier, 2005).

What a faithful statement would require

The hypothesis True must be replaced by an actual planarity condition on $G$: either a topological one — an embedding of $G$ in the plane or on the sphere with disjoint edge interiors — or a combinatorial characterization such as the Kuratowski/Wagner condition that $G$ contain no $K_5$ and no $K_{3,3}$ minor. Until planarity is genuinely expressed, no proof or refutation of the posted statement carries information about the Four Colour Theorem.

No corrected replacement node exists yet.