KI-Unterstützung ist erst am Anfang
Birkbeck äußert aber auch Bedenken. Er mache sich Sorgen, dass jemand sich das Projekt von Math, Inc. ansehe und denke, KI habe sämtliche Matheprobleme oder die Formalisierung gelöst. Dabei sei es immer noch "entscheidend, dass Menschen diese KI-Werkzeuge lenken". Sich nur auf den KI-Teil zu konzentrieren, ignoriere die Arbeit, die viele Mathematiker im Voraus hätten leisten müssen, damit der Beweis formalisiert werden konnte.
Außerdem sei der Code, den Gauss produziere, "weit unter dem, was Menschen können". Sein ursprünglicher Beweis bestand aus 500.000 Zeilen(öffnet im neuen Fenster), und selbst nach umfangreichem Refactoring, das ihn auf 200.000 Zeilen reduzierte, sei dieser Code "viel schwieriger zu maintainen" als guter von Menschen geschriebener Code.
Es muss nur der Code kompilieren
Andere Experten sehen kaum Hoffnung, das Forschungsgebiet Formalisierung vor KI-Firmen zu bewahren. So sieht das zum Beispiel Patrick Massot, Professor am Laboratoire de Mathématiques d'Orsay der Universität Paris-Saclay und einer der Begründer der modernen Formalisierung.
Massot schrieb in einem öffentlichen Online-Lean-Forum(öffnet im neuen Fenster), KI-Firmen und "insbesondere Math, Inc." würden Formalisierung durch automatische generierte Beweise "in ein riesiges radioaktives Niemandsland verwandeln, auf dem nie wieder Leben gedeihen kann". Jungen Mathematikern riet er bereits jetzt, sich lieber Projekte in anderen Bereichen zu suchen.
Denn Mathematikerinnen und Mathematiker erhalten aktuell wenig Ansehen oder Fördergelder, wenn sie etwas als Zweite machen. Selbst wenn der erste Beweis aus kaum verständlichem, KI-generierten Code besteht: "Solange der Code kompiliert", sagt Buzzard, gelte die Sache als erledigt.
Formalisieren kann mehr als Beweis sein
Dabei wollten Buzzard und Kollegen "mehr als nur schauen, ob [Viazovskas] Beweis korrekt ist". Ihre Formalisierung(öffnet im neuen Fenster) sollte eine "interaktive Blaupause" werden: eine Kombination aus Lean-Code und für Menschen verständlicher Mathematik. Das sollte den Beweis "noch schöner" machen und mehr Menschen einen Weg eröffnen, ihn besser zu verstehen.
In Why Formalize (PDF)(öffnet im neuen Fenster) schreibt Massot, der Traum der Formalisierung sei ein mathematisches Dokument, in dem Leser dynamisch verändern könnten, wie viele Details sie sehen und auf welches Hintergrundwissen sie zugreifen möchten. Mit so einer Formalisierung könnten sich auch Nicht-Experten in Viazovskas hochgradig komplexen Beweis einarbeiten. Aus Gauss' Kauderwelsch werde hingegen niemand schlau, sagt Buzzard.
"Aber überlegen Sie mal", fragt er, "was mit der Motivation [des Blaupause-Teams] passiert, jetzt, wo eine Tech-Firma eine Formalisierung im Internet veröffentlicht?"
Aus KI das Beste machen
Tatsächlich sind nicht nur Gauss und der Einsatz von KI umstritten. Auch der immer höhere Stellenwert von Formalisierungen an sich könnte langfristig verändern, welche Mathematik Menschen machen(öffnet im neuen Fenster). Und nicht alle Mathematiker sind darüber glücklich.
Einige befürchten, die Mathematik fokussiere sich heute zu einheitlich und zu stark auf bestimmte Teilgebiete
Diesen Trend könnte Gauss noch beschleunigen. Und zwar bisher ohne einen der großen Vorteile von üblichen Formalisierungen. Denn die ursprüngliche Idee war, jeden logischen Schritt und Gedanken in einem Beweis nachvollziehbar zu machen – so ähnlich retteten junge Mathematiker bereits einige archaische Beweise, die kaum ein lebender Mensch noch verstand(öffnet im neuen Fenster).
Gauss' Beweis kann aber erst mal niemand verstehen. Und darum geht es auch gar nicht. Es ist eine von Computern lesbare, vollständige Dokumentation Viazovskas preisgekrönter Arbeit. Das zu schaffen, ist beeindruckend, und es hat Menschen viel Zeit gespart. Aber es wirft auch Fragen auf, wie man aus solchen Errungenschaften das Beste für die mathematische Community macht.
Tim Reinboth(öffnet im neuen Fenster) ist freiberuflicher Wissenschaftsjournalist und Kognitionswissenschaftler. Er schreibt über Herausforderungen, Möglichkeiten und kuriose Momente an den Schnittstellen von Technologie und Gesellschaft.
Dieser Artikel erscheint bei Golem Plus, weil ...
... er ein aktuelles Spannungsfeld beleuchtet: den Durchbruch KI-gestützter Beweisformalisierung am Beispiel der Fields-Medaillen-Arbeit von Maryna Viazovska – und die damit verbundenen Folgen für die Mathematik als Disziplin. Gleichzeitig bietet er Einblicke in eine kontroverse Debatte unter Fachleuten wie Kevin Buzzard, die über die Zukunft von Beweisen, Verständlichkeit und wissenschaftlichem Ansehen streiten.
- 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.