Beweis
Der Vierfarbensatz gilt seit 1976 als bewiesen. Allerdings ist der Beweis - auch unter Mathematikern - umstritten da er nur mit Computerhilfe zustande kam. Im Beweis sind später einige Fehler aufgetaucht die eine Anpassung des Beweises nötig machten. Inzwischen gibt es einen modifizierten Beweis von Georges Gonthier und Benjamin Werner der mit Hilfe des Beweisassistenten Coq konstruiert wurde. Seitdem wird der Beweis von einem größeren Teil der Mathematiker anerkannt. Viele sind aber nach wie vor skeptisch und bemängeln die fehlende Verständlichkeit und Eleganz des Compuberbeweises.
Tatsächlich gibt es einiges was den Computerbeweis des Vierfarbensatzes "abwertet". Als Kinder fanden wir es früher lustig auf die Frage "Wissen Sie wie spät es ist" mit einem schlichten "Ja" zu antworten. Es wurde ja nur gefragt ob wir die Zeit wissen, wir wurden aber nicht gebeten die aktuelle Zeit mitzuteilen. Ähnlich verhält es sich beim Computerbeweis des Vierfarbensatzes. Auf die Frage "Kann eine beliebige Landkarte mit vier Farben so eingefärbt werden dass keine zwei angrenzenden Länder die gleiche Farbe bekommen?" können wir - dank des Computerbeweises - nun mit "ja" antworten. Wir können aber die Karte - trotz des Computerbeweises - nicht notwendigerweise mit vier Farben zeichnen. Tatsächlich können wir dies offensichtlich genauso gut oder schlecht wie vor dem Beweis. Aus einem verständlichen computerfreier Beweis könnte man dagegen mit einiger Wahrscheinlichkeit auch eine praktikable Methode zum Färben der Landkarten ableiten.
Aktuell läßt sich das Färben der Landkarte am Computer wohl am einfachsten mit einem Backtracking-Algorithmus (Versuch-und-Irrtum-Prinzip / trial and error) durchführen. Dabei werden nacheinander alle Länder mit einer Farbe gefärbt, anschließend wird getestet ob die Färbung die Vierfarben-Regel verletzt. Ist dies der Fall wird mit einer anderen Farbe fortgefahren, ist alles ok wird mit dem nächsten Land genauso verfahren. Führen bei einem Land alle 4 Färbungen nicht zum Erfolg bekommt das davor gefärbte Land eine neue Farbe. Der Algorithmus endet entweder damit dass alle Länder gefärbt sind oder er bricht ab weil keine Färbung der Landkarte mit 4 Farben möglich ist. Mit Hilfe der vielfältigen Erkenntnisse aus der Vierfarbenforschung und der Graphentheorie ist es möglich den Backtracking-Algorithmus deutlich effektiver zu programmieren, wobei das Grundprinzip (trail and error) sich jedoch nicht ändert. Der Vorteil des Computerbeweises von 1976 liegt beim Backtracking-Algorithmus vor allem darin, dass man vorher weiss dass der Algorithmus nicht abbricht sondern eine entsprechend gefärbte Landkarte liefert.