The repository contains a mechanization of the Four Color Theorem(Appel & Haken, 1976), a landmark result of graph theory.

The formal proof is based on the Mathematical Components library for the Coq proof assistant.

If you already have OPAM installed:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-fourcolor