Beweis der Keplerschen Vermutung

Wu-Yi Hsiang versuchte ab etwa 1990 die Keplersche Vermutung zu beweisen. Seine Lösung wurde von Hales und anderen heftig kritisiert. Um 1997 lehnten die sich damit beschäftigenden Mathematiker den Beweisversuch im überwiegenden Konsens als unzureichend ab, wogegen Hsiang von der Gültigkeit überzeugt blieb.

Der daraufhin von Thomas C. Hales und seinem Doktorand Samuel P. Ferguson vorgestellte Beweis umfasste eine extrem große Datenmenge. Die Gutachter um Gábor Fejes Tóth sahen sich nach eigenen Worten „zu 99 Prozent“ von der Richtigkeit des Beweises überzeugt, gaben aber nach Jahren intensiver Arbeit erschöpft auf. Der Beweis folgt einem von László Fejes Tóth vorgeschlagenen Weg über Lineare Programmierung. Die Gutachter beanstandeten auch teilweise nur skizzenhafte Beweis-Dokumente in Preprint-Form im Umfang von etwa 200 Seiten, ohne die Computerausdrucke. Hales und Ferguson gaben an, nach der jahrelangen Arbeit am Beweis zu ausgelaugt zu sein, um dies auf eine polierte Form zu bringen, was Hales aber nach dem Verdikt der Gutachter nachholte. Die Annals of Mathematics veröffentlichten den Beweis trotz des Eingeständnisses des Scheiterns der Gutachter 2005. Die Herausgeber der Annals schrieben, dass sie den menschlichen Teil Computer-unterstützter Beweise besonders wichtiger mathematischer Sätze künftig abdrucken, auch wenn der Computer-Code (den die Annals auf ihrer Website veröffentlichten) nicht restlos zufriedenstellend überprüft war. Der Annals-of-Mathematics-Aufsatz war eine Übersicht. Eine vollständigere Veröffentlichung, die die Preprints von 1998 überarbeitete, erfolgte 2006 in einem Sonderheft der Zeitschrift Discrete & Computational Geometry, in dem die Herausgeber Gabor Fejes Toth und Jeffrey Lagarias den Peer-Reviewern danken und diese teilweise namentlich aufführen, was unüblich ist, da Peer Reviewer an sich anonym bleiben.

Damit erhielten Diskussionen zur Frage, inwieweit auf Computer angewiesene Beweise als akzeptabel gelten, Auftrieb. Ähnliche Diskussionen wurden seit dem Beweis des Vier-Farben-Satzes durch Kenneth Appel und Wolfgang Haken im Jahre 1977 geführt.

Hales sucht daher Wege, um allgemein in Bereichen, in denen Computer zur Überprüfung allzu vieler Zwischenschritte notwendig sind, streng mathematische Beweise zu erstellen. Im Project FlysPecK formalisierte er seinen Beweis der Vermutung Keplers, damit ihn automatische Theorembeweiser wie B. John Harrisons HOL light prüfen können. Derartige Prüfungen sollen künftig – wie zum Beispiel im SETI@home-Projekt – über verteiltes Rechnen im Web erfolgen.

Im August 2014 verkündete Hales, die Übertragung des Beweises in computerisierte Form sei beendet, die Software habe die Richtigkeit des Beweises bestätigt.

Beweis der Honigwaben-Vermutung

Hales bewies auch einige andere berühmte Vermutungen der Geometrie. 1999 bewies Hales die Honigwaben-Vermutung (Honeycomb Conjecture), die auf die Antike zurückgeht und vermutet, dass bei einer Aufteilung der Ebene in Gebiete jeweils gleichen Flächeninhalts der Gesamtumfang der Ränder mindestens dem der regelmäßigen hexagonalen Honigwaben-Aufteilung entspricht.

Beweis der Dodekaeder-Vermutung

Mit seinem Studenten Sean McLaughlin bewies er 1998 die Dodekaeder-Vermutung von Laszlo Fejes-Toth, die ausgehend von der Kusszahl 12 von Kugeln in drei Dimensionen vermutet, dass das aus der Konfiguration abgeleitete Voronoi-Polygon mindestens das Volumen eines regulären Dodekaeders hat (der entsprechend dem Problem skaliert ist). McLaughlin war damals erst Vordiplom-Student (mit Hauptfach Musik, Klarinette). Er erhielt dafür 1999 den Frank and Bennie Morgan Prize für herausragende Arbeiten von Mathematikstudenten.

Hales selbst schrieb einen Übersichtsartikel über den Beweis und die Geschichte der Keplervermutung und verwandter Vermutungen in den Notices of the AMS. Der Aufsatz gewann 2003 den Chauvenet-Preis.

Offenlegung der Hintertür im NIST-Standard zur Zufallszahlenerzeugung

Aufmerksamkeit wurde Hales auch zuteil für seine Analyse des US-Standards zur Erzeugung von Zufallszahlen (Dual EC DRBG), in der er die vorher von Dan Shumow und Nils Ferguson gefundene Schwäche des Verfahrens mathematisch beschrieb. Die Normungsbehörde NIST musste auch aufgrund seiner Veröffentlichung das Verfahren Dual_EC_DRBG aus dem Standard SP 800-90A entfernen.