Das Vierfarbenproblem

Zusammenfassung

Im Jahre 1976 verkündeten Renneth Appel und Wolfgang Haken, zwei Mathematiker an der Universität von Illinois, daß sie ein hundert Jahre altes Problem, das mit der Färbung von Landkarten zusammenhing, gelöst hätten. Es sei ihnen gelungen, so sagten sie, die Vierfarbenvermutung zu beweisen. Dies war an sich bereits eine sensationelle Nachricht, denn das Vierfarbenproblem war nach der Fermatschen Vermutung (vgl. Rapitel 8) wahrscheinlich das berühmteste ungelöste Problem der gesamten Mathematik. Für die Mathematiker bestand der wahrlich dramatische Aspekt dieser Nachricht jedoch in der Art und Weise, wie der Beweis erzielt worden war. Umfangreiche und entscheidende Teile der Beweisführung wurden nämlich von einem Computer ausgeführt, wobei die für das Programm maßgeblichen Überlegungen ihrerseits ebenfalls auf computer-erzeugten Daten beruhten. Der erforderliche Rechenaufwand war so groß, daß kein Mathematiker je hoffen konnte, alle Schritte per Hand zu überprüfen. Damit hatte sich der Begriff eines «mathematischen Beweises» plötzlich von Grund auf gewandelt. Eine Befürchtung, die seit dem Aufkommen der ersten elektronischen Computer in den fünfziger Jahren bestanden hatte, war schließlich Wirklichkeit geworden: Der Computer hatte den Mathematiker bei einem Teil der Ronstruktion eines echten mathematischen Beweises abgelöst.