Skip to content

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

License

Notifications You must be signed in to change notification settings

Alizter/fourcolor

 
 

Repository files navigation

The Four Color Theorem

Docker CI Contributing Code of Conduct Zulip

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

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.

About

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

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Coq 99.8%
  • Other 0.2%