Skip to content

Formal proof of the Four Color Theorem

Notifications You must be signed in to change notification settings

herbelin/fourcolor

 
 

Repository files navigation

Build Status

The Four Color Theorem

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.

Installation

If you already have OPAM installed:

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

About

Formal proof of the Four Color Theorem

Resources

Stars

Watchers

Forks

Packages

No packages published

Languages

  • Coq 100.0%