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