coq-community / fourcolor

Formal proof of the Four Color Theorem [maintainer=@ybertot]

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):
  • Formal Proof—The Four-Color Theorem
  • A computer-checked proof of the Four Color Theorem

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

To instead build and install manually, 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.

fourcolor's Issues

opam package for mathcomp-1.12

I just noticed that pinning the new opam file locally installs a package called coq-mathcomp-fourcolor while the name in the opam-coq-archive has been coq-fourcolor for a long time.

In any event, I just checked and a72978a10c1eace75c2d7bb37b87f6cf7a7a4d69 (master at the time of this writing) is compatible with mathcomp-1.12 and it would be nice to have a point-release fort this in the opam-coq-archive.

CC: @ybertot

README copies too much from odd-order

I think the part "a landmark result of finite group theory" in README.md comes a bit too directly from the odd-order repository.

OPAM package for mathcomp-1.14.0

It would be nice to have OPAM packages of coq-fourcolor for MathComp 1.14.0 (and maybe also 1.13.0), so that I can make another release of the graph theory library.

Please add the opam package to https://github.com/coq/opam-coq-archive

In this way benchmarks like this one (for coq/coq#9905)
https://ci.inria.fr/coq/view/benchmarking/job/benchmark-part-of-the-branch/667/console
can run on fourcolor too.