Terence Tao

Terence Tao (* 17. Juli 1975 in Adelaide, Australien) ist ein australisch-amerikanischer Mathematiker und Professor an der University of California, Los Angeles. Er erhielt 2006 die Fields-Medaille und gilt als einer der einflussreichsten lebenden Mathematiker. Für die KI-Debatte bedeutsam ist er als der prominenteste Fachvertreter, der den Einsatz von KI und Beweisassistenten in der mathematischen Forschung praktisch erprobt und öffentlich einordnet.

Zusammenfassung

Taos Bedeutung für das Thema liegt weniger in einer Position als in einer Praxis: Er arbeitet seit Jahren mit dem Beweisassistenten Lean, leitet Formalisierungsprojekte und dokumentiert seine Erfahrungen mit Sprachmodellen öffentlich.

Daraus ist eine differenzierte Einschätzung entstanden, die weder der Abwehr noch der Begeisterung folgt.

In seiner öffentlichen Vorlesung beim Internationalen Mathematikerkongress im Juli 2026 unter dem Titel Mathematics in the Age of AI fasste er sie zusammen: KI-Systeme sind beim Erzeugen von Beweisen inzwischen stark, das eigentliche Problem verlagert sich auf das, was danach kommt – Prüfung, Darstellung, Veröffentlichung und die Aufnahme in den gesicherten Bestand des Fachs.

Werdegang

Tao wurde 1975 in Adelaide geboren und galt als mathematisches Wunderkind: Mit dreizehn Jahren gewann er als bis dahin jüngster Teilnehmer eine Goldmedaille bei der Internationalen Mathematik-Olympiade. Er promovierte 1996 an der Princeton University bei Elias Stein und wurde 1999 mit 24 Jahren Professor an der UCLA.

Sein Werk erstreckt sich über harmonische Analysis, partielle Differentialgleichungen, Kombinatorik und Zahlentheorie. Bekannt ist insbesondere der gemeinsam mit Ben Green geführte Beweis, dass die Primzahlen beliebig lange arithmetische Folgen enthalten. 2006 erhielt er die Fields-Medaille, 2014 den Breakthrough Prize in Mathematics.

Arbeit mit Beweisassistenten

Seit den frühen 2020er Jahren arbeitet Tao mit Lean, einem quelloffenen Beweisassistenten, der ursprünglich von Leonardo de Moura bei Microsoft Research entwickelt wurde. In einem solchen System wird jeder Beweisschritt maschinell geprüft; ein akzeptierter Beweis ist im Rahmen des zugrunde liegenden Axiomensystems fehlerfrei.

Zu den von ihm geleiteten oder angestoßenen Vorhaben zählen:

• die Formalisierung der polynomialen Freiman-Ruzsa-Vermutung (2023/24), die binnen weniger Wochen mit verteilter Beteiligung gelang;
• das Projekt Equational Theories, das Millionen von Implikationen zwischen algebraischen Gesetzen maschinell prüfte;
• die Formalisierung seines eigenen Lehrbuchs Analysis I;
• eine gemeinsam mit Alex Kontorovich gestellte Aufgabe zur Formalisierung des Primzahlsatzes, die 2026 von einem KI-gestützten System gelöst wurde.

Sein Argument für diese Arbeit ist arbeitsteilig: Formale Prüfung ermöglicht Zusammenarbeit in Größenordnungen, die in der Mathematik bislang unüblich waren, weil niemand mehr die Korrektheit der Beiträge anderer selbst nachvollziehen muss.

Position zu KI

Taos Einschätzung hat sich mit der Entwicklung verschoben und ist gut dokumentiert.

Der Kernvorbehalt. Er benennt als größte Schwäche der Systeme, dass sie Fehler machen, die sich nicht überprüfen lassen. In der Mathematik entfällt dieser Nachteil weitgehend, weil Beweise formal geprüft werden können – deshalb hält er das Fach für einen besonders geeigneten Anwendungsbereich.

Die Verschiebung des Engpasses. Bei seiner ICM-Vorlesung 2026 unterschied Tao fünf Stufen mathematischer Arbeit jenseits des ersten Lösens: Beweiserzeugung, Prüfung, Darstellung, Veröffentlichung und Aufnahme in den Bestand des Fachs.

KI-Systeme sind bei der ersten Stufe inzwischen leistungsfähig und machen bei der zweiten Fortschritte. Damit entsteht, was in der Diskussion als Beweisfülle bezeichnet wurde: Die Erzeugung ist nicht mehr das Nadelöhr – das Schwierige beginnt danach.

Er verwies dabei auf einen Versuch vom Mai 2026, bei dem vier KI-Systeme gegen zehn neuartige Forschungsprobleme antraten und für sieben davon mindestens eine Lösung in Veröffentlichungsqualität erzeugten.

Menschliches Verstehen. Tao betont, dass ein geprüfter Beweis nicht dasselbe ist wie Verstehen. Die Frage, warum ein Satz gilt und wie er sich in den Zusammenhang des Fachs fügt, bleibt bestehen – auch wenn die Herleitung maschinell erfolgte.

Umbruch des Fachs. Beim Kongress 2026 beschrieb er die Mathematik als in einer Umbruchphase, die er als Krise ihrer Grundlagen und Arbeitsweisen bezeichnete. Anders als Jacob Tsimerman, der daraufhin in die KI-Sicherheitsforschung wechselte, bleibt Tao in der Mathematik und arbeitet an der Frage, wie sich die Werkzeuge in das Fach einfügen lassen.

Einordnung

Tao ist in der Debatte eine ungewöhnliche Instanz, weil er weder als Anbieter noch als Kritiker auftritt, sondern als Anwender, der seine Erfahrungen offenlegt. Seine Einschätzungen werden entsprechend von beiden Seiten herangezogen – als Beleg für die Leistungsfähigkeit der Systeme wie für deren Grenzen.

Bemerkenswert ist seine Konsequenz: Die Verbindung von Sprachmodellen mit formaler Prüfung behebt genau die Schwäche, die er als deren größte benennt. Damit ist die Mathematik zugleich Anwendungsfeld und Testfall für die allgemeinere Frage, ob sich unzuverlässige Erzeugung durch zuverlässige Prüfung nutzbar machen lässt – eine Frage, die auch für die KI-Sicherheitsforschung offen ist.

Verwandte Begriffe

• Formale Verifikation – Verfahren, mit dem er arbeitet
• Lean – von ihm verwendeter Beweisassistent
• mathlib – Bibliothek formalisierter Mathematik
• Jacob Tsimerman – Fields-Medaillist 2026, der in die KI-Sicherheit wechselte
• AlphaProof – KI-System zur formalen Beweisführung
• Chain-of-Thought – Grundlage der Beweiserzeugung durch Sprachmodelle
• Halluzination – die von ihm benannte Kernschwäche
• Reasoning-Modelle – Modellklasse, die in der Mathematik eingesetzt wird
• AGI – Zielbegriff, zu dessen Nähe er sich zurückhaltend äußert

Quellenangaben

1. de Moura, Leonardo / Ullrich, Sebastian (2021): The Lean 4 Theorem Prover and Programming Language. In: CADE-28, LNCS 12699, S. 625–635.
2. Tao, Terence (2025): Machine-Assisted Proof. In: Notices of the American Mathematical Society 72 (1), S. 6–13.
3. Tao, Terence (2026): Mathematics in the Age of AI. Öffentliche Vorlesung, International Congress of Mathematicians, Philadelphia, 24. Juli 2026.
4. Tao, Terence / Dillies, Yaël u. a. (2024): Formalization of the Polynomial Freiman-Ruzsa Conjecture. Lean-4-Projekt.
5. Tao, Terence / Green, Ben (2008): The Primes Contain Arbitrarily Long Arithmetic Progressions. In: Annals of Mathematics 167 (2), S. 481–547.
6. Tao, Terence, laufend. Terence Tao on AI – a living summary. https://teorth.github.io/tao-web/ai-views.html

← Zurück zur Lexikon-Übersicht

Zuletzt bearbeitet: 10. August 2026

Zusammengestellt, formuliert, lektoriert und korrigiert mit KI-Unterstützung. Kuratiert von Nils Brauer. Alle Angaben ohne Gewähr.