Der Computerbeweis des 4-Farben-Problems führte nach seiner Veröffentlichung 1977 zu großen Diskussionen. Es ging um die Frage, ob ein Computerbeweis, der so umfangreich ist, daß kein Mensch seine Richtigkeit überprüfen kann, den Ansprüchen an einen mathematischen Beweis genügt. Befördert wurden diese Diskussionen noch durch einige kleinere Fehler in Details, die in den nächsten Jahren gefunden wurden, sich aber alle leicht korrigieren ließen. (1982 hatte Ulrich Schmidt in seiner Diplomarbeit 40% des Beweises von Hand überprüft, dabei 15 Fehler gefunden, von denen aber nur einer wirklich eine inhaltliche Korrektur des Beweises nötig machte.)
1996 fanden Robertson, Sanders, Seymour, Thomas einen Beweis mit ‘nur’ 633 unvermeidbaren Strukturen. Auch diese können bisher nur von einem Computer geprüft werden.
Heute gelten Computerbeweise zwar als allgemein akzeptiert, die meisten Mathematiker bevorzugen aber schon Beweise, deren Richtigkeit man selbst nachprüfen kann.
Ein relativ aktuelles Beispiel ist Hales’ Beweis der Kepler-Vermutung: die effektivste Packung von Kugeln im 3-dimensionalen Raum (d.h. mit geringstmöglichem freigelassenem Volumen) entsteht durch Anordnung der Kugeln in einem 6-Eck-Muster. (Annals of Mathematics (2) 162, No. 3, 1065-1185, 2005)
Ein anderes Beispiel eines mit Computerhilfe bewiesenen Satzes ist der Satz von Gabai-Meyerhoff-Thurston, daß homotopie-hyperbolische 3-Mannigfaltigkeiten hyperbolisch sind. (Annals of Mathematics (2) 157, No. 2, 335-431, 2003) Dieser Satz folgt aber inzwischen auch aus Perelman’s Arbeiten über Geometrisierung, so daß man ihn jetzt also auch ohne Computer beweisen kann.
Es gibt nach wie vor viele Graphentheoretiker, die versuchen, einen ‘verstehbaren’ Beweis des 4-Farben-Satzes zu finden.
Diverse Graphfärbungsprogramme findet man übrigens bei Joseph Culberson.
Nachtrag: Ein Souvenir, das mir von Herrn Grassmann aus Mühlenbeck zugeschickt wurde:
Teil 1, Teil 2, Teil 3, Teil 4, Teil 5, Teil 6, Teil 7 , Teil 8, Teil 9 , Teil 10 ,Teil 11, Teil 12, Teil 13, Teil 14, Teil 15
Neil Robertson, Daniel P. Sanders, Paul Seymour, Robin Thomas (1996). A new proof of the four-colour theorem Electronic Research Announcements of the American Mathematical Society, 02 (01), 17-26 DOI: 10.1090/S1079-6762-96-00003-0
Kommentare (5)