400 Jahre später: Kepler, Hales, Viazovska
Kepler konnte das aber nicht beweisen. Erst im Jahr 1998 gelang das dem US-Amerikaner Thomas Hales. Sein Beweis war jedoch so umfangreich, dass er dazu einen Computer verwenden musste: einen Vorfahren der heutigen KI-Beweis-Assistenten. Weil nicht mit hundertprozentiger Sicherheit festzustellen war, dass Hales' Code keine Fehler enthielt, akzeptierten nicht alle den Beweis.
Erst als dieser 2014 wiederum computergestützt formalisiert wurde, galt die Keplersche Vermutung in drei Dimensionen als bewiesen(öffnet im neuen Fenster). Es war eines der ersten mathematischen Projekte, die mithilfe eines Computers formalisiert wurden. Diese Tradition setze Math, Inc. fort, sagt Birkbeck.
Aber Mathematiker wären keine Mathematiker, wenn sie sich keine Gedanken über höhere Dimensionen machen würden. So erhielt die ukrainische Mathematikerin Maryna Viazovska im Jahr 2022 die Fields-Medaille(öffnet im neuen Fenster), weil sie zeigte, dass Kugeln auch in acht Dimensionen nicht mehr als ein bestimmtes Volumen einnehmen können.
Später bewies sie dasselbe auch in 24 Dimensionen – in allen anderen Dimensionen bleibt die Keplersche Vermutung genau das: nur eine Vermutung.
Gauss liefert zwei Datenpunkte
Aufbauend auf der Arbeit von Viazovska und einigen Kollegen(öffnet im neuen Fenster), hat Math Inc. nun die Beweise in 8 und 24 Dimensionen formalisiert. Das bedeutet, es wurde auf eine Art, die von Computern interpretiert werden kann, gezeigt, dass der Beweis wirklich stimmt. Bei Hales' ursprünglichem Beweis war das nötig, um zu belegen, dass sein Code keine Fehler enthielt. Bei Viazovkas Beweisen hingegen habe es "keine Zweifel an deren Richtigkeit" gegeben, sagt Buzzard. "Deswegen hat sie die Fields-Medaille gewonnen."
In diesem Fall liegt der Sinn der Formalisierung also nicht darin, zu zeigen, dass der Beweis stimmt. Vielmehr biete die Formalisierung Datenpunkte, sagt Buzzard. Erstens, dass Beweis-Assistenten Mathematik formalisieren können, die komplex genug ist, eine Fields-Medaille zu verdienen.
Zweitens, dass KI gestützte Werkzeuge unter den richtigen Voraussetzungen in der Lage sein können, einen entsprechenden Beweis automatisch zu formalisieren. Der Einsatz von KI, sagt Birkbeck, habe es erlaubt, den Beweis "viel schneller zu formalisieren, als wir erwartet haben". Das belege auch wie mächtig die Programmiersprache Lean geworden sei, speziell deren Library Mathlib, die sowohl Birkbeck als auch Buzzard maintainen und entwickeln.
- Anzeige Hier geht es zu Künstliche Intelligenz: Wissensverarbeitung bei Amazon Wenn Sie auf diesen Link klicken und darüber einkaufen, erhält Golem eine kleine Provision. Dies ändert nichts am Preis der Artikel.