|- import_tame_classification /\ the_nonlinear_inequalities
==> the_kepler_conjecture

ist ein mit Hilfe von HOL formalisiertes Theorem, wobei the_kepler_conjecture definiert ist durch

`(!V. packing V
==> (?c. !r. &1 <= r ==> &(CARD(V INTER ball(vec 0,r))) <= pi * r pow 3 / sqrt(&18) + c * r pow 2))`

Die Erklärung dazu findet man hier (meine Übersetzung):
Für jede Packung V (gegeben durch die Mittelpunkte der Kugeln vom Radius 1) gibt es eine den Fehlerterm kontrollierende Konstante c, so dass für jedes r≥1 die Anzahl der Kugelmittelpunkte innerhalb eines kugelförmigen Behälter vom Radius r höchstens pi * r ^ 3 / sqrt (18) plus ein Fehlerterm kleinerer Ordnung ist. Für r gegen unendlich gibt das die Dichte pi / sqrt (18) = 0.74+, was die Dichte des flächenzentrierten kubischen Packung ist.
Pyramid_of_35_spheres_animation
Es geht um das Stapeln von Kugeln. Die flächenzentrierte kubische Packung (Bild oben) hat eine Packungsdichte von \frac{\pi}{\sqrt{18}} =0,74... und die Kepler-Vermutung besagt, dass es keine dichteren Kugelpackungen gibt. Diese Vermutung war 1998 von Thomas Hales bewiesen worden, allerdings benutzte sein Beweis umfangreiche Computerrechnungen und die Gutachter hatten seinerzeit gemeint, sie seien (nur?) zu 99% von der Richtigkeit des Beweises überzeugt. Jedenfalls hatte Hales daraufhin 2003 ein Projekt gestartet, um einen formalen computerlesbaren Beweis zu erstellen, welcher dann von HOL überprüft werden kann. Dieses Projekt ist jetzt zu einem erfolgreichen Abschluß gebracht worden und das Resultat ist der oben zitierte Satz.

Nach beispielsweise dem Satz von Feit-Thompson, dem Vier-Farben-Satz, dem Primzahlsatz und dem Jordanschen Kurvensatz gibt es nun also einen weiteren mit Computer überprüften bekannten mathematischen Satz. Langsam fragt man sich, ob bei Fachzeitschriften in absehbarer Zeit vielleicht Computerverifikationen die Aufgaben der Gutachter übernehmen.

Kommentare (3)

  1. #1 Karl Mistelberger
    14. September 2014

    > Langsam fragt man sich, ob bei Fachzeitschriften in absehbarer Zeit vielleicht Computerverifikationen die Aufgaben der Gutachter übernehmen.

    Ich würde diesen Satz anders formulieren:

    Gutachter werden in absehbarer Zeit zunehmend einen Beweis-Assistenten zur Verifikation verwenden.

    Das trifft die Verhältnisse eher.

  2. […] mehr dazu. Dafür wurde nach Hales computerformalisiertem Beweis der Kepler-Vermutung gefragt (Computerformalisiertes Apfelsinenstapeln). Atiyah hatte sich ja in den 80ern dezidiert kritisch zum Beweis der Klassifikation endlicher […]

  3. […] manche die Gültigkeit des Beweises anzweifelten. 2014 veröffentlichte er dann einen formalen, computerlesbaren und von HOL überprüften Beweis, wonach die Zweifler wohl verstummt […]