Ein Graph \(G := (V, E)\) besteht aus einer endlichen Menge Knoten \(V\) und einer Menge Kanten \(E\) mit je 2 Elementen, welche einzelne Kanten bilden.
Der Vier-Farben-Satz besagt, dass vier Farben immer genügen, um eine beliebige Landkarte so einzufärben, dass keine zwei angrenzenden Länder die gleiche Farbe haben. Damit der Vier-Farben-Satz gilt, müssen die folgenden Voraussetzungen erfüllt sein.
In der Abbildung 1 ist die Fläche A nicht zusammenhängend, deshalb braucht man dafür fünf Farben. Hier sieht man, dass bei der Lösung in der graphischen Darstellung, sich die zwei "problematischen" Verbindungen (rot makiert) überkreuzen.
Die zweite Regel des Vier-Farben-Satz besagt, dass Flächen, die nur über ihre Ecken miteinander verbunden sind, die gleiche Farbe haben können. Falls dies nicht gelten würde, müssten wir wie in Abbildung 2 eine Kuchenform mit so vielen Farben einfärben, wie Kuchenstücke.
Stundenplanprobleme lassen sich als Graphenfärbungsprobleme formulieren: Die Knoten des Graphen sind dabei die zu platzierenden Veranstaltungen, und eine Kante wird zwischen zwei Veranstaltungen eingefügt, die nicht gleichzeitig stattfinden können. In der Schule wären das z.B. Stunden, die von demselben Lehrer unterrichtet werden, sowie Stunden in derselben Klasse. Die möglichen Farben entsprechen den zuteilbaren Zeitfenstern.
In gleicher Weise können beispielsweise Register-Zuweisungsprobleme in Prozessoren, Bandbreiten-Zuweisungsprobleme und auch viele Probleme aus der Mathematik als Graphenfärbungsprobleme formuliert werden.
Um mit unserem Handy eine Nachricht senden zu können, benötigen wir eine aktive Verbindung zu einem umliegenden Antennenmast. Dieser sendet auf einer gewissen Frequenz in einem Gebiet, welches wir uns als Kreis um den Mast vorstellen können (siehe Abbildung 3). Da in einer grösseren Innenstadt alle 500 Meter ein weiterer Antennenmast benötigt wird, um Funklöcher vermeiden zu können, kommt es zwingend zu Überschneidungen. Das Problem bei solchen Überschneidungen ist, falls die beiden Antennenmasten auf gleicher Frequenz senden, führt es bei dem Nutzer zu Interferenzen, welche bei einem Telefonat immer wieder zu Unterbrechungen führen. Um genau diese Interferenzen zu vermeiden, werden den Masten unterschiedliche Frequenzen gegeben. Auch hier hilft uns der Vier-Farben-Satz. Denn damit wissen wir dass nicht mehr als vier verschiedene Frequenzen benötigen.
Stellen wir uns vor, die Masten sind die Knoten und die Überlappungen der Gebiete sind die Kanten, welche die Knoten miteinander verbinden. Die Anzahl Frequenzen werden als verschiedene Farben wiedergegeben. Nun kann der Vier-Farben-Satz angewendet werden. Da dieser besagt, dass die Knoten mit maximal vier Farben einfärbbar sind, lassen sich unseren Masten jeweils eine von maximal vier Frequenzen zuordnen.
So schön diese Theorie auch funktioniert, hat sich in der Praxis gezeigt, dass es nicht so einfach anwendbar ist. Die Realität zeigt, dass nicht nur gleiche Frequenzen zu Interferenzen führen, sondern auch ähnliche Frequenzen. Um dieses Problem zu beheben, müsste eine Separationsbedingung eingeführt werden, welche dem benachbarten Mast eine ähnliche Frequenz verbietet, was durch den Vier-Farben-Satz nicht mehr abgedeckt wird.
Der Vier-Farben-Satz wurde erstmals im Jahre 1852 von Francis Gutrie als Vermutung aufgestellt, als er die Gebietseinheiten in England einfärben wollte. In einem Brief vom Londoner Mathematikprofessor Augustus De Morgan vom 23. Oktober 1852 an den irischen Kollegen William Rowan Hamilton wurde die Vermutung erstmals diskutiert und veröffentlicht.
Schnell wurden erste vermeintliche Beweise für den Vier-Farben-Satz aufgestellt, diese wurden aber alle widerlegt. 1890 entstand aus einer Widerlegung der Beweis für den Fünf-Farben-Satz, womit eine obere Grenze für die Färbung eines Graphen zum ersten Mal fehlerfrei bewiesen wurde.
Mit Hilfe der Technologie konnte in den 1960er und 1970er Jahren ein erster Entwurf eines Computerbeweises entwickelt werden. Dieser wurde stetig optimiert und prüfte 633 Färbungsfälle, wodurch man den Vier-Farben-Satz “beweisen” konnte.
2005, wurde der Satz von Georges Gunthier und Benjamin Werner formal bewiesen.
Der Vier-Farben-Satz war das erste grosse mathematische Problem, das mit Hilfe von Computern gelöst wurde. Deshalb wurde der Beweis von einigen Mathematikern nicht anerkannt, da er nicht direkt durch einen Menschen nachvollzogen werden kann. Auch der Mangel an mathematischer Eleganz des Beweises wurde kritisiert.