Pittsburgh/Wien – Das Problem hat vermutlich auch schon den einen oder anderen Obstverkäufer beschäftigt: Wie ordne ich Orangen oder andere gleich große kugelförmige Früchte an, sodass sie möglichst wenig Raum beanspruchen? Der deutsche Mathematiker und Astronom Johannes Kepler vermutete bereits 1611, dass Stapelungen über einer quadratischen Grundfläche und die über einer dreieckigen (hexagonalen) Anordnung der Kugeln die dichtesten und platzsparendsten sind. (Das ergibt eine Dichte von etwas über 74 Prozent.) Eine zufällige Anordnung der Kugeln hingegen kommt auf nur rund 65 Prozent ausgefüllten Raums.

Den Beweis, warum diese beiden Stapelformen die raumsparendsten sind, blieb Kepler allerdings schuldig. Knapp 400 Jahre lang suchte diese Keplersche Vermutung ihren Meister. 1998 behauptete Thomas Hales, beweisen zu können, dass Kepler richtig lag. Der US-Mathematiker ging für seinen Beweis davon aus, dass die maximale Dichte aller Kugelanordnungen durch die Minimierung einer Funktion mit 150 Variablen gefunden werden kann. Sein Beweis bestand aus knapp 300 Seiten Text und Formeln sowie – eher ungewöhnlich – aus drei Gigabyte Computerprogrammen, Daten und Ergebnissen.

Fast-Bestätigung nach vier Jahren

Ein Herausgeber der "Annals of Mathematics" schlug trotz dieser unkonventionellen Form des Beweises eine Publikation in dieser renommierten Fachzeitschrift vor, aber erst nach einem Begutachtungsverfahren. Der Beweis wurde zwölf Mathematikern vorgelegt, die nach sage und schreibe vier Jahren bekanntgaben, "zu 99 Prozent sicher" zu sein, dass der Beweis korrekt sei. Sie könnten aber nicht die Korrektheit aller am Computer durchgeführten Berechnungen bestätigen.

2003 veröffentlichte Hales einen hundertseitigen Aufsatz als Preprint, der den nicht vom Computer berechneten Teil seines Beweises im Detail beschreibt; 2005 erschien dann der theoretische Teil von Hales' Beweis.

Noch vor Publikation des Preprints, also vor mittlerweile mehr als elf Jahren, kündigte Hales den Beginn eines Projektes namens Flyspeck an, wobei das F, P und K für Formal Proof of Kepler stehen. Flyspeck soll jeden verbliebenen Zweifel an der Gültigkeit des Beweises mittels neuer Software ausräumen: Der formale Beweis wird in der Programmiersprache Objective CAML erstellt, der wiederum von interaktiven Theorembeweisern wie John Harrisons HOL light überprüft werden kann.

Eine Zu(ku)nft ohne Fachgutachter?

Vergangenen Sonntag verkündete Hales, dass die Übertragung des gesamten dichten Beweises in eine computerisierte Form gelungen sei. Und die Software habe bestätigt, dass der Beweis tatsächlich richtig sei. Hales geht davon aus, dass dieser Erfolg weitreichende Folgen für die Mathematik haben könnte: Die Verifikation eines Beweises brauche nun nämlich keine mathematischen Fachgutachter mehr, "ihre Meinung ist nicht mehr länger nötig", ließ er im britischen Wissenschaftsmagazin "New Scientist "verlauten.

Mit der Bestätigung des Beweises sei ihm jedenfalls eine enorme Last von den Schultern gefallen: "Ich fühle mich plötzlich zehn Jahre jünger." Für die Fields-Medaillen, die zu den höchsten Auszeichnungen für Mathematiker zählen, kommt dieser Beweis selbst trotz gefühlter Verjüngung zu spät: Hales ist mit mittlerweile 56 Jahren dafür schlicht zu alt. Der mit umgerechnet rund 10.000 Euro dotierte Preis geht nur an Kandidaten, die jünger als 40 sind. Aber es gibt ja auch noch den Abel-Preis, der zudem auch wesentlich besser dotiert ist: nämlich mit 750.000 Euro.

Der jugendlich aussehende US-Mathematiker indes hat nach eigener Aussage neben der Arbeit an Flyspeck jede Menge Ideen für neue Projekte angehäuft. Und laut "New Scientist" hofft Hales, dass sein nächstes Projekt keine zwanzig Jahre lang dauern wird. (DER STANDARD, 16.8.2014)