est. 1852 · proven 1976 · re-proven 2005
Four colors. No more, no less.
TetraChroma Lab is a working notebook for the Four-Color Theorem — visual intuition, the 1,482 / 633 unavoidable configurations, MCMC experimentation, and the formal proofs that finally closed the gap.
Theorem
Every planar graph admits a proper 4-coloring.
Discharging identity
The total charge on a planar triangulation is fixed by Euler's formula.
Module 1
Visual Sandbox
Draw a map, see the dual graph, watch DSATUR color it, invert a Kempe chain.
Open
Module 2
Configurations
Browse a gallery of reducible configurations with verification labels.
Open
Module 4
MCMC Simulate
Generate random planar triangulations and watch Glauber dynamics find a 4-coloring.
Open
Module 3
Formal Proofs
Read the Coq / Lean artifacts that close the theorem. Pluggable adapter for live provers.
Open