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
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
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.
Kommentare (13)