TetraChroma Lab

About TetraChroma Lab

An interactive companion to the Four-Color Theorem — visual, computational, and formal.

The theorem

Every planar graph admits a proper coloring with at most four colors. Equivalently: any geographical map can be colored with four colors so that no two regions sharing a border get the same color.

A short timeline

  • 1852Francis Guthrie notices that 4 colors suffice to color the counties of England.
  • 1879Alfred Kempe publishes a 'proof' — later found to be flawed by Heawood.
  • 1890Heawood's correction yields the (much easier) 5-color theorem.
  • 1969Heesch develops the discharging method and the concept of reducible configurations.
  • 1976Appel & Haken close the theorem using a computer-assisted exhaustion of 1,482 configurations.
  • 1996Robertson, Sanders, Seymour, Thomas simplify the proof to 633 configurations.
  • 2005Gonthier formalizes the entire proof in Coq, ending the trust debate.

Verification labels

Every configuration in the lab carries a Strict Verification Label of the form [Provenance]-[Category]-[SubID]-[State].

  • AH — Appel–Haken (1976) · RSST — Robertson, Sanders, Seymour, Thomas (1996) · EXP — experimental · USR — user-defined
  • U — unavoidable · R — reducible · B — both · S — sandbox
  • COMP-1976, COQ-2005, LEAN-VERIFIED, UNVERIFIED

Architecture & extensibility

  • TanStack Start (React 19) on the edge; pure-TS graph kernels.
  • MCMC engine in a Web Worker — drop-in replacement with a Rust→Wasm build is supported.
  • Configuration dataset is a DatasetSource — bundled stand-in today, full RSST 633 / Appel-Haken 1,482 when imported.
  • Formal proofs go through a ProverAdapter interface; the local cache adapter ships, a remote Coq/Lean adapter is one file away.

References

  • K. Appel, W. Haken. Every planar map is four colorable. Bull. AMS, 1976.
  • N. Robertson, D. Sanders, P. Seymour, R. Thomas. The Four-Colour Theorem. J. Combin. Theory B, 1997.
  • G. Gonthier. A computer-checked proof of the Four-Color Theorem. Microsoft Research, 2005.
  • D. Heesch. Untersuchungen zum Vierfarbenproblem. Bibliographisches Institut, 1969.
SOCR logo

About SOCR

TetraChroma Lab is developed by the Statistics Online Computational Resource (SOCR) at the University of Michigan. SOCR designs interactive tools, open educational materials, and computational libraries for probability, statistics, data science, and AI — used in classrooms and research worldwide. This app is part of the SOCR GAIM (Generative AI & Mathematics) initiative.