Computer als Assistenz-Mathematiker

Deswegen prüft die Forschungsgemeinschaft Beweise mittels Peer-Review-Verfahren auf Korrektheit und Vollständigkeit. Dabei bewerten unabhängige Gutachterinnen und Gutachter die entsprechenden wissenschaftlichen Arbeiten. Ob ein Theorem als bewiesen gilt, wird also letztlich durch einen Konsens entschieden.

Peter Scholzes komplexer Beweis

Peter Scholze von der Universität Bonn muss sich immer wieder mit der Frage nach der Korrektheit seiner Beweise auseinandersetzen. Der Mathematiker stellt mit seinen Theorien die Fachwelt fast schon regelmäßig auf den Kopf. Für seine „Theorie der perfektoiden Räume“ erhielt er 2018 im Alter von nur 30 Jahren die Fields-Medaille, die oft als Nobelpreis der Mathematik bezeichnet wird.

Anschließend entwickelte er gemeinsam mit seinem Kollegen Dustin Clausen die „Theorie der verdichteten Mengen“. Diese liefert eine neue Grundlage für die Topologie, einem eher jungen Teilgebiet der Mathematik, das Ende des 19. Jahrhunderts entstand. Die Topologie befasst sich mit den Eigenschaften geometrischer Objekte, die bei stetigen Verformungen wie dem Strecken, Stauchen und Biegen unverändert bleiben. Das Fachgebiet untersucht also, welche fundamentalen Gemeinsamkeiten bestimmte Objekte haben.

Scholzes und Clausens Theorie der verdichteten Mengen hinterfragt die Praktikabilität zentraler und etablierter Konstrukte der Topologie. Einige grundlegende Definitionen des Fachgebiets haben die Mathematiker dafür neu formuliert. So auch die Definition eines sogenannten topologischen Raumes, die Felix Hausdorff vor etwa 100 Jahren einführte. „Dustin Clausen und ich sind zu der Überzeugung gekommen, dass sich viele technische Probleme der Mathematik komplett in Luft auflösen, wenn man die Definition geringfügig verändert“, erklärt Scholze.

Im Laufe ihrer Forschung erkannten Scholze und Clausen, dass die Funktionalität ihrer Theorie maßgeblich von einem einzelnen, fundamentalen Theorem abhing: ihrem „Hauptsatz der flüssigen Vektorräume“. Wäre das Theorem korrekt, so ließe sich ihre gesamte Theorie tatsächlich anwenden – falls nicht, wäre sie kaum zu gebrauchen. Die Mathematiker benötigten daher einen sicheren Beweis des Theorems. Ein Jahr lang arbeiteten sie daran. Das Ergebnis: Ein langer und schwieriger Beweis, der sich Vorgehensweisen und Konstrukten der Algebra bedient, aber auch viel mathematische Abschätzung benutzt. Um ihren Beweis prüfen zu lassen, benötigten die Forscher daher eine Mathematikerin oder einen Mathematiker, der mit beiden Fachdisziplinen sicher und intuitiv umgehen konnte.

Weltweit fanden Scholze und Clausen jedoch niemanden, der beide mathematischen Disziplinen hinreichend gut beherrschte, um ihren Beweis zu überprüfen. Deswegen entschieden sich die Mathematiker dazu, ihre Arbeit auf eine ungewöhnliche Weise zu verifizieren: Ein Computerprogramm sollte den Beweis auf seine Korrektheit untersuchen.

Im November 2020 schlägt Peter Scholze daher in einem Blogpost ein Projekt vor, das er in Anspielung auf die Rockband Liquid Tension Experiment als „Liquid Tensor Experiment“ bezeichnet. Darin fordert Scholze die Forschungsgemeinschaft heraus, den Hauptsatz der flüssigen Vektorräume computergestützt zu überprüfen. „Ich denke, dass dieses Theorem von größter grundlegender Bedeutung ist. Sich zu 99,9 Prozent sicher zu sein, ist also nicht genug“, schreibt er damals in dem Blogeintrag.

Computerprogramme als Beweisassistenten

Maschinelle Beweisassistenten werden seit Jahrzehnten entwickelt. Die Computerprogramme überprüfen die mathematische Argumentation eines Beweises anhand logischer Prinzipien. Indem sie maximal kleinschrittig vorgehen, können die Programme Fehler entdecken, die vom Menschen übersehen wurden. So helfen sie, Unsicherheiten in mathematischen Arbeiten zu reduzieren. Bestenfalls können sie Beweise sogar vollständig verifizieren.

Die Anwendung ist jedoch sehr aufwendig. Denn: Damit die Computerprogramme einen Beweis überprüfen können, muss ihnen vorerst der gesamte mathematische Hintergrund der Theorie in einer für den Computer verständlichen Sprache beigebracht werden. Mathematiker sprechen hierbei von einer vollständigen Formalisierung des Beweises. Deswegen wurden Beweisprogramme lange Zeit eher für relativ elementare und wenig umfangreiche Beweise genutzt.

Der Hauptsatz der flüssigen Vektorräume ist jedoch keineswegs elementar, sondern ein theoretisch tiefgreifendes Theorem. Das Team des seit 2013 entwickelten Beweisassistenten „Lean“ nahm Scholzes Herausforderung dennoch an: 25 Personen aus aller Welt arbeiteten ab 2021 monatelang an der Formalisierung des Beweises. Insgesamt schrieben sie etwa 90.000 Codezeilen. Mit Erfolg: Das Team konnte den schwierigen Beweis verifizieren.

„Aktuelle mathematische Forschung, die so komplex ist, dass sie kaum in ein menschliches Gehirn passt, kann mittels Lean in relativ kurzer Zeit verifiziert werden. Das hat das Liquid Tensor Experiment gezeigt“, sagt Johan Commelin. Er ist Leitender Ingenieur für mathematische Forschung bei der Lean Focused Research Organization und eine der zentralen Personen hinter dem Liquid Tensor Experiment.

KI-generierte Beweise

Beispiele wie diese werfen die Frage auf, ob Computerprogramme künftig noch einen Schritt weitergehen könnten: weg vom reinen Prüfen von Beweisen, hin zu eigenständiger mathematischer Forschung. Aktuelle Beweisassistenten wie Lean arbeiten zwar mit traditionellen Algorithmen und folgen starren mathematischen Regelwerken, in Kombination mit KI-Systemen wie Large Language Models hätten sie jedoch das Potenzial, eigenständig neue Beweise zu führen – und zwar mit deutlich höherer Erfolgswahrscheinlichkeit, als es ein Large Language Model allein könnte.

Auf einem Large Language Model basiert beispielsweise der Chatbot ChatGPT. Stellt man ChatGPT eine mathematische Frage, erhält man häufig absurde Antworten. Die KI wird aber mit jedem Jahr besser im Lösen mathematischer Aufgaben. Der Mathematiker und Fields-Medaillen-Gewinner Terence Tao von der University of California führte dazu ein kleines Experiment durch: Er stellte dem Chatbot im März 2023 eine vage formulierte mathematische Aufgabe, die mithilfe eines in der Literatur bekannten Theorems gelöst werden konnte. Im September 2024 wiederholte er das Experiment. Dazu schrieb er im sozialen Netzwerk Mathstodon: „2023 war GPT in der Lage, einige relevante Konzepte zu erwähnen, die Details waren jedoch halluzinierter Unsinn. Dieses Mal wiederum wurde das Theorem identifiziert und eine vollkommen zufriedenstellende Antwort gegeben.“

Trotz der Fortschritte produzieren Large Language Models vor allem bei komplexen Themen noch immer viel mathematischen Unsinn. Denn vereinfacht dargestellt, generieren sie auf Basis ihrer Trainingsdaten lediglich eine statistisch wahrscheinliche Antwort auf die gestellte Frage – ohne jedoch ein Verständnis für die tatsächlichen logischen Zusammenhänge zu haben: Eine sehr ungenaue Methode gemessen an den absolut exakten Ansprüchen der Mathematik.

Das ist jedoch kein Problem, wenn man die KI-Systeme in Kombination mit Lean verwendet. Schließlich überprüft Lean die mathematische Argumentation der KI. „Large Language Models können etwas schreiben, das überzeugend aussieht. Wenn es aber kein korrekter Lean-Beweis ist, wird Lean sich davon nicht überzeugen lassen“, erklärt Johan Commelin. Versuche, mit Hilfe künstlicher Intelligenz mathematische Beweise zu führen, sehen also wie folgt aus: Eine KI, die gezielt für mathematische Themen trainiert wurde, schlägt verschiedene Ansätze vor, Lean überprüft diese, und mit etwas Glück findet die KI vielleicht einen Weg, der tatsächlich funktioniert. An dieser Stelle lässt sich tatsächlich von Glück sprechen – besonders effizient ist die Anwendung nämlich noch nicht.

„Habe ich eine Codezeile bereits zur Hälfte geschrieben, kann die KI sie häufig vervollständigen. In dem nächsten Beweisschritt muss ich ihren Kurs jedoch meist wieder korrigieren“, berichtet Commelin von seiner persönlichen Erfahrung mit mathematischen KI-Systemen. Die Entwicklung der Programme befindet sich zwar noch in den Anfängen, geht jedoch schnell voran. Unter anderem durch Projekte wie das Liquid Tensor Experiment, deren bereits formalisierte Beweise der KI als Trainingsdaten dienen.

Das KI-System AlphaProof des Unternehmens Google DeepMind versuchte im vergangenen Jahr, die Aufgaben der Internationalen Mathematik-Olympiade zu lösen, an dem alljährlich Schülerinnen und Schüler aus aller Welt teilnehmen. Als Vorbereitung für den Wettkampf lernte das System, Millionen verschiedene Probleme zu beweisen oder zu widerlegen, und erzielte anschließend in der Olympiade 28 von maximal zu erreichenden 42 Punkten. Damit gewann die KI eine Silbermedaille und verfehlte die Goldmedaille nur knapp. Gold gewannen 58 der 609 Teilnehmerinnen und Teilnehmer, die eine Mindestpunktzahl von 29 Punkten erzielt hatten.

Löst KI die Millenium-Probleme?

Entwicklungen wie diese lassen vermuten, dass die Anwendung in den kommenden Jahren an Nützlichkeit gewinnen und eine zunehmend wichtigere Rolle in der Mathematik spielen wird. „Es ist zu erwarten, dass der Forschungsgemeinschaft innerhalb des kommenden Jahrzehnts wirklich nützliche Beweisunterstützungen zur Verfügung stehen“, sagt Johan Commelin und ergänzt: „Dabei denke ich an Unterstützungen bei kleineren mathematischen Problemen und in Form von Gegenbeispielen sowie an Hilfen bei der Suche und Zusammenfassung von Fachliteratur.“

Das Unternehmen Google DeepMind gibt sich noch optimistischer: „Ich glaube wir sind kurz davor, ein Millennium-Problem zu lösen – das werden wir in dem nächsten Jahr oder den nächsten anderthalb Jahren sehen“, behauptet Demis Hassabis, Gründer von DeepMind und Nobelpreisträger für Chemie. Als Millennium-Probleme werden sieben mathematische Probleme bezeichnet, auf deren Lösung jeweils ein Preisgeld von einer Million US-Dollar ausgeschrieben ist. Seit der Preisausschreibung im Jahr 2000 wurde erst eins der Probleme gelöst.

Zukunft der Mathematik

Bisher war die Arbeitsaufteilung in der Mathematik klar geregelt: Maschinen haben komplizierte Rechnungen übernommen, Menschen die Beweise. Nun scheint diese Trennung zu verschwimmen. Dennoch müssen Mathematikerinnen und Mathematiker in Zukunft nicht um ihre Jobs fürchten. Schließlich führen die Beweisprogramme komplexe Beweise noch nicht eigenständig. Und selbst wenn sie das in einigen Jahren könnten, müssten die zu beweisenden Theoreme zuvor weiterhin von Menschen erdacht worden sein. Denn Computer können sich nicht eigenständig Theoreme ausdenken, die spannend und anwendungsreich sind. Dazu fehlt ihnen ein mathematisches Interesse.

„Mathematik ist und bleibt ein menschliches Projekt“, sagt Peter Scholze. Dennoch verändert sich die Wissenschaft aktuell – vor allem durch die Möglichkeit, komplexe Beweise maschinell zu überprüfen. Dadurch kann die Forschungsgemeinschaft nun in relativ kurzer Zeit Gewissheit über die Korrektheit ihrer Theoreme gewinnen. Die Anwendung bringt Mathematikerinnen und Mathematiker aber auch fachlich voran. Denn sie begreifen ihre eigene Arbeit nach dem Prozess der Formalisierung oft besser als zuvor. „Ich habe selbst besser verstanden, was wir in dem Beweis getan haben und habe eine bessere Intuition dafür gewonnen, was in dem Beweis passiert“, resümiert Peter Scholze nach Abschluss des Liquid Tensor Experiments.

In der mathematischen Fachwelt ist die Arbeit mit Beweisassistenten längst zu einem viel diskutierten Thema geworden. Terence Tao hält beispielsweise regelmäßig Vorträge über deren Anwendung. Er ist überzeugt, dass sich die Arbeitsweise in der Mathematik durch Programme wie Lean verändern wird. Bisher war die Mathematik eher eine einsame Wissenschaft. Der britische Mathematiker Andrew Wiles beispielsweise hatte in den 1980er-Jahren über sechs Jahre an einem einzigen Beweis gearbeitet – dem Beweis vom Großen Fermatschen Satz – und tauschte sich dabei ausschließlich mit seiner Frau darüber aus. Dass im Fall des Liquid Tensor Experiments mehr als 20 Mathematikerinnen und Mathematiker gemeinsam an einem Projekt gearbeitet haben, ist also äußerst ungewöhnlich. „In der Mathematik kollaborieren wir üblicherweise nicht mit vielen Menschen. Fünf Personen sind schon viel. Denn wenn man an einem großen Projekt arbeitet, muss man sich darauf verlassen können, dass die Mathematik von jeder Person stimmt“, sagt Terence Tao in einem Vortrag: „Lean jedoch prüft das automatisch. Man kann also mit Leuten zusammenarbeiten, die man vorher noch nie getroffen hat.“

Das größte zurzeit laufende Lean-Projekt möchte den von Wiles bewiesenen Großen Fermatschen Satz nun in Lean formalisieren. Beinahe 350 Jahre lang hatten Mathematikerinnen und Mathematiker zuvor nach einem Beweis des Theorems gesucht. Entsprechend interessiert ist die Fachwelt an der Formalisierung. Nach dem Liquid Tensor Experiment könnte diese Formalisierung den nächsten Meilenstein in der Nutzung maschineller Beweisassistenten darstellen. Außerdem wird das Projekt die mathematische Bibliothek in Lean noch weiter ausbauen. In ein paar Jahren wird diese voraussichtlich so weit entwickelt sein, dass sie über die gesamten Inhalte eines Bachelor- und Master-Studiums der Mathematik verfügt. Dann wird das Programm noch effizienter Beweise prüfen als bisher und die Forschenden noch besser dabei unterstützen, das beeindruckende Theorie-Gebilde der Mathematik weiter auszubauen. ■

Energiereiche exotische Elementarteilchen könnten helfen, Zollkontrollen in Häfen und an Flughäfen zu verbessern.