Hales: "Walter Raleigh betraute den Mathematiker Thomas Harriot mit der Aufgabe, Kanonenkugeln in verschiedenen Stapeln zu zählen. Harriot entwickelte eine hübsche Formel dafür und dachte begeistert über andere Anwendungen nach. Er schrieb darüber in einem Brief an Johannes Kepler und der griff die Gedanken 1611 in einem Bändchen auf. Darin findet sich die Aussage, die heute als Keplersche Vermutung bekannt ist."

"Es gibt keine Anordnung von Kugeln, die platzsparender ist als die pyramidenförmige Anordnung."

Hales: "Für mich klang das so einfach. Warum konnte die Keplersche Vermutung jahrhundertelang niemand beweisen? Jeder weiß doch, wie man Orangen am besten packt. Zu sehen an jedem Obststand.
Als ich in den späten 80ern merkte, dass es nicht so leicht war, hatte ich bereits Feuer gefangen. Mir wurde klar, dass ich dieses Problem nicht nebenbei lösen konnte. Das war 1994, ich nenne es "Das Jahr der Kugeln", das ich vollkommen der Keplerschen Vermutung widmete. Danach wollte ich entscheiden, wie es weiter geht. Der Durchbruch kam im November. In Princeton hörte ich einen Vortrag des Mathematikers MacPherson über ein geometrisches Problem. Er beschrieb einen Ansatz, dann einen zweiten. Und ich dachte an meine beiden Ansätze für die Keplersche Vermutung. Und dann sagte er."

"Natürlich gibt es für alles mehr als zwei Wege."

Hales: "Es musste einen Mittelweg geben. Ungefähr einen Monat später hatte ich eine unruhige Nacht. Ich dachte die ganze Zeit über die Keplersche Vermutung nach, im Schlaf, im Halbschlaf, im Traum. Am Morgen sagte ich mir, ich werde das Bett nicht verlassen, bis ich weiß, wie ich die beiden Ansätze verbinden kann. Als ich es hatte, sprang ich aus dem Bett, setzte mich an den Rechner und tippte ein paar Berechnungen ein. Ich war mir vollkommen sicher, dass ich die Keplersche Vermutung beweisen würde. Es sollte aber noch vier Jahre dauern, bis ich das Projekt mithilfe des Doktoranden Sam Ferguson abschließen konnte."

McLaughlin: "Tom war sich super sicher. Was mich immer noch verblüfft: Er schrieb schon den Artikel, bevor die Ergebnisse da waren. Ich bin Sean McLaughlin, ich habe als Student und Doktorand mit Tom Hales gearbeitet. Die Frage war nie, ob das Projekt abgeschlossen werden würde. Es war nur eine Frage der Zeit."

Hales: "Wir mussten zeigen, dass alle möglichen Anordnungen schlechter sind als der klassische Kanonenkugel-Stapel. Angenommen, man wirft Orangen durcheinander in eine große Kiste. Wie kann man wissen, ob diese zufällige Anordnung nicht besser ist als die ordentliche pyramidenförmige Anordnung? Mit Computern haben wir ermittelt, dass es etwa 18.000 mögliche Anordnungen gibt. Jede einzelne mussten wir überprüfen. Gegen Ende des Projekts hängte ich die verbliebenen Anordnungen an die Tafel. Einen Zettel nach dem anderen riss ich herunter. Und als ich auch den letzten abriss, war der Beweis vollständig.

McLaughlin: "Er war besessen. Er hatte ja schon locker ein Jahrzehnt damit verbracht."

Hales: "Die Besessenheit wurde stärker, je näher ich der Lösung kam. Am Ende verbrachten wir sehr lange Tage am Computer."

McLaughlin: "Besessene vernachlässigen ihr Leben oder werden zu Arschlöchern oder so. Tom war nie so. Obwohl er super hart arbeitete, war er immer nett und enthusiastisch und er liebte seine Arbeit."

Hales: "Anfang August 1998 gaben wir bekannt, dass wir den Beweis fertig hatten. Ich war ziemlich erschöpft. Als hätte ich einen Marathon absolviert und wäre über die Ziellinie gekrochen. Ich war eher erschöpft als erleichtert. Der Beweis war 300 Seiten lang und ich reichte ihn zur Veröffentlichung ein. Am Anfang dachte ich, das war's für meinen Teil. Aber dann wurde ich nervös. Ich stand als einziger für den Beweis ein. Und er war sehr lang und sehr komplex. Es wurde klar, dass das niemand so schnell würde nachvollziehen und für die Richtigkeit einstehen können."

Boroczky: "Wir waren neugierig. Wir waren skeptisch, aber definitiv neugierig. Ich bin Karoly Boroczky vom Renyi-Institut für Mathematik und der Central European University, beide in Budapest."

Es gibt dieses schöne Zitat von C. A. Rogers: "Viele Mathematiker glauben und alle Physiker wissen, dass die Keplersche Vermutung stimmt."

Boroczky: "Es war also fast undenkbar, dass es eine platzsparendere Anordnung gibt. Aber das zu beweisen, das war seit den 50er-Jahren klar, braucht großartige Ideen und erfordert eine unglaubliche Menge Arbeit. Was ja auch der Fall war. Der Beweis war so kompliziert! Teilweise wegen der intensiven Nutzung von Computern, aber auch die Geometrie war so kompliziert, dass es selbst von uns Gutachtern zu viel verlangt war, alle Details durchzugehen.

Hales: "Zwölf Gutachter sollten die Details prüfen. Ungewöhnlich viele, normal sind ein, zwei oder drei Gutachter. Die Herausgeber wollten jeden Teil des Beweises von mindestens zwei Gutachtern prüfen lassen."

Boroczky: "Wir teilten das Skript auf und jeder versuchte, seinen Teil zu verstehen. Am Renyi-Institut trafen wir uns einmal pro Woche zu einem Seminar. Jemand referierte über einen Teil, den er verstand und wir sezierten diesen Teil dann, um die zugrunde liegenden Ideen, mögliche Lücken und auch schöne Gedanken zu identifizieren. Jemand rannte an die Tafel, zeichnete etwas und erklärte, dass etwas unmöglich war. Dann rannte wieder jemand anders zur Tafel und zeigte, wie es doch ging. Das war sehr lebhaft."

Hales: "Im Sommer darauf hieß es dann, es sehe vielversprechend aus, aber sie bräuchten mehr Zeit. Ein Jahr später: immer noch sehr vielversprechend, aber wir brauchen mehr Zeit. Noch ein Jahr verstrich und ich wurde immer frustrierter. Ich konnte das Ergebnis jahrelanger Arbeit nicht veröffentlichen."

Boroczky: "Wir haben da viel Arbeit reingesteckt, aber es wurde klar, wir können nicht jedes kleine Detail prüfen. Wir waren erschöpft. Am Ende waren wir zu 99 Prozent sicher, dass der Beweis stimmt."

Hales: "Jeff Lagarias, einer der Herausgeber des Beweises hat das hier geschrieben: Manche Gutachter haben Computerexperimente durchgeführt, um bestimmte Teile des Beweises detailliert zu überprüfen. Diese spezifischen Aussagen erwiesen sich nach detaillierter Überprüfung als grundsätzlich korrekt, und zwar in jedem Fall. Das Ergebnis der Begutachtung rief in jedem Gutachter einen hohen Grad der Überzeugung hervor, dass der Ansatz dieses Beweises im wesentlichen korrekt ist. Dieses Statement ist voller Ausflüchte. Sie sind nicht sicher, sondern es gibt einen hohen Überzeugungsgrad. Er ist nicht korrekt, sondern im Wesentlichen korrekt. Die Rede ist nicht vom Beweis, sondern vom Ansatz des Beweises."

Thomas Hales wechselt von der Universität Michigan nach Pittsburgh. Der Beweis wird letztendlich doch in der wichtigsten mathematischen Fachzeitschrift veröffentlicht – trotz Vorbehalten bei Gutachtern und Herausgebern.

Hales: "Das reichte mir nicht. Auch weil ich selbst Restzweifel hatte. Kann ich garantieren, dass in den 300 Seiten komplexer Mathematik und den 40.000 bis 160.000 Zeilen Computercode, je nach Zählweise, keine Fehler sind? Ich kenne meine Grenzen. Ab 2001 dachte ich darüber nach, ob es nicht Wege um die Gutachter herum gibt. Ich fuhr zu einer Konferenz nach Siena in Italien. Da ging es um formale Beweise."

McLaughlin: "Er sagte sich, was soll's, ich mach das jetzt selbst. Und zwar so, dass es nicht angezweifelt werden kann. Also ging er online und suchte nach formaler Beweisführung und sagte: Klar, das ist es."

Hales: "Ich war begeistert. Endlich eine Technik, die Gutachter obsolet machen kann. Schließlich, ich glaube inzwischen waren fünf Jahre um, gab ich bekannt, dass ich einen formalen Beweis des Theorems vorlegen wollte. Das war ein sehr schwieriges Projekt. Einen so großen formalen Beweis hatte in der reinen Mathematik bis dahin noch niemand versucht. Geschätzter Arbeitsaufwand: 20 Jahre. Aber ich war frustriert genug und das der einzige Ausweg aus der Sackgasse."

Avigad: "Tom kennt keine Angst. Allein schon die Keplersche Vermutung zu beweisen und danach dann noch zu sagen, jetzt verifiziere ich das, das ist schon bemerkenswert. Ich bin Jeremy Avigad, Philosophie- und Mathematikprofessor an der Carnegie-Mellon-Universität. Im 17. Jahrhundert entwickelte Leibniz die Universalsprache Characteristica Universalis, um rationale Gedanken auszudrücken. Und Calculus Ratiocinator zur Berechnung von Schlussfolgerungen. Er dachte, man könne das so weit treiben, dass jede Meinungsverschiedenheit statt durch einen Kampf oder Ähnliches entschieden werden könne, indem man sie in symbolischer Form aufschreibt und dann berechnet. Sein berühmter Ausruf war "Calculemus!", lasst uns berechnen. Das ist also die Idee hinter formalen Beweisen: logische und mathematische Argumentation auf eine präzise Rechnung zu reduzieren. Man fängt mit einer sehr kleinen Zahl linguistischer Grundelemente an, Symbolen und grundsätzlichen Regeln um Aussagen zu treffen und abzuleiten und mit ein paar Axiomen. Das ist ein Axiomensystem. Das Bemerkenswerte daran ist, dass man das von einem kleinen Ausgangspunkt zu immer komplizierteren Aussagen hin aufbauen kann. Und so kann ein Computer einem dabei helfen, einen präzisen, detaillierten Beweis auf die Grundprinzipien zurückzuführen.

McLaughlin: "Jemand, der noch nie mit einem formalen Beweisassistenten gearbeitet hat, ist es kaum nachzuvollziehen, wie verrückt die Idee war. Die sind sehr einfach. Man schreibt nicht eine Formel rein und dann beweist das System die für einen. Nein. Es gibt gewisse Automation, die grundlegende Logik überprüfen kann, aber das Level ist im Vergleich zu Toms Beweis ... Es war sehr ambitioniert."

Hales: "Ich weiß, was Angst ist. Als ich hörte, dass die Finanzierung steht, wurde mir schlecht. Dieses Projekt war zu groß für mich. Nie zuvor wollte ich Geld ausschlagen, aber jetzt doch. Ich wollte nicht wieder von vorne anfangen mit dem formalen Beweis. Letztendlich habe ich das Geld akzeptiert, aber wenn ich dieses 20-Jahres-Projekt nicht erst als alter Mann fertig haben wollte, brauchte ich viel Hilfe."

McLaughlin: "Tom erstaunt mich immer wieder. A) beschließt er, den Gutachterprozess zu umgehen und sagt sich: Ich prüfe jetzt jeden Schritt der Keplerschen Vermutung selbst, principia-mathematica-mäßig. Das ist schon sehr kühn. Aber dann sagt er: Oh, das ist eine Menge Arbeit. Mit meinem Budget kann ich keine amerikanischen Programmierer bezahlen. Ich werde nach Vietnam fahren und heuere ein paar Leute an. Und bringe ihnen alles bei. Das ist so stürmisch und voller Tatendrang ... Und er wusste nie, was als Nächstes passieren würde.

Hales: "Ein formaler Beweis ist zeitaufwendig, weil die Technik noch in der Entwicklung steckt. Wir entwickeln die Werkzeuge, während wir sie benutzen. Das Grundsystem war da, aber damit mussten wir dann nicht nur die Keplersche Vermutung beweisen, sondern auch Grundlagen der Geometrie, auf denen wir aufbauen, das gesamte Hintergrundwissen, Topologie, Rechenvorschriften, Kombinatorik, Polyeder-Geometrie: Das mussten wir erst mal alles eingeben."

Avigad: "Wenn man zum Beispiel beweisen will, dass 1+1=2 ist, dann setzt man sich vor das System, in das die Axiome eingebaut sind. Dann muss man die natürlichen Zahlen definieren, die Null definieren, Addition definieren. Dann kann man behaupten, dass 1+1=2 ist und dann wendet man Regeln aus dem System an, um einen Beweis zu konstruieren. Am Ende hat man einen präzisen Beweis der Behauptung und der Computer hat ihn überprüft und sagt: Ja, das ist ein Beweis, dass 1+1 gleich 2 ist. Und dann ist es keine Frage des Glaubens mehr. Es ist direkt von den Grundregeln abgeleitet."

Hales: "In Zukunft kann man vielleicht einfach etwas einscannen und dann wird es formalisiert, aber davon sind wir weit entfernt. Jeder Tag, den man damit verbringt, den Beweis zu vereinfachen, spart zehn Tage Arbeit am Computer beim eigentlichen formalen Beweis. Es zahlt sich aus, den Beweis elegant aufzubauen. Jetzt, wo das Projekt abgeschlossen ist, kann ich die Hauptaussage der Keplerschen Vermutung mit aufgezeichneten Beweisskripten auf meinem Computer innerhalb von 40 Minuten formal beweisen. Darin sind drei rechenintensive Teilaufgaben nicht enthalten. Zwei davon dauern jeweils etwa einen Tag, die letzte braucht 5000 Stunden. Alexey Solovyev, damals Doktorand und dann Postdoc hier an der Uni Pittsburgh, war für diese Berechnung zuständig. Als er fertig war, schickte er mir eine E-Mail. Ich stellte sicher, dass wir nichts übersehen hatten und dann machten wir am 10. August 2014 die offizielle Bekanntgabe. Jetzt habe ich endlich meinen Frieden."

Boroczky: "Diese ganze Geschichte mit der Keplerschen Vermutung ist viel mehr als einfach nur ein Beweis eines berühmten mathematischen Theorems. Was Tom Hales gemacht hat, war vielleicht noch wichtiger als die Keplersche Vermutung zu beweisen. Die Tatsache, dass er seinen sehr, sehr komplizierten Beweis mit Computern verifizieren konnte, zeigt die Macht dieser formalen Beweise."

Avigad: "Das ist ein sensibles Thema. Manche Mathematiker würden zwar sagen, dass das Besondere an der Mathematik ist, wie präzise, exakt, bestimmt und korrekt sie ist. Andere würden eher sagen: Nein, es geht um Konzepte. Wo aber vermutlich jeder zustimmen würde, ist, dass Korrektheit wichtig ist. Und einen solchen Grad an Korrektheit zu erreichen ist bemerkenswert."

Hales: "Ich finde, formale Beweise müssen dringend Mainstream werden in der Mathematik."

Avigad: "Das wird die Mathematik verändern. In Zukunft werden wir erwarten, dass Beweise mit dieser Genauigkeit überprüft werden und wir werden die Mittel dafür haben. Jetzt beweisen wir ein Theorem, versichern uns bei Kollegen, schicken es an die Gutachter. Langfristig wird diese Technik die Art und Weise ändern, wie wir Computer in der Wissenschaft verwenden, nämlich zum Sicherstellen von Korrektheit und um uns beim Ziehen von Schlussfolgerungen zu helfen und die Richtigkeit unserer Argumente zu bestätigen."

Hales: "Um mich zu motivieren, war der Gedanke wichtig, dass diese Technik sehr wertvoll ist - nicht nur für die Keplersche Vermutung, sondern auch für Computersicherheit. Mit formalen Beweisen können wir ohne jeden Zweifel zeigen, dass ein Stück Computercode keinen einzigen Fehler hat. Dass es makellos ist. Fast täglich hören wir von Softwarefehlern, manche harmlos, andere katastrophal. Ich glaube wirklich, dass diese Technik Softwareentwicklung zu etwas viel Wissenschaftlicherem, weniger Fehleranfälligem machen kann."

Avigad: "So kann man garantieren, dass ein System seiner Spezifikation entspricht. Das ist besonders wichtig, wenn dieses System Ihr Auto fährt oder einen Zug steuert oder ein Flugzeug oder ein Space Shuttle fliegt oder in einem Kernreaktor läuft."

Calculemus! Der Mathematiker Thomas Hales und die Kunst, Orangen zu stapeln.

Hales: "Das ist die offizielle Veröffentlichung des ursprünglichen Beweises der Keplerschen Vermutung. Auf das Cover habe ich in Großbuchstaben SUFFERING, Leiden, geschrieben."