"Flyspeck"-Projekt

von George Szpiro, NZZ vom 16. 2. 2003

20 Jahre für einen Beweis des Beweises
Der Mathematiker Thomas Hales ist eigentlich kein Mensch grosser Worte. Aber in den E-Mails, die er am 8. August 1998 an seine Kollegen in aller Welt verschickte, war seine Bescheidenheit von vornherein vergeblich: Die 400 Jahre alte Keplersche Vermutung habe er gelöst, schrieb er in seiner Mitteilung. Diese Vermutung besagt, dass die dichteste Art, Kugeln aufzustapeln, darin besteht, sie pyramidenförmig übereinander zu placieren - also genau so, wie man Orangen aufeinander stapelt. Hales hatte die Vermutung mit Hilfe eines massiven Einsatzes von Computern bestätigt. Doch auch viereinhalb Jahre später ist der Beweis immer noch in keiner Fachzeitschrift veröffentlicht worden. Wieso?
Bevor eine wissenschaftliche Arbeit in gedruckter Fassung erscheinen kann, muss sie einen rigorosen Prozess der Begutachtung durchlaufen. Nach Bekanntwerden von Hales' Mammutleistung wollte Robert MacPherson, Professor am Institute of Advanced Studies in Princeton und einer der sechs Redaktoren der "Annals of Mathematics", dem jungen Professor die Veröffentlichung in der wohl renommiertesten mathematischen Zeitschrift vorschlagen. Ganz wohl war ihm nicht dabei, denn es handelte sich ja um einen der von vielen Mathematikern verpönten Computerbeweise. Also holte er zuerst die Meinung seiner fünf Kollegen im Redaktionsstab ein. Diese meinten, dass ein Computerbeweis im Prinzip akzeptabel sei, doch beharrten alle Seiten darauf - Thomas Hales inbegriffen -, dass der Begutachtungsprozess den allerhöchsten Ansprüchen genügen müsse.

Vier Jahre lang gerechnet
Daraufhin beauftragte MacPherson nicht weniger als ein Dutzend Mathematiker mit der Aufgabe, den Beweis minuziös durchzuarbeiten und auf Schwachstellen zu prüfen. Geleitet wurde das Projekt von dem ungarischen Mathematiker Gabor Fejes Toth, dem Sohn des legendären Geometrieprofessors Laszlo Fejes Toth, der schon 1965 vorausgesagt hatte, dass ein Beweis der Keplerschen Vermutung eines Tages mit Hilfe eines Computers möglich sein würde. Die Gutachter arbeiteten vier Jahre lang an dem Beweis. Eine Inspektion der Computercodes, der Berechnungen und des Outputs war auf jeden Fall illusorisch, und die Referees beschränkten sich deshalb auf eine eingehende Rekonstruktion der Gedankengänge, auf Konsistenzprüfungen sowie auf die logische Überprüfung aller Schritte und Folgerungen. Ganzjährige Seminare wurden veranstaltet, in denen die Teilnehmer einzelne Teile des Beweises unter die Lupe nahmen. Wie MacPherson einst in einem Interview erklärte, war er zutiefst beeindruckt, wie selbstlos alle diese Leute an die undankbare Arbeit gingen, denn für die Überprüfung eines Manuskripts war und ist kein Ruhm zu erringen. Aber der Erfolg blieb aus. Nach mehrjähriger intensiver Arbeit fasste Fejes Toth in einem Brief nach Princeton die Begutachtung in den Worten zusammen, dass er von der Richtigkeit des Beweises zwar zu 99 Prozent überzeugt sei, dass sein Team aber nicht in der Lage gewesen sei, den Beweis mit allerletzter Sicherheit zu zertifizieren. MacPherson schrieb umgehend an Hales. "Die Nachrichten der Referees sind schlecht. Sie waren nicht in der Lage, die Richtigkeit des Beweises festzustellen, und werden auch in Zukunft nicht dazu in der Lage sein. Sie sind mit ihrer Energie am Ende." Vielleicht, so fügte er noch hinzu, wären die Begutachter zu einer definitiven Antwort gekommen, wenn das Manuskript von Anfang an etwas klarer geschrieben worden wäre.
In diesem Satz schwang ein Ton der Ungehaltenheit mit. Der Beweis, den Hales und sein Doktorand und Mitarbeiter Tom Ferguson abgeliefert hatten, war nämlich nicht gerade eine stilistisch ausgefeilte Arbeit. Stattdessen bestand er aus einer Reihe von "Laborberichten", die Hales und Ferguson jedes Mal, wenn der Computer einen Teil des Beweises beendet hatte, ausfüllten. Lesbarkeit und Verständlichkeit des Manuskripts litten sehr unter diesem für Mathematiker ungewohnten Vorgehen. Ursprünglich hatte MacPherson die Autoren ersucht, das Manuskript vor der Weiterleitung an die Referees zu redigieren, aber die beiden, die viele Jahre mit der Keplerschen Vermutung zugebracht hatten, hatten die Nase voll. Zu der langweiligen Überarbeitung der 250 Seiten hatten sie einfach keine Lust mehr. Stattdessen machte sich Hales an die Lösung der ebenfalls jahrhundertealten Honigwaben-Vermutung (NZZaS vom 14. April 2002), und Ferguson heuerte beim amerikanischen Verteidigungsministerium an. Dennoch wird der Beweis der Keplerschen Vermutung in den kommenden Monaten in den "Annals" erscheinen, allerdings versehen mit einem Vorwort, in der die Redaktoren darauf hinweisen, dass sie dessen Richtigkeit nicht mit allerletzter Sicherheit verifizieren konnten.

Publikation mit Warnung
Aber Hales will sich damit nicht zufriedengeben. Dass seine Arbeit mit einem Warnschild versehen wird - quasi "Benutzung auf eigene Gefahr" -, lässt ihn nicht ruhen. Am 1. Januar 2003 startete er ein Projekt, mit dem seinem Beweis doch noch ein Gütesiegel verliehen werden soll. In dem von ihm "Flyspeck" oder FPK (Formal Proof of Kepler) getauften Projekt soll mit Hilfe von Computern jeder einzelne Schritt seines Beweises kontrolliert werden. Keine Vorbildung der Referees wird vorausgesetzt, keine Annahmen werden gemacht. Computer werden automatisch und ohne menschliches Eingreifen jede einzelne Behauptung und jede auch noch so triviale Folgerung auf ihren Wahrheitsgehalt überprüfen, um sicherzustellen, dass keine einzige Lücke offen ist.
Erst dann wird Hales' Beweis der Keplerschen Vermutung als richtig gelten. Schnell wird das nicht geschehen: Das Projekt ist auf zwanzig Jahre angesetzt und soll in Zusammenarbeit mit Freiwilligen aus aller Welt vollbracht werden, die sich mit einer eigens entwickelten Computersprache bekannt machen und ihre PC-Zeit zur Verfügung stellen müssen.

Von George Szpiro erscheint Ende Februar im Verlag John Wiley & Sons, New York, das Buch " Kepler's Conjecture: How Some of the Greatest Minds in History Helped Solve One of the Oldest Math Problems in the World".