Computerformalisiertes Apfelsinenstapeln

|- 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.

Es geht um das Stapeln von Kugeln. Die flächenzentrierte kubische Packung (Bild oben) hat eine Packungsdichte von 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.