1998 bewies Tom Hales zusammen mit seinem Doktoranden Samuel Ferguson, dass Kugeln den dreidimensionalen Raum am dichtesten füllen, wenn man sie stapelt, wie Gemüsehändler es mit Orangen tun -- die neue Lage immer in die Lücken der Lage darunter.
Tom Hales/Wikipedia
Der Beweis beruhte auf einer Umformulierung des Problems in eine Reihe von nichtlinearen Optimierungsproblemen. Deren Lösungen berechneten Hales und Ferguson per Computer. Doch die Programmierung und die Formulierung der Optimierungsaufgaben erfordern viel Programmcode aus menschlicher Hand. Das macht die Sache schwer lesbar: Insgesamt umfasst Hales' und Fergusons Beweis mehr als fünf Aufsätze oder 250 Seiten und mehr als 3 Gigabyte an Programmen und Daten. Die Gutachter der renommierten Annals of Mathematics gaben einst die Überprüfung auf, weil ihnen die Energie ausging, wie sie schrieben.
Das konnte weder die Fachwelt noch Hales selbst befriedigen. Der startete daher das Projekt Flyspeck, zu deutsch: Fliegendreck (im Sinne von »sehr genaue Arbeit«; das Wort ist Ergebnis einer Matching-Suche im Wörterbuch mit dem Muster F.*P.*K für "Formal Proof of Kepler"). Ursprünglich sollte das Projekt noch mehrere Jahre dauern. Doch jetzt konnte es durch die Zusammenarbeit eines großen Teams überraschend schnell abgeschlossen werden: Am 10.8. verkündete Hales stolz, dass der Fliegendreck fertig ist.
Der formale Beweis der Kepler-Vermutung, geschrieben in für die Beweiser-Software Isabelle und HOL Light, lässt sich nun (zumindest zum Teil) herunterladen und auf dem heimischen Rechner überprüfen. Allerdings rechnete selbst Hales Computernetzwerk mit 32 Prozessoren noch 156,25 Stunden an der Überprüfung. (Und man muss hinterher glauben, dass der Code auch das beweist, was er beweisen soll.)
Andreas Loos