Au passage, le théorème des quatre couleurs et le programme associé ont été prouvé entièrement dans l'assistant de preuve Coq par Georges Gonthier, un ancien chercheur de l'INRIA maintenant chez Microsoft Research : http://research.microsoft.com/en-us...

Coq est un logiciel libre (LGPL 2.1) : http://coq.inria.fr/what-is-coq