Text
Thomas Reintjes

Bild
Sandra Teschow

„Ich fühlte mich, als hätte ich einen Marathon absolviert und wäre über die Ziellinie gekrochen“, sagt Thomas Hales. Er redet nicht von Extremsport seine Disziplin ist die Mathematik. Ein mathematisches Problem hat es ihm besonders angetan: die Keplersche Vermutung. Er fragt sich, wieso seit Keplers Lebzeiten, also seit rund 400 Jahren, niemand beweisen konnte, dass man Kugeln nicht dichter packen kann als in der kubisch-flächenzentrierten Packung. „Das Problem schien einfach“, sagt Thomas Hales. Schließlich weiß jeder Obsthändler, dass man Orangen oder Äpfel am besten in dieser Anordnung stapelt, die eine Pyramidenform ergibt. „Als ich merkte, dass es nicht einfach war, war es zu spät“, so Hales. Das war in den 80ern. Über die Jahre, in denen er nebenbei an einem Beweis herum denkt, entwickelt sich eine Besessenheit. 1994 entscheidet er, sich Vollzeit der Keplerschen Vermutung zu widmen. Er findet schließlich einen Ansatz für einen Beweis. Der erfordert aber das Berechnen aller denkbaren Anordnungen von Kugeln. Es kostet ihn, einen Studenten und ihre Computer vier Jahre. Im August 1998 ist der Beweis endlich fertig, der Marathon absolviert.

Dann passieren ein paar Merkwürdigkeiten. Statt Rückmeldungen von Reviewern bekommt Thomas Hales eine Einladung nach Princeton. Dort soll er in einer Reihe von Vorträgen seinen Beweis erklären. Irgendwo im Publikum sitzen die Gutachter. Später stellt sich heraus, dass nicht wie üblich drei oder vier Gutachter den Beweis prüfen, sondern etwa ein Dutzend. Thomas Hales wird klar: Niemand kann seinen Beweis durchschauen. Er ist 300 Seiten lang, plus einige Gigabyte an Daten. Jahr um Jahr wird er vertröstet, es frustriert ihn mehr und mehr, bis man ihm 2003 mitteilt: Die Gutachter sind erschöpft, aber zu 99 Prozent überzeugt, dass der Beweis stimmt. Eine Katastrophe.

Thomas Hales will Gewissheit, dass sein Beweis zu 100 Prozent korrekt ist. „Ich kenne meine Grenzen“, sagt er, wissend, dass sich durchaus ein Fehler eingeschlichen haben könnte, der die Keplersche Vermutung auch weiterhin eine Vermutung bleiben lässt. Der traditionelle Peer-Review-Prozess war offenbar daran gescheitert, seine Ergebnisse zu verifizieren oder zu falsifizieren. Seine Konsequenz: „Ich habe nach Wegen gesucht, die Gutachter zu umgehen“.

Er findet eine Methode namens Formal Proof, formelle Beweise. Computer überprüfen dabei einen Beweis Schritt für Schritt und führen auch die kompliziertesten Formeln auf die grundlegenden Regeln der Mathematik zurück. Das klingt nach mehr Automation, als tatsächlich dahinter steckt. Hales schätzt, dass es 20 Mannjahre dauert, seinen Beweis in ein Formal-Proof-System zu füttern. Nochmal Jahrzehnte mit der Keplerschen Vermutung verbringen? Das ist selbst für den Marathon-Mathematiker zu viel. Er holt sich Hilfe, unter anderem bei Wissenschaftlern in München. Am 10. August 2014, 16 Jahre nach seinem schriftlichen Beweis, liefert ein Computer nach 5000 Stunden Rechenarbeit die Erlösung: Thomas Hales hat – zusammen mit mehr als 20 Kollegen – zweifelsfrei bewiesen, dass die Keplersche Vermutung stimmt.

Erschienen am 18. Mai 2018

Text
Thomas Reintjes

Bild
Sandra Teschow