The Four Colour Theorem as a ClaimGraph: from the 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.