Bislang galt: Computer können rechnen, aber mathematische Beweise bleiben Kopfarbeit. Doch ein neues Verfahren könnte die Lösung großer Probleme revolutionieren.
Das wäre anders, wenn es ein automatisiertes Verfahren gäbe, das mathematische Arbeiten auf ihre Korrektheit prüft – was nun so weit ist. Es heißt Lean, und der aus Brasilien stammende de Moura, zurzeit als Informatiker in der Forschungsabteilung von Amazon beschäftigt, hat es seit 2013 mitentwickelt. Große Teile des mathematischen Wissens sind für Lean bereits in eine Art Computersprache übersetzt worden. Wenn nun eine Mathematikerin oder ein Mathematiker einen neuen mathematischen Beweis vorschlägt und in Lean formuliert, kann das System ihn Schritt für Schritt nachvollziehen und nachher mit dem Siegel „stimmt“ oder „stimmt nicht“ versehen. Jeder kann dem Ergebnis trauen, sobald es erfolgreich überprüft wurde.
Bei der Arbeit mit Lean müssen die menschlichen Mathematiker noch selbst die Idee für einen Beweis haben. Schon bald aber könnten auch Computer neue Beweise vorschlagen. Nimmt man beides zusammen – die Beweisfindung und die Überprüfung –, dann bekommen menschliche Forscherinnen und Forscher einen mächtigen Gehilfen an die Hand. So mächtig, dass der sie sogar eines Tages überflügeln könnte.
Um die Tragweite dieser Entwicklung zu verstehen, die erst vor ein paar Jahren begann, muss man ein paar Missverständnisse aus dem Weg räumen. Nummer eins: Computer helfen Mathematikern schon jetzt permanent in ihrem Berufsalltag, weil sie viel besser rechnen können als Menschen. Bloß: Rechnen ist gar nicht das Kerngeschäft von Mathematikern. „Wir erforschen den Raum dessen, was wahr und falsch ist“, sagt Terence Tao, ein australisch-amerikanischer Mathematiker, der uns später noch begegnen wird. „Und warum Dinge wahr sind.“
Ein Beispiel: Computer mögen in der Lage sein, Primzahlen zu berechnen – also jene Zahlen, die nur durch eins und sich selbst teilbar sind und elementare Bausteine der Zahlenwelt darstellen. Darin sind Maschinen uns überlegen. Die größte Primzahl, die sie berechnet haben, hat fast 25 Millionen Stellen. Aber Mathematiker wollen wissen: Hört die Abfolge dieser Zahlen irgendwann einmal auf? Gibt es unendlich viele Primzahlen? Diese Frage kann man mit noch so viel Rechenarbeit nicht beantworten, es muss ein Beweis her. Der ist relativ einfach, schon der alte Grieche Euklid kannte ihn: Man nimmt an, es gäbe eine größte dieser Zahlen, und konstruiert dann eine neue Zahl, die durch keine der bisherigen Primzahlen teilbar ist.
Einen Beweis zu finden, ist eine kreative Tätigkeit, es gibt keinen Standardweg dafür. Und wenn jemand einen gefunden hat, muss er oder sie die mathematische Community von dessen Richtigkeit überzeugen. Hier kommt das zweite Missverständnis ins Spiel: dass es relativ offensichtlich ist, ob ein Beweis stimmt. So hat der japanische Mathematiker Shin’ichi Mochizuki 2012 einen Beweis für die sogenannte ABC-Vermutung vorgelegt, eine relativ einfach zu formulierende Behauptung über die ganzen Zahlen. Bis heute streitet die Fachwelt darüber, ob der Beweis korrekt ist oder nicht.
Das Problem wird besonders heikel in den obersten Etagen der mathematischen Abstraktion, wo die intellektuelle Luft immer dünner wird. Als der Bonner Mathematiker Peter Scholze 2018 die Fields-Medaille bekam, die auch der „Mathematik-Nobelpreis“ genannt wird, antwortete er im ZEIT-Interview auf die Frage, wie viele Menschen seine Arbeit komplett verstehen würden: etwa zehn. Es ist schon vorgekommen, dass in wichtigen, von wenigen Menschen verstandenen Beweisen nachträglich argumentative Lücken entdeckt wurden.
Dabei ist es natürlich ein Anspruch der Mathematik, dass all ihre Sätze und Theoreme streng logisch von den Axiomen, also den Grundeigenschaften etwa der natürlichen Zahlen, abgeleitet sind. Es ist nur praktisch unmöglich, diese komplette Ableitung in jedem konkreten Fall aufzuschreiben. Und da kommen „Proof-Checker“ wie Lean ins Spiel: Wenn alle Elemente der Mathematik, also Axiome, Definitionen und Sätze, tatsächlich formal in einer Art Computersprache formuliert werden, dann kann man das gesamte mathematische Gebäude neu errichten und systematisch überprüfbar machen.
„Es ist Zeit, dass wir uns modernisieren“
Solche Versuche gab es schon in der Vergangenheit. Lean ist dabei weiter vorgedrungen als jedes System zuvor. Bereits der erste Prototyp war in der Lage, den Satz über die Unendlichkeit der Primzahlen zu beweisen. Seitdem haben die Lean-Nutzer Baustein für Baustein eine Bibliothek aufgebaut, auf die sie sich stützen können – nicht jeder neue Beweis muss wieder im Urschlamm der einfachsten Axiome beginnen.
Mittlerweile ist alles, was Mathematikstudierende in den ersten Semestern lernen, in Lean codiert. Je anspruchsvoller es wird, desto löchriger wird das System aber. Bisher enthält die Bibliothek etwa 1,5 Millionen Zeilen Programmcode – um mit der Entwicklung der Mathematik mithalten zu können, müsste sie jedes Jahr um zehn Millionen Zeilen wachsen, schätzt Leonardo de Moura. Das geht nur, wenn Tausende von Mathematikerinnen und Mathematikern sich beteiligen.
Als Peter Scholze die Fields-Medaille für seine Arbeit über sogenannte perfektoide Räume bekam, beschloss der britische Mathematiker Kevin Buzzard, diese Theorie für Lean zu formalisieren. Und als Scholze im Sommer 2019 einen Beweis für einen komplizierten neuen Satz erdacht hatte, von dem er selbst nicht vollständig überzeugt war, trat die Lean-Community in Aktion. Scholze selbst war allerdings nicht an der Programmierung beteiligt. Im Juli 2022 schließlich konnte das „Liquid Tensor Project“ abgeschlossen werden – Scholzes Beweis erhielt das Prädikat „vom Computer überprüft“.
In einer E-Mail sagt Peter Scholze heute über das Projekt, es sei „unterhaltsam“ gewesen. Er ist beeindruckt von den Möglichkeiten, Beweise zu überprüfen, mahnt aber auch: „Man muss aufpassen, dass dadurch das eigentliche, tiefe Verständnis für die Mathematik nicht verloren geht.“ Für Lean hatte das Unterfangen einen unschätzbaren Werbeeffekt – zeigte es doch, dass sich auch die vorderste Forschungsfront der Mathematik formalisieren lässt.
Ein anderer Fields-Medaillenträger, der auf Lean aufmerksam wurde, sah ein erheblich größeres Potenzial in der neuen Technik. Terence Tao von der University of California in Los Angeles, der die Medaille 2006 bekam und der unangefochtene Superstar der US-Mathematik ist, begann sich 2023 für den Proof-Checker zu interessieren. Er nahm sich vor, einen Beweis für die sogenannte Polynomiale Freiman-Ruzsa-Vermutung zu formalisieren, den er gerade veröffentlicht hatte, und kniete sich in den Lean-Code. Er zerlegte den Beweis in viele Schritte und verteilte die Aufgaben an rund 20 Helferinnen und Helfer aus der Lean-Gemeinde. In wenigen Wochen war der Beweis formalisiert und überprüft.
Die herkömmliche Mathematik arbeitet heute aber noch so wie vor Hunderten von Jahren. Mit Proof-Checkern wird nun eine neue Arbeitsweise möglich. Beim Kongress der amerikanischen Mathematiker Anfang Januar in San Francisco hielt Tao darüber einen Vortrag. „Wir arbeiten gewöhnlich mit maximal fünf Leuten zusammen, weil jeder dem anderen vertrauen und dessen Arbeit checken muss“, erzählt Tao am Rand des Kongresses. „Es ist Zeit, dass wir uns modernisieren.“ Die Formalisierung mache es möglich, auch in der Mathematik große ungelöste Probleme mit einem großen, arbeitsteiligen Team anzugehen.
Im Moment steht dem noch die Tatsache entgegen, dass die Formalisierung eines Beweises äußerst aufwendig ist. Tao schätzt, dass es zehnmal so lange dauert, einen Beweis in Lean aufzuschreiben, wie auf die herkömmliche Weise. Aber wenn die Bibliothek der formalisierten Mathematik wächst, könnte dieser Faktor schrumpfen. Und irgendwann, so hofft er, werde man durch Lean Zeit sparen.
Lean arbeitet formalisierte mathematische Sätze nach festen Regeln ab. Künstliche Intelligenz kommt hier nicht zum Zuge. Angesichts der sich rasant entwickelnden KI stellt sich aber die Frage: Könnte man nicht auch große Sprachmodelle wie GPT für mathematische Forschung nutzen?
„Vorerst sitzen wir noch am Steuer“
Chatbots wie ChatGPT sind bereits in der Lage, einfache mathematische Aufgaben zu lösen. Beim großen Mathematiktest der ZEIT im Oktober schnitt ChatGPT besser ab als 92 Prozent der Deutschen. Auch einfache Beweise kann der Bot führen. Allerdings „beweist“ er auch manchmal falsche Behauptungen, erzählt Leonardo de Moura. Etwa, dass es zwischen zwei ganzen Zahlen immer unendlich viele weitere ganze Zahlen gebe – was wirklich mathematischer Unsinn ist.
Um einem Sprachmodell die formale Strenge höherer Mathematik beizubringen, muss es einem spezielleren Training unterzogen werden. Daran haben Tony Wu und Christian Szegedy seit 2015 bei Google gearbeitet. Kürzlich sind sie zu der neuen KI-Firma xAI von Elon Musk gewechselt.
Anders als ihr Chef, dessen Firmen notorisch pressefeindlich sind, haben die beiden KI-Entwickler, die xAI mitgegründet haben, keine Berührungsängste. Wie Musk lieben sie starke Worte: In einem Café in Palo Alto im Silicon Valley erzählen die beiden im Interview, dass sie mit ihrer KI „die Mathematik lösen“ wollen. Was bedeutet das? Der Computer soll den besten menschlichen Mathematikern ebenbürtig sein und sie irgendwann überflügeln. Der Weg dorthin: Ein Sprachmodell, trainiert mit mathematischer Literatur, formuliert mögliche Beweise für ein Theorem – und ein Proof-Checker wie Lean überprüft, ob der Beweis wirklich formal korrekt ist oder eine der „Halluzinationen“, für welche die Modelle bekannt sind.
Im Moment sind diese KI-Systeme noch auf dem Niveau von Gymnasiasten, aber ganz unbescheiden schätzt der aus Ungarn stammende Christian Szegedy, dass sie ihr Ziel schon im Jahr 2026 erreichen. „Vor ein paar Jahren lag meine Schätzung noch beim Jahr 2029, aber ich werde immer optimistischer.“ Einer seiner Brüder, auch ein Mathematiker, nenne das Projekt „eine intellektuelle Atombombe“ – damit könne eine ganz neue Ära in der Mathematik anbrechen.
Arbeitende Mathematiker wie Terence Tao haben ihre Zweifel an diesen Prognosen. „Ihr Zeitrahmen ist ein bisschen aggressiv. Aber ich glaube, in drei Jahren wird die KI ein großartiger Co-Pilot für Mathematiker sein.“
Ein Problem beim Training von Sprachmodellen für mathematische Zwecke ist, dass der Umfang der akademischen Mathematik-Literatur natürlich viel geringer ist als die schieren Datenmengen, mit denen die allgemeinen Modelle trainiert werden. Vor allem aber könnte es das falsche Material sein: Das, was Mathematiker in Zeitschriften veröffentlichen, ist nur das kondensierte Ergebnis eines langen kreativen Prozesses. Die Gedankengänge, die zur Formulierung eines Beweises geführt haben, werden nicht erläutert, Irrwege nicht dokumentiert. „Es steckt so viel Wissen in den individuellen Mathematikerköpfen“, sagt Terence Tao, „und nur ein Bruchteil davon wird explizit gemacht.“ Aber das könnten die kollaborativen Lean-Projekte ändern: Vielleicht müssten Forscher, wenn sie mit einer solchen KI zusammenarbeiten wollen, künftig zustimmen, dass der gesamte Prozess aufgezeichnet wird. „Damit wird dann die nächste KI-Generation trainiert.“
Werden die künstlichen Intelligenzen in Zukunft also die Beweise führen und in Sphären vordringen, in denen ein Mensch ihnen kaum noch folgen kann? Tao glaubt nicht, dass die KI uns irgendwann überflüssig machen wird. „In der Zukunft werden wir keine Beweise mehr aufschreiben – wir erklären unsere Idee irgendeinem ChatGPT, das formalisiert die Idee in Lean. Und wenn alles funktioniert, drückt man einen Knopf, und der fertige Artikel wird an eine mathematische Zeitschrift verschickt. Auch Leonardo de Moura will Mathematiker beruhigen. Es werde noch genügend Arbeit geben für Menschen: „Da sind die Leute, die ein neues Gebiet begründen und von einem sehr hohen Level auf das Problem schauen, ich nenne sie auch die Architekten. Dann gibt es die Problemlöser, die sich um die Details kümmern.“ Terence Tao erwähnt noch die KI-Trainer, die den Maschinen neue mathematische Gebiete beibringen, und die Übersetzer, die von der KI entwickelte Beweise für Menschen verständlich machen.
Mit solchen fast industriellen Großanstrengungen könnte es gelingen, die großen ungelösten Fragen der theoretischen Mathematik zu beantworten, etwa die Riemannsche Vermutung oder das P=NP-Problem. Ob die Maschinen danach eine Mathematik treiben, die für uns so unverständlich ist wie der Primzahlen-Beweis für einen Schimpansen – das ist heute noch Science-Fiction. „Vorerst sitzen wir noch am Steuer“, sagt Terence Tao. „In 50 Jahren ist das vielleicht anders.“