Awesome
<!--- This file was generated from `meta.yml`, please do not edit manually. Follow the instructions on https://github.com/coq-community/templates to regenerate. --->The Four Color Theorem
This library contains a formal proof of the Four Color Theorem in Coq, along with the theories needed to support stating and then proving the Theorem. This includes an axiomatization of the setoid of classical real numbers, basic plane topology definitions, and a theory of combinatorial hypermaps.
Meta
- Author(s):
- Georges Gonthier (initial)
- Coq-community maintainer(s):
- Yves Bertot (@ybertot)
- License: CeCILL-B
- Compatible Coq versions: 8.16 or later
- Additional dependencies:
- MathComp ssreflect 2.1.0 or later
- MathComp algebra
- Hierarchy Builder 1.5.0 or later
- Coq namespace:
fourcolor - Related publication(s):
Building and installation instructions
The easiest way to install the latest released version of The Four Color Theorem is via opam:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-fourcolor
If you are only interested in the formalization of real numbers, you can install it separately:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-fourcolor-reals
To instead build and install the whole project manually from the repository, do:
git clone https://github.com/coq-community/fourcolor.git
cd fourcolor
make # or make -j <number-of-cores-on-your-machine>
make install
Documentation
The Four Color Theorem (Appel & Haken, 1976) is a landmark result of graph theory.
The formal proof is based on the Mathematical Components library.