#Optimalität der E8-Kugelpackung – Mathlog

In seiner Broschüre “Vom sechseckigen Schnee” vermutete Johannes Kepler 1611, dass die optimalen Kugelpackungen im 3-dimensionalen Raum die hexagonale und die kubisch-flächenzentrierte Packung mit jeweils Dichte sind. Während die Optimalität der hexagonalen Kreispackung in der 2-dimensionalen Ebene 1940 von László Fejes Tóth bewiesen wurde, blieb die 3-dimensionale Vermutung lange offen und wurde nach verschiedenen lange umstrittenen und letztlich nicht anerkannten Beweisen anderer Mathematiker 1998 von Thomas Hales gelöst mit einem 1953 von Fejes Tóth vorgeschlagenen Ansatz, der den Beweis auf die Betrachtung einer endlichen (aber großen) Zahl von Fällen reduziert hatte. Hales’ Arbeit wurde dann bei den Annals of Mathematics eingereicht, wo ein langer Überprüfungsprozeß begann. Die erste Gruppe, angeführt von Gábor Fejes Tóth – dem Sohn von László Fejes Tóth – gab nach fünf Jahren auf. Alles, was sie geprüft hatten, sei korrekt gewesen. Aber es sei ihnen nicht möglich, jede einzelne Rechnung zu überprüfen. Robert MacPherson als zuständiger Herausgeber verglich ihre Aufgabe mit dem Überprüfen eines Telefonbuchs. Alle Nummern, die sie geprüft hätten, wären korrekt gewesen, und sie hätten wirklich viele Nummern überprüft. Er wollte die Arbeit zunächst mit einer Erklärung veröffentlichen, dass viele, aber nicht alle Teile des Beweises geprüft worden seien. Das stieß auf Widerspruch und so schickte er die Arbeit an einen neuen Gutachter. Der bestätigte, dass die theoretischen Grundlagen korrekt wären und schlug eine Aufteilung der Arbeit vor. Der theoretische Teil wurde in den Annals of Mathematics veröffentlicht, der nicht vollständig überprüfte Teil mit Computerberechnungen in der spezialisierteren Zeitschrift Discrete and Computational Geometry. Zu dieser Zeit hatte Hales bereits den Start eines Gemeinschaftsprojekts angekündigt, das einen vollständig formalisierten Beweis der Kepler-Vermutung erstellen sollte. 2015 war diese Arbeit abgeschlossen, der Beweis in computerisierter Form gelungen und eine Überprüfung durch interaktive Theorembeweiser wie HOL light erfolgt.

Computerüberprüfbare Beweise wurden vor allem von Voevodsky am Institute for Advanced Study propagiert. In einem langen Text auf seiner Webseite erzählte er die Geschichte verschiedener Fehler, die im Laufe der Jahre von ihm und anderen in einigen seiner grundlegenden Arbeiten gefunden worden waren. Auch in ständig zitierten Arbeiten seien Fehler über lange Zeit unentdeckt geblieben. Seine Folgerung daraus war, nur noch computerüberprüfbaren Beweisen zu vertrauen. Er entwickelte eine Bibliothek für das Computerbeweissystem Coq und vor allem entwickelte er neue “univalente” Grundlagen der Mathematik, die für den Zweck computerlesbarer Beweise besser geeignet sein sollten. Statt auf die in der Mathematik überall verwendete Mengenlehre und Kategorientheorie wollte er auf die Typentheorie zurückgreifen, allerdings auf eine sehr spezielle intuitionistische Typentheorie, in der Typen als Homotopietypen topologischer Räume interpretiert werden. Er organisierte dazu ein spezielles Jahr am Institute for Advanced Study, blieb aber doch der alleinige wichtigste Proponent seiner Theorie.

In höheren Dimensionen war die Frage nach optimalen Kugelpackungen völlig offen, es gab aber in sehr speziellen Dimensionen einige Kandidaten, nämlich in Dimension 8 die Gitterpackung zum E8-Gitter und in Dimension 24 die Gitterpackung zum Leech-Gitter.

Nach den langen Diskussionen um den Beweis der (3-dimensionalen) Kepler-Vermutung war man natürlich davon ausgegangen, dass die Beweise der höherdimensionalen Versionen um so schwieriger sein würden. Überraschenderweise hatte die 8-dimensionale Version dann aber einen viel kürzeren Beweis. Eine Arbeit Viazovskas bewies die Optimalität der durch das E8-Gitter gegebenen 8-dimensionalen Kugelpackung auf nur 22 Seiten (von denen ein Teil expositorisch war, so erhielt man nebenbei noch eine Einführung in die Theorie der Modulformen). Der Beweis baute noch auf einer älteren Arbeit von Cohn und Elkies auf, die aber auch nur 25 Seiten lang war. Neben der Kürze überraschte an dem Beweis vor allem die Methodik: wichtigstes Werkzeug im Beweis waren Modulformen, die sonst eigentlich in der Zahlentheorie ein unverzichtbares Werkzeug sind.