The 5 Colour Theorem in Isabelle/Isar

Gertrud Bauer and Tobias Nipkow

Based on an inductive definition of triangulations, a theory of undirected planar graphs is developed in Isabelle/HOL. The proof of the 5 colour theorem is discussed in some detail, emphasizing the readability of the computer assisted proofs.



@inproceedings{BauerN:2002,author={Gertrud Bauer and Tobias Nipkow},
title={The 5 Colour Theorem in {Isabelle/Isar}},
booktitle={Theorem Proving in Higher Order Logics},
editor={V. Carre{\~n}o and C. Mu{\~n}oz and S. Tahar},