Terence Taos Vorhersage von vor 12 Jahren wurde jetzt von KI wahrgemacht

Es hat sich gezeigt, dass Preisträger der Fields-Medaille manchmal auch als Prophet fungieren.

Vor 12 Jahren war eine Vorhersage, die Terry Tao auf der Bühne der ersten Breakthrough-Preise für Mathematik aussprach, als Wahnsinn angesehen worden:

Eines Tages werden wir vielleicht keine wissenschaftlichen Artikel mehr mit LaTeX verfassen, sondern stattdessen formalisierte Sprachen nutzen, die von Computern verstanden werden können.

In jenem Jahr war der Transformer noch nicht erfunden, und ChatGPT war nicht einmal in Sicht.

Unerwartet trifft der Bumerang das Ziel. Im vergangenen Jahr hat die KI in der Mathematik plötzlich einen starken Schwung genommen.

Von OpenAI, das offene Probleme löst, bis hin zu DeepMind, das mathematische Vermutungen in Massen bewältigt, werden immer mehr mathematische Beweise in formalisierte Systeme übertragen und von Computern automatisch verifiziert.

Wenn man zurückblickt, war Terry Tao derjenige, der zuerst den Trend erkannte und selbst in die Praxis eingestiegen ist.

Innerhalb von zehn Jahren hat er nacheinander großangelegte kollaborative Mathematik vorangetrieben, Lean-formalisierte Beweise durchgeführt und das Equational Theories-Projekt initiiert. Bei 22 Millionen mathematischen Problemen hat er dank der "Kollaboration zwischen KI und Menschen" in nur 48 Stunden die Mehrheit bewältigt.

Das Projekt ist dank der Unterstützung der KI äußerst effizient, und oft muss er selbst gar nicht mehr eingreifen.

Tatsächlich beweist Terry Tao mit seiner Tat, dass die beste Möglichkeit, die Zukunft vorherzusagen, darin besteht, sie selbst zu erschaffen.

Wunderkind, aber fasziniert von Kollaboration

Wenn man über Terry Tao spricht, denken viele Menschen zuerst an seine legendäre Karriere:

Mit zwei Jahren lehrte er ältere Kinder das Zählen, mit sieben Jahren begann er mit der Differential- und Integralrechnung, mit zehn Jahren wurde er der jüngste Bronze-Medailleträger in der Geschichte des Internationalen Mathematik-Olympiads, mit vierundzwanzig Jahren wurde er einer der jüngsten Professoren an der UCLA, und mit einunddreißig Jahren gewann er die Fields-Medaille.

△ Der 72-jährige Paul Erdős und der 10-jährige Terry Tao. Quelle: Quantamagazine

Im Allgemeinen wird jemand wie er als "Genie-Loner" angesehen.

Aber Terry Tao ist genau das Gegenteil.

Im Vergleich zu Alleinstellungsgeschäften interessiert er sich viel mehr für eine andere Sache:

Können Mathematiker wie Open-Source-Software-Entwickler zusammenarbeiten?

Wenn eine Person A weiß und eine andere Person B weiß, würde es dann möglich sein, neue Dinge zu entdecken, die eine einzelne Person nicht hätte vorhersagen können, wenn man die Kenntnisse beider Personen kombiniert?

Diese Idee hat später seinen gesamten beruflichen Werdegang tiefgreifend beeinflusst.

Im Jahr 2009 nahm er am Polymath-Projekt teil, einem Experiment, das mathematische Kollaboration auf ein öffentliches Forum brachte.

In diesem Projekt konnte jeder sich anmelden, Teilprobleme übernehmen, Ideen einreichen und gemeinsam an Problemen arbeiten.

Probleme, die normalerweise von wenigen Experten Monate oder sogar Jahre dauern würden, wurden in diesem öffentlichen Kollaborationsmodell schnell vorangetrieben.

Dieses Experiment hat schließlich ein Problem in der Kombinatorik gelöst und bewiesen, dass großangelegte Kollaboration in der Mathematik keine Illusion ist.

Das Polymath-Projekt war erfolgreich, aber Terry Tao entdeckte bald ein größeres Problem:

Alle Fehlersuche lag in den Händen des Kernverantwortlichen.

Je mehr Teilnehmer es gab, desto größer war der Prüfungsaufwand; je größer das Kollaborationsmaßstab war, desto höher waren die Organisationskosten.

Ohne automatische Verifizierungstools konnte die Geschwindigkeit der manuellen Fehlerkorrektur nie mit dem Maßstab der Kollaboration Schritt halten. Die Obergrenze der kollaborativen Mathematik war erreicht.

Um diese Grenze zu überwinden, musste man einen anderen Weg finden.

Im Jahr 2014 beschrieb er auf der Bühne der ersten Breakthrough-Preise seine Vision der zukünftigen Mathematik, also drei Vorhersagen, die damals nicht sehr glaubwürdig klangen:

Großangelegte mathematische Kollaborationen mit Hunderten von Teilnehmern würden zur Norm werden;

Computer würden in der Lage sein, mathematische Beweise automatisch zu verifizieren;

LaTeX würde von formalierten Sprachen ersetzt werden, die von Maschinen verstanden werden können.

Heute gesehen entsprechen diese drei Einschätzungen fast allen Hauptlinien der Entwicklung der KI in der Mathematik.

Aber damals klangen sie zu visionär.

Obwohl das Polymath-Projekt gezeigt hat, dass kollaborative Mathematik funktioniert, ist es schwierig, eine echte skalierbare Kollaboration in der mathematischen Forschung zu erreichen, wenn die "Verifizierung" nicht automatisiert werden kann.

Die Lösung, auf die er gewartet hat, war schließlich in einem Werkzeug namens Lean zu finden.

Zehn Jahre lang hat er Vorhersagen gemacht, und jetzt entschied er sich, es selbst auszuprobieren

Der Wendepunkt kam im Jahr 2023.

In jenem Jahr lernte er bei einem Austauschvortrag den Mathematiker Kevin Buzzard kennen, der auch einer der frühen Förderer von Lean war.

Lean ist ein interaktives Theorembeweissystem, das mathematische Beweise in formalisierter Sprache beschreibt und es dem Computer ermöglicht, die Logik jeder einzelnen Schrittzeile zu verifizieren.

Diese Idee traf genau das Problem, über das Terry Tao seit Jahren nachgedacht hatte. Also entschied sich der 48-jährige Terry Tao, auf die Empfehlung von Buzzard hin selbst in die Praxis einzusteigen.

Am 9. Oktober 2023 veröffentlichte er einen Beitrag auf sozialen Medien:

Ich habe beschlossen, endlich mit dem Lernen des interaktiven Beweissystems Lean4 zu beginnen (bei Bedarf mit Unterstützung der KI).

Der Preisträger der Fields-Medaille dachte zunächst, dass es nicht so schwierig sein würde. Also wählte er ein Problem über die Maclaurin-Ungleichung als Übungsprojekt aus, um zu versuchen, den Beweis in Lean zu formalisieren.

Er fertigte zuerst einen 10-seitigen handschriftlichen Beweis an und versuchte dann, ihn in Lean-Code umzuwandeln. Nach seiner Einschätzung sollte es etwa eine Woche dauern.

Dann stieß er auf Schwierigkeiten.

Er stellte fest, dass formalisierte Beweise und das Schreiben von mathematischen Artikeln zwei völlig verschiedene Denkweisen sind.

In einem herkömmlichen Artikel würde niemand viel Aufmerksamkeit auf einen Satz wie "Die Summe dreier Zahlen größer als 1 ist größer oder gleich 3" legen, aber in Lean geht das nicht:

Sie müssen dem System genau sagen, woher die verwendeten Ergebnisse stammen und welchem Lemma sie entsprechen.

Viele Schritte, die scheinbar offensichtlich sind, erfordern eine große Anzahl von formalisierenden Details. Ein paar Zeilen papierliche Ableitungen können leicht in Hunderte von Codezeilen umgewandelt werden.

Einen Monat später absolvierte Terry Tao endlich seinen ersten formalierten Beweis.

Obwohl der Code nicht elegant war, wurde er ab diesem Tag ein echter Teil der formalisierten Mathematik-Community.

PFR-Projekt: Die erste Umsetzung einer Vorhersage

Kurz nachdem er mit dem Lernen von Lean begonnen hatte, gab es eine neue Gelegenheit.

Am 9. November 2023 fertigte Terry Tao zusammen mit seinen Koautoren Ben Green, Tim Gowers und anderen einen Artikel über die PFR-Vermutung ab.

Dies ist ein zahlentheoretisches Problem über die additive Struktur von Mengen, das seit vielen Jahren ungelöst war.

Nachdem der Artikel fertig war, hielt er nicht an. Dann veröffentlichte er einen Beitrag in der Lean-Community:

Hallo zusammen, ich plane, ein Projekt zu starten, um den neuesten Beweis der PFR-Vermutung in Lean4 zu formalisieren... Jeder ist herzlich willkommen, teilzunehmen.

Der größte Unterschied zu Polymath war, dass Lean die Prüfung übernahm.

Diesmal teilte er den Artikel in unabhängige Teilaufgaben auf und öffnete sie für die globale Community.

Jeder absolvierte seine eigene Aufgabe, und das System überprüfte automatisch, ob sie korrekt war. Erst wenn die Aufgabe bestanden war, konnte sie in die Hauptlinie integriert werden.

Das Ergebnis war beeindruckend: Innerhalb von nur drei Wochen war die gesamte formalisierte Arbeit abgeschlossen.

Sogar eine zusätzliche kleine Aufgabe, die er veröffentlichte, wurde von einem Community-Mitglied in weniger als einer Stunde abgeschlossen und eingereicht.

Dies war auch das erste Mal, dass er sah, dass das von ihm vor über einem Jahrzehnt erdachte kollaborative mathematische Modell tatsächlich funktionieren kann.

22 Millionen mathematische Beziehungen, die Mehrheit in 48 Stunden festgestellt

Nachdem er Erfolg hatte, wagte er einen noch größeren Schritt.

Am 25. September 2024 initiierte Terry Tao das Equational Theories-Projekt mit dem Ziel, systematisch die logischen Implikationen zwischen etwa 22 Millionen algebraischen Gleichungen zu bestimmen.

Einfach ausgedrückt, es ging darum, herauszufinden, welche Gleichungen aus welchen anderen Gleichungen abgeleitet werden können.

Diesmal nutzte Terry Tao eine neue Kombination: Die KI half bei der Erstellung von Beweisen, Lean übernahm die Prüfung auf Richtigkeit, und die globale Community von Freiwilligen arbeitete an den spezifischen Problemen. Die drei Parteien arbeiteten zusammen, um das Projekt voranzutreiben.

Arbeitsablauf des automatisierten Beweissystems. Quelle: Quantamagazine

Diesmal kam das Ergebnis noch schneller! Innerhalb von 48 Stunden war die Massensuche fast abgeschlossen, und viele Probleme waren fast gelöst.

Nach neun Tagen war der Gesamtfortschritt auf 99,866 % gestiegen. Am 57. Tag wurde das Hauptprojekt als fast abgeschlossen erklärt, und nur noch 162 Implikationen warteten auf Abschluss.

Sogar während des Projekts wurde ein neues mathematisches Konzept namens magma cohomology (Magma-Kohomologie) entwickelt.

Dieses Konzept ist eine Kohomologietheorie speziell für Magmen ohne Axiomeneinschränkungen. Der Kern besteht darin, die von Gleichungen abhängigen Kohomologiegruppen H¹ und H² zu definieren, die zur Klassifizierung von Magma-Erweiterungen, zur Konstruktion von Gegenbeispielen und zur Unterscheidung verschiedener Magmen verwendet werden. Es ist eine Verallgemeinerung der klassischen Gruppenkohomologie und dient zur Untersuchung der allgemeinsten algebraischen Strukturen.

Außerdem hat Terry Tao sich über die Selbstständigkeit des Equational Theories-Projekts gefreut.

Dank der Unterstützung der KI und der automatischen Prüfung können die Arbeiten auch ohne seine ständige Aufsicht fortgesetzt werden.

In den letzten zwei Jahren hat Terry Tao die KI immer häufiger in seinen Forschungsablauf integriert und auch jungen Wissenschaftlern immer wieder empfohlen, die Fähigkeit zur Kollaboration mit KI zu erwerben.

An Terry Tao kann man sehen, dass der beste Prophet eigentlich der Vorreiter ist –

Er beschränkt sich nicht nur auf die Vorhersage der Zukunft, sondern setzt sich auch aktiv ein und verwandelt allmählich seine Visionen in Realität.

Heute ist dieser Vorreiter auch der festeste Prediger für die KI in der Mathematik.

Referenzlinks:

[1]https://www.quantamagazine.org/how-terry-tao-became-an-evangelist-for-ai-in-math-20260608/

[2]https://terrytao.wordpress.com/2023/