Das Vierfarbenproblem

Die „Vier-Farben-Vermutung“ oder das „Vier-Farben-Problem“ wurde erstmals 1852 von dem südafrikanischen Mathematiker Francis Guthrie (1831-1899) formuliert, als er in einer Karte die Grafschaften von England so einfärben wollte, dass keine zwei angrenzenden Flächen die gleiche Farbe erhielten. Es war offensichtlich, dass drei Farben dafür nicht ausreichten. Andererseits konnte er kein Beispiel konstruieren, bei dem man fünf Farben benötigte. Aber ist das tatsächlich immer so, das heisst, lässt sich mathematisch beweisen, dass vier Farben ausreichen, gleichgültig welche Formen und Größen die Flächen haben?

Obwohl sich viele Mathematiker an dem Problem versuchten, dauerte es 124 Jahre bis 1976 von den amerikanischen Mathematikern Kenneth Appel und Wolfgang Haken mit Hilfe eines Computers ein Beweis gefunden wurde, der die Anzahl der problematischen Fälle von unendlich auf letztlich 1.476 reduzierte. Und erst 2004 konnte mit Hilfe eines Softwareprogrammes namens „Coq“ ein formaler Beweis konstruiert werden, der eine Überprüfung verbleidender Einzelfälle überflüssig machte.

Der Vier-Farben-Satz war das erste große mathematische Problem, das mit Hilfe von Computern gelöst wurde. Allerdings wurde der Beweis von einigen Mathematikern nicht anerkannt, da er nicht direkt durch einen Menschen nachvollzogen werden kann und man sich auf die Korrektheit des Compilers und der Hardware verlassen muss. Auch die mathematische Eleganz des Beweises wurde kritisiert: Ein guter Beweis lese sich wie ein Gedicht – dieser sehe aus wie ein Telefonbuch.