Mathematik ist traditionell eine einsame Wissenschaft. Andrew Wiles etwa zog sich 1986 sieben Jahre in seine Studierstube zurück, um Fermats Großen Satz zu beweisen. Und die Beweise, die dabei herauskommen, sind für Kolleginnen und Kollegen häufig schwer verständlich, manche sind bis heute umstritten. Aber in den letzten Jahren sind immer größere Gebiete der Mathematik so streng in ihre einzelnen Bestandteile aufgespalten (»formalisiert«) worden, dass Beweise von Computern überprüft und verifiziert werden können.

Terence Tao von der University of California in Los Angeles ist überzeugt, dass diese Verfahren ganz neue Möglichkeiten der Kooperation in dieser Wissenschaft ermöglichen. Nimmt man die jüngsten Fortschritte in der künstlichen Intelligenz noch dazu, etablieren sich in der Mathematik in den nächsten Jahren eventuell ganz neue Arbeitsweisen – und mit Computerhilfe könnten die großen ungelösten Probleme einer Lösung näher kommen.

Terence Tao, in Ihrem Vortrag auf dem Joint Mathematics Meeting in San Francisco Anfang Januar sagten Sie: »Mathematiker trauen einander nicht.« Was haben Sie damit gemeint?

Wir sind nicht grundsätzlich misstrauisch, aber es ist schwer, mit Leuten zusammenzuarbeiten, die man noch nie getroffen hat – es sei denn, man kann ihre Arbeit Zeile für Zeile überprüfen. Fünf Menschen sind normalerweise das Maximum.

Wie verändert sich das mit dem Aufkommen von Beweisprüfern?

Jetzt kann man mit Hunderten von Leuten zusammenarbeiten, die man noch nie zuvor getroffen hat. Man muss ihnen nicht mehr vertrauen, denn sie laden ihren Code hoch und der Lean-Compiler (eine Software, die die logischen Schritte eines Beweises durchgeht; Anm. d. Red.) überprüft ihn. Man kann Mathematik in viel größerem Maßstab betreiben, als wir es normalerweise tun. Als ich unseren jüngsten Beweis für die so genannte PFR-Vermutung formalisiert habe, waren wir mehr als 20 Leute. Wir haben den Beweis in viele kleine Schritte aufgeteilt, und jeder bewies einen dieser kleinen Schritte. Ich musste nicht Zeile für Zeile überprüfen, ob die Beiträge korrekt waren. Mein Job war es, das ganze Projekt zu koordinieren und sicherzustellen, dass alles in die richtige Richtung lief. Es war eine andere Art, Mathematik zu betreiben. Eine modernere Art.

Der deutsche Mathematiker und Fields-Medaillen-Gewinner Peter Scholze hat auch ein Lean-Projekt initiiert – obwohl er mir gesagt hat, dass er nicht viel von Computern versteht.

Bei diesen Formalisierungsprojekten muss nicht jeder ein Programmierer sein. Manche Leute können sich einfach auf das große mathematische Ganze konzentrieren. Und dann gibt es Spezialisten dafür, die kleinere Teile in formale Beweise verwandeln. Es ist eine Arbeitsteilung.

Ich habe vor 20 Jahren von maschinengestützten Beweisen gehört, als das Gebiet noch in den Kinderschuhen steckte. Alle dachten, man müsse bei null anfangen, die Axiome formalisieren, dann die einfache Geometrie und Algebra, und der Weg zur höheren Mathematik lag jenseits aller Vorstellungskraft. Was hat dazu geführt, dass die formale Mathematik plötzlich praktikabel ist?

Eine Sache ist die Entwicklung von Standardbibliotheken. Zur Programmiersprache Lean gehört ein großes Projekt namens Mathlib. Alle grundlegenden Theoreme der ersten Mathematiksemester, etwa aus Analysis und Topologie, wurden nach und nach in diese Bibliothek aufgenommen. Man ist also bereits zu einem beachtlichen Niveau gelangt. Der Traum ist es, die Standardbibliotheken auf das Level der höheren Semester zu bringen. Dann wird es viel einfacher sein, neue Gebiete zu formalisieren. Die Systeme haben auch eine hervorragende Suchfunktion – denn wenn man etwas beweisen will, muss man die Dinge finden können, die bereits verifiziert wurden.

»Wir müssen die Leute dazu bringen, diese Methode zu verwenden«

Es ist also keine Frage der gestiegenen Rechenleistung?

Nein. Nachdem wir zum Beispiel das gesamte PFR-Projekt formalisiert hatten, dauerte es nur noch eine halbe Stunde, es zu kompilieren und zu bestätigen. Das ist nicht der Flaschenhals. Wir müssen die Leute dazu bringen, diese Methode zu verwenden, es muss nutzerfreundlich sein. Die Gemeinschaft umfasst jetzt Tausende von Menschen, es gibt ein sehr aktives Onlineforum, in dem diskutiert wird, wie man das System immer besser machen kann.

Neben Lean gibt es noch andere formale Sprachen wie Isabelle oder Coq. Ist Lean heute der Standard?

Lean hat wahrscheinlich die aktivste Community mit der größten Bibliothek. Für Projekte einzelner Autoren sind vielleicht ein paar andere Systeme besser geeignet, aber Lean ist generell einfacher zu lernen. Vielleicht wird es irgendwann durch eine Alternative ersetzt, doch im Moment ist Lean die dominierende formale Sprache.

Bei einem Vortrag auf dem Joint Mathematics Meeting zu einem anderen mathematischen Problem fragte ein Zuschauer, ob Sie es formalisieren wollten. Sie sagten, das würde zu lange dauern.

Ich könnte es formalisieren, aber das würde mich einen Monat kosten. Wir sind noch nicht an dem Punkt, an dem wir routinemäßig alles formalisieren. Man muss auswählen: etwa die Dinge, die einem persönlich etwas bringen (wie dass man sich in Lean einarbeitet), oder wenn andere wirklich zweifeln, ob ein Ergebnis korrekt ist. Doch die Technik wird immer besser. Deshalb ist es in vielen Fällen klüger zu warten, bis es einfacher wird. Anstatt zehnmal so lange für die Formalisierung zu brauchen wie zum Aufschreiben eines herkömmlichen Beweises, braucht man dann nur noch doppelt so lange.

»In Zukunft werden wir unsere Beweise nicht mehr Zeile für Zeile aufschreiben, sondern sie einer KI erklären, die das in Lean formalisiert«

Sie sprachen sogar davon, den Faktor auf weniger als eins zu senken. Wie soll das gehen?

Mit künstlicher Intelligenz kann das eine echte Möglichkeit sein. Ich denke, in Zukunft werden wir unsere Beweise nicht mehr Zeile für Zeile aufschreiben, sondern sie einer KI erklären, die das in Lean formalisiert. Wenn alles stimmt, sagt die KI: Hier ist dein druckfertiges Paper, hier ist der Lean-Beweis. Wenn du willst, reiche ich es bei einem Fachjournal ein. So könnte die KI in Zukunft zu einem wunderbaren Assistenten werden.

Bis jetzt muss die Idee für den Beweis immer noch vom menschlichen Mathematiker kommen, oder?

Ja, der schnellste und im Moment einzige Weg zur Formalisierung ist es, wenn zunächst ein Mensch den Beweis findet. Der macht eine erste Beweisskizze, und die wird in einen formalen Beweis übersetzt. In Zukunft könnte es allerdings auch anders laufen: Womöglich gibt es kollektive Beweisprojekte, bei denen wir noch nicht wissen, wie der Gesamtbeweis läuft. Aber die Leute haben Ideen, wie man einzelne Teile beweisen kann, formalisieren diese und versuchen sie dann zusammenzufügen. Vielleicht wird in Zukunft ein wichtiges Theorem von einer Gruppe aus 20 Menschen und einer Reihe von KIs bewiesen. Damit kann man Wunderbares schaffen. Es wird jedoch noch viele Jahre dauern, bis das möglich ist. Die Technik ist noch nicht so weit, auch weil die Formalisierung noch so mühsam ist.

Tony Wu und Christian Szegedy haben gerade das neue Unternehmen xAI von Elon Musk mitgegründet, und sie behaupten, dass die Mathematik in drei Jahren in demselben Sinne »gelöst« ist wie das Schachspiel – dass Maschinen im Beweisen besser sind als jeder Mensch.

Ich denke, in drei Jahren werden KI-Systeme für Mathematiker ein nützliches Werkzeug sein, ein großartiger Kopilot. Sie versuchen eventuell, einen Satz zu beweisen, und es gibt einen Schritt, von dem Sie glauben, dass er wahr ist, aber Sie sind sich nicht ganz sicher. Dann fragen Sie die KI: Kannst du das für mich tun? Und die macht vielleicht einen Vorschlag. Ich glaube nicht, dass die Mathematik »gelöst« werden wird. Vielleicht wäre es möglich, wenn es einen weiteren großen Durchbruch in der KI gäbe. Ich denke, die Art und Weise, wie wir Mathematik betreiben, wird sich ändern; die Prognose dieser Kollegen ist allerdings ein bisschen optimistisch.

»In absehbarer Zeit wird die KI zuerst die langweiligen, trivialen Dinge automatisieren«

Ein guter Beweis hakt nicht nur ab, dass etwas korrekt ist, sondern vermittelt auch ein besseres Verständnis der Materie. Wenn wir diese Aufgabe an eine Maschine delegieren – werden wir dann überhaupt noch in der Lage sein zu verstehen, was sie herausgefunden hat?

Mathematiker erforschen den Raum dessen, was wahr und was falsch ist. Und warum Dinge wahr sind. Das tun wir mit Hilfe von Beweisen, und das kostet eine Menge Zeit. Es ist mühsam. Möglicherweise werden wir in Zukunft einfach eine KI fragen: Ist das wahr oder nicht? Und wir können uns auf das konzentrieren, was uns wirklich interessiert. Die KI wird uns dabei helfen, indem sie diesen Prozess beschleunigt. Doch wir werden immer noch am Steuer sitzen. Vielleicht wird das in 50 Jahren anders sein. Aber in absehbarer Zeit wird die KI zuerst die langweiligen, trivialen Dinge automatisieren.

Die Mathematik, die wir machen, ist die Mathematik, zu der unsere Gehirne in der Lage sind. Wenn die KI irgendwann so viel schlauer ist als wir, könnte sie in Sphären vordringen, die wir einfach nicht mehr begreifen.

Die Mathematik ist schon jetzt größer als jeder einzelne menschliche Verstand. Mathematiker verlassen sich routinemäßig auf Ergebnisse, die andere bewiesen haben. Sie wissen ungefähr, warum etwas wahr ist, sie haben eine gewisse Intuition, sie können es jedoch nicht bis auf die Axiome herunterbrechen. Aber sie wissen, wo sie suchen müssen, oder sie kennen jemanden, der es weiß. Es gibt bereits heute viele Sätze, die nur mit Hilfe eines Computers überprüft werden können, der eine Million Fälle durchgerechnet hat. Man könnte sie von Hand verifizieren, doch niemand hat die Zeit dazu, es lohnt sich einfach nicht. In Zukunft wird es nicht mehr nötig sein, dass einer oder eine alles Schritt für Schritt überprüft. Wenn Computer das für uns übernehmen, ist das für mich völlig okay.

An der vordersten Forschungsfront der Mathematik werden häufig Dinge aus scheinbar nicht verwandten Disziplinen zusammengeführt. Nach meinem naiven Verständnis könnte eine KI, die all diese Bereiche kennt, einen Hinweis geben und sagen: Schau doch mal dort nach, das könnte dir bei deinem Problem helfen.

Das ist ein sehr spannendes Potenzial für den Einsatz von KI: Verbindungen schaffen oder zumindest auf mögliche Verbindungen hinweisen. Im Moment ist die Erfolgsquote sehr schlecht, die KI macht Ihnen vielleicht zehn Vorschläge, von denen einer interessant ist und neun unsinnig. Das ist fast noch schlechter als Raten. Aber das könnte sich ändern.

Was sind die Probleme, die dem Training eines mathematischen KI-Sprachmodells im Weg stehen?

Ein Problem ist, dass es nicht genügend Trainingsdaten gibt. Bisher kann man die Algorithmen nur mit den publizierten mathematischen Arbeiten trainieren.

Und selbst wenn man die Daten aller mathematischen Publikationen der Menschheitsgeschichte zum Training benutzen würde, wäre das immer noch sehr wenig im Vergleich zu den Textmengen, mit denen Modelle wie GPT trainiert worden sind.

Vor allem steckt ein großer Teil der Intuition nicht in den gedruckten Artikeln, sondern in Gesprächen zwischen Mathematikern, in Vorlesungen, in Beratungsgesprächen mit Studierenden. Manchmal sage ich im Scherz, dass die KI ein normales Graduiertenstudium absolvieren müsste, in den Seminaren sitzen, Fragen stellen wie Studierende und Mathematik so lernen, wie Menschen sie lernen.

»Mathematiker veröffentlichen nur die Erfolgsgeschichten, nicht den Prozess«

Die veröffentlichte Version eines Beweises ist also immer eine Verkürzung eines Gedankengangs?

Mathematiker veröffentlichen nur die Erfolgsgeschichten, nicht den Prozess. Die Daten, die wirklich wertvoll wären: Jemand probiert etwas aus, es funktioniert nicht ganz, aber er oder sie weiß, wie man es besser machen kann.

Eventuell sollte man mathematische Beweisprojekte so behandeln wie medizinische Studien. Wenn die registriert sind, muss man die Ergebnisse veröffentlichen, auch wenn es nicht funktioniert hat.

Diese Kultur gibt es bei uns nicht. Vielleicht wird die Formalisierung in Zukunft in Echtzeit funktionieren, und wenn man im Jahr 2040 eine ausgeklügelte KI-Version von Lean benutzen und eine Finanzierung für das Projekt haben will, muss man vielleicht zustimmen, dass der gesamte Prozess des Ausprobierens und auch des Scheiterns aufgezeichnet wird. Diese Daten könnten dann für das Training zukünftiger KIs verwendet werden. Oder eine andere Gruppe arbeitet an einem ähnlichen Problem, und die können dann sehen: Oh, diese andere Gruppe hat dasselbe versucht, ist aber gescheitert. So muss man keine Zeit damit verschwenden, genau dieselben Fehler noch einmal zu machen.

Verschwenden Mathematiker eine Menge Zeit?

Oh, sehr viel sogar. Es ist so viel Wissen in den Köpfen einzelner Mathematiker gefangen, und bloß ein winziger Teil wird explizit gemacht. Doch je mehr wir formalisieren, desto mehr von unserem impliziten Wissen wird explizit. Das wird große Vorteile mit sich bringen.