The Four Colour Theorem: from Guthrie's 1852 conjecture, through Kempe's
refuted proof, to the 1976 computer-assisted proof and Gonthier's 2005 machine-checked Coq
formalization. Node colour is the effective status, the weakest status in a claim's
Depends-On/Assumes closure. Click a claim to trace what it rests on;
click a broken claim to highlight the claims it affects.