Die Welt der Mathematik steht vor einem bedeutenden Wandel. Künstliche Intelligenz hilft nicht mehr nur bei Berechnungen, sondern ist nun auch in der Lage, komplexe mathematische Beweise zu verifizieren, eine Aufgabe, die bisher menschlichen Experten vorbehalten war. Dieser Durchbruch verspricht, die Forschung zu beschleunigen, Fehler zu beseitigen und die Art und Weise, wie mathematisches Wissen geschaffen und validiert wird, grundlegend zu verändern.
Die Herausforderung der Formalisierung
Seit Jahrzehnten träumen Mathematiker von einer automatisierten Beweisüberprüfung. Bestehende Tools können Beweise prüfen, allerdings nur, wenn sie zunächst in ein strenges, computerlesbares Format übersetzt werden – ein Prozess, der Formalisierung genannt wird. Dies ist bekanntermaßen mühsam und erfordert oft Monate oder sogar Jahre sorgfältiger Arbeit. Das Problem ist nicht die Mathematik selbst; Es liegt an der unflexiblen Natur von Programmiersprachen, die absolute Präzision erfordern, während die menschliche Notation flüssiger sein kann.
Math, Inc. und die Gauss-KI
Ein Start-up namens Math, Inc. behauptet, diese Hürde mit seiner KI namens Gauss überwunden zu haben. Das Unternehmen hat zwei bahnbrechende Beweise von Maryna Viazovska erfolgreich formalisiert, die 2022 die prestigeträchtige Fields-Medaille für ihre Arbeit zur Kugelpackung in höheren Dimensionen erhielt. Diese Beweise galten als äußerst komplex und die Fähigkeit der KI, sie automatisch zu übersetzen, ist ein großer Fortschritt.
Das Sphere Packing Puzzle: Warum es wichtig ist
Viazovskas Forschung befasste sich mit einem klassischen Problem: Wie man Kugeln am effizientesten anordnet. In drei Dimensionen ähnelt die dichteste Packung dem Stapeln von Orangen in einem Lebensmittelgeschäft. Aber mit zunehmender Dimension wird das Problem exponentiell schwieriger. Viazovska löste es für acht und 24 Dimensionen und bewies, dass durch die Übertragung effizienter Anordnungen aus niedrigeren Dimensionen in jedem höheren Raum eine zusätzliche Kugel untergebracht werden könnte.
Dies ist nicht nur eine abstrakte Theorie. Die Kugelpackung findet Anwendung in Bereichen wie der Codierungstheorie, der Materialwissenschaft und sogar dem Arzneimitteldesign. Um auf dieser Arbeit aufzubauen, sind genaue Beweise unerlässlich.
Eine gestörte Zusammenarbeit
Auch die Erfolgsgeschichte von Gauss ist eine warnende Geschichte. Forscher hatten jahrelang an der manuellen Formalisierung von Viazovskas Beweisen zusammengearbeitet und die Arbeit in überschaubare Teile für die Lean-Formalisierungsgemeinschaft zerlegt. Math, Inc. nutzte stillschweigend ihre Fortschritte und entwickelte dann seine KI, um die Aufgabe innerhalb von Wochen zu erledigen, ohne den Fortschritt vollständig offenzulegen.
Wie Hariharan, einer der Mitarbeiter, es ausdrückte: „KI ist disruptiv.“ Das Team hatte geplant, ihre Formalisierung als Grundlage für die Bachelorarbeit eines Studenten zu verwenden, doch die KI löste das Problem zuerst.
Die Zukunft: KI als mathematischer Supervisor
Math, Inc. hat seitdem Viazovskas zweiten Beweis formalisiert und 120.000 Zeilen Lean-Code generiert. Die Auswirkungen sind weitreichend. KI kann nicht nur Beweise übersetzen, sondern auch Fehler in Originalarbeiten erkennen und korrigieren.
Poiroux, der Gründer von Math, Inc., stellt sich eine Zukunft vor, in der KI „die gesamte Mathematik überwacht … und vielleicht sogar den Menschen in der Forschung übertrifft“. Sobald die KI mathematische Konzepte vollständig versteht, könnte sie diese auf völlig neue Weise angehen und neuartige Ergebnisse generieren.
Dies wirft kritische Fragen zur Rolle menschlicher Mathematiker auf. Wird KI zum ultimativen Schiedsrichter der mathematischen Wahrheit? Die Entwicklung von Gauß lässt vermuten, dass die Antwort näher liegt, als wir denken.
