Wovor hat Terence Tao „Angst“?

Wenn KI beginnt, mathematische Beweise in Massenproduktion herzustellen, wovon aus können Menschen sicher sein, dass diese Beweise zuverlässig sind?

Am 9. Oktober Ortszeit in den USA hat der berühmte Mathematiker und Fields-Medaillen-Träger Terence Tao in seinem Blog den Kolumnenartikel von Thomas Hales „Der Lean-Beweiser, den Mathematiker kennen sollten: Zuverlässigkeit und Probleme der künstlichen Intelligenz“ weitergeleitet.

Screenshot des weitergeleiteten Artikels auf Terence Taos Blog

Der Widerspruch dieser Welle der KI-Mathematik liegt darin: KI löst mathematische Probleme mit einer nie dagewesenen Geschwindigkeit, deren Beweise Mathematiker früher Jahre oder sogar Jahrzehnte brauchten, um abzuschließen.

Ein typisches Beispiel ist, dass OpenAI am 6. Oktober auf GitHub auf einmal 722 mathematische Manuskripte veröffentlicht hat, die von internen Modellen erzeugt wurden, die 372 Ergebnisreihen und etwa 4000 Testfragen abdecken.

„Die Mathematiker in meinem Umfeld beschäftigen sich in letzter Zeit alle mit unterhaltsamer Mathematik“, scherzt ein Forscher für Spitzenmodelle, „Alle denken, dass Mathematikforschung keinen Sinn mehr hat, man kann mit KI nicht konkurrieren. Es ist besser, sich mit unterhaltsamer Mathematik zu beschäftigen, Spaß zu haben und Kindern etwas beizubringen.“

Der Forscher fügt hinzu, dass die Mathematikforschung, insbesondere die nicht angewandte Mathematikforschung, ein bestimmtes schwieriges Problem lösen muss, dann Fördermittel und Stipendien beantragt, um die Forschung umzusetzen, nach Erzielung von Teilergebnissen erneut Fördermittel beantragt und die Forschung weiter vorantreibt – und so immer im Kreis läuft. Jetzt löst KI diese „schwierigen Probleme“ jedoch massenhaft.

„Diese „Mathematiker“ haben ihre „schwierigen Probleme“ mitten in der Arbeit verloren. Sie können ihre Arbeiten nicht einmal abschließen. Ganz zu schweigen von der Beantragung nachfolgender Fördermittel“, sagt der Forscher.

Aber dass „schwierige Probleme“ von KI nacheinander überwunden werden, bedeutet nicht, dass Terence Tao sich der unterhaltsamen Mathematik zuwenden wird. Stattdessen ändert sich seine Haltung: Er hat gemeinsam mit 25 Fields-Medaillen-Trägern die Erklärung „Die schwerwiegende Fehlausrichtung der künstlichen Intelligenz in der Mathematik“ initiiert, und gleichzeitig hat die von ihm geleitete „Vereinigung der menschlichen Mathematik“ eine Erklärung veröffentlicht, in der dazu aufgerufen wird, die Zusammenarbeit mit OpenAI einzustellen.

„Er schwankt auch, früher hat Terence Tao die Nutzung von KI für die Mathematikforschung nachdrücklich unterstützt“, sagt der oben genannte Forscher.

01

Problemlösung ist kein knappes Gut mehr

Terence Taos Wandel ist kein Zufall.

Als Fields-Medaillen-Träger und Professor an der Universität von Kalifornien, Los Angeles (UCLA) war Terence Tao bisher ein aktiver Befürworter der Kombination von KI und formaler Mathematik. Da die Ausgabegeschwindigkeit von KI die menschliche Kapazität jedoch vollständig übertrifft, verlagert sich der Fokus des Problems schnell von „Kann KI Probleme lösen?“ zu „Wie sollen wir mit diesen massiv erzeugten Schlussfolgerungen umgehen?“.

Unmittelbar bevor OpenAI diese Manuskripte veröffentlichte, hat Terence Tao auf Mathstodon eine Reihe von Beiträgen veröffentlicht, in denen er die Begriffe „Math 1.0“ und „Math 2.0“ vorschlug.

Er weist darauf hin, dass die traditionelle Mathematik (Math 1.0) großen Wert darauf legt, „wer ein offenes Problem als Erster löst“, auch wenn der ursprüngliche Beweis äußerst schwer verständlich ist.

Wenn dieses Ziel jedoch übermäßig verfolgt wird, bis es nicht mehr nachhaltig ist, muss die mathematische Gemeinschaft die Bewertungsstandards anpassen und mehr Wert auf Erklärung, Gemeinschaftsaufbau und die Erschließung neuer Forschungsrichtungen (Math 2.0) legen, anstatt nur die Geschwindigkeit der Problemlösung zu verfolgen.

Mit anderen Worten: Wenn KI nur massenhaft oberflächliche Ergebnisse ausgibt und Menschen diese Beweise nicht mehr lesen und verstehen können, sogar nicht ihre Richtigkeit bestätigen können, wird der Wert der Mathematik vollständig untergraben.

Seine Wachsamkeit konzentriert sich weiter auf ein grundlegenderes Problem: Wenn Menschen die massiven von KI erzeugten Beweise nicht mehr selbst prüfen, sondern sich vollständig auf Computerprogramme zur Kontrolle verlassen, ist dieser „ultimative Schiedsrichter“ selbst wirklich fehlerfrei?

02

Der „ultimative Schiedsrichter“ Lean und Lücken in der Korrektheit

Hier kommt man nicht umhin, die Kernfigur dieser Welle der maschinellen Überprüfung zu erwähnen: Lean.

Lean ist eine formale Sprache und ein „interaktiver Theorembeweiser“, der von dem Informatiker Leonardo de Moura während seiner Arbeit bei der Microsoft Research initiiert wurde und derzeit in der mathematischen Gemeinschaft weit verbreitet ist.

Einfach ausgedrückt: Wenn die von KI erzeugten mathematischen Papiere als für Menschen lesbare „natürliche Sprache“ betrachtet werden, ist Lean gleichwertig mit einem extrem strengen „logischen Compiler“ oder „Computerschiedsrichter“: Es erfordert, dass mathematische Sprache in präzisen Code übersetzt wird, der von Computern streng erkannt werden kann (also „formaler Code“), und dann prüft der Kernalgorithmus von Lean Zeile für Zeile, ob die Ableitungslogik lückenlos ist.

In der Vergangenheit hat die mathematische Gemeinschaft in der Regel angenommen, dass ein Beweis eine sehr hohe logische Glaubwürdigkeit hat, solange er die Überprüfung von Lean bestanden hat. Dieses Vertrauen wird jedoch derzeit stark erschüttert. Nicht nur zwischen dem formalen Code, der diesen Manuskripten von OpenAI beigefügt ist, und der Ableitung in natürlicher Sprache treten häufig Trennungen zwischen Annahmen und Schritten auf, sondern das größere Problem ist: Die Überprüfungswerkzeuge selbst sind nicht unantastbar.

Im Sommer 2026 hat Lean nacheinander mehrere Korrektheitslücken (Soundness bugs) aufgedeckt, diese Phase wird in der Branche als „Sommer der Lean-Korrektheitslücken“ bezeichnet.

Der auffälligste Vorfall ereignete sich im Juli: Jemand hat mit Unterstützung von KI einen formalen Lean-Beweis veröffentlicht, der behauptet, die Collatz-Vermutung widerlegt zu haben. Dieser Beweis wurde sowohl vom Lean-Kern als auch von einem unabhängigen Prüfer akzeptiert, aber einige Tage später stellte sich heraus, dass er einen Implementierungsfehler des Kerns bei der Verarbeitung von verschachtelten induktiven Typen ausgenutzt hat, sodass das System widersprüchliche Aussagen fälschlicherweise akzeptiert hat. Einen Beweis an den Computer zu übergeben, bedeutet nicht, dass er absolut sicher ist.

Ähnliche Bedenken hinsichtlich der Zuverlässigkeit – Rückzug wegen Symbolfehlern – sind auch bei OpenAI aufgetreten.

Die 722 von Modellen erzeugten mathematischen Manuskripte, die zuvor erwähnt wurden, wurden einen Tag nach ihrer Veröffentlichung bereits von OpenAI in 3 Fällen zurückgezogen.

Der oben genannte Forscher betont, dass OpenAI eigentlich etwas unverantwortlich handelt, „Einige Beweise sind tatsächlich fehlerhaft, nach ihrer Veröffentlichung müssen viele Mathematiker sie trotzdem überprüfen.“

Nach Ansicht dieses Forschers muss man, um einen Satz A zu beweisen, den Satz A formalisieren und dann den Beweis des Satzes A formalisieren. Im Allgemeinen ist der zweite Schritt definitiv korrekt, wenn man ihn mit Lean abgeschlossen und die Überprüfung bestanden hat. Aber es ist möglich, dass der erste Schritt falsch ist – das heißt, sie haben einen falschen Satz korrekt bewiesen.

„Mit vielen Mathematikern zusammenzuarbeiten und sie die Überprüfung übernehmen zu lassen“, meint der oben genannte Forscher, das ist die Verantwortung, die OpenAI übernehmen sollte. Aber in diesem Fall entsteht ein weiteres Paradoxon: Mathematiker „beenden“ die Arbeit der Mathematiker selbst.

03

Gründe, die man nicht verlieren darf, und Schritte, die man nicht aufhalten kann

Der berühmte Mathematiker Hales hat den Artikel „Der Lean-Beweiser, den Mathematiker kennen sollten: Zuverlässigkeit und Probleme der künstlichen Intelligenz“ verfasst. Er leugnet nicht das große Potenzial von KI zur automatischen Generierung und Formalisierung von Beweisen, aber seine echte Sorge lautet: Wenn KI massenhaft formale Beweise erzeugt und sogar tief an der Überprüfung und Reparatur von Überprüfungswerkzeugen selbst teilnimmt, hat die mathematische Gemeinschaft dann noch eine ausreichend solide Grundlage, um zu beurteilen, ob die gesamte Überprüfungskette vertrauenswürdig ist?

In dem Artikel wird eine schärfere Frage aufgeworfen: Da KI bereits an der Schwachstellensuche im Lean-Kern beteiligt war, wie können wir dann beweisen, dass sie während des Scan- oder Reparaturvorgangs keine verborgenen Mängel oder sogar Hintertüren hinterlassen hat?

Was Terence Tao und Hales wirklich wachsam hält, ist nicht, dass KI Sätze schneller beweist als Menschen, sondern dass die Mathematik allmählich den Kernwert verliert, „einen zuverlässigen Grund zu haben, zu glauben, dass die Antwort wahr ist“.

Die Mathematik braucht nicht nur schnellere Ergebnisgenerierung, sondern es muss auch Menschen geben, die diese Ergebnisse erklären, verstehen und dafür verantwortlich sind. Das ist auch einer der Gründe für das von Terence Tao vorgeschlagene „Beweisverdauungsstörung“.

Nach Ansicht des oben genannten Forschers ist das Problem der „Beweisverdauungsstörung, die durch den KI-Boom verursacht wird“ im KI-Zeitalter nicht auf den Bereich der Mathematik beschränkt, viele akademische Bereiche stehen vor dem gleichen Problem: „Die Anzahl der Einreichungen bei ICLR ist dieses Jahr auf 60.000 explodiert.“

Viele Praktiker mit mathematischem Hintergrund geben an, Terence Taos Sorge zu verstehen, aber sie sind auch der Meinung, dass die KI-Welle nicht aufgehalten werden kann.

„Die Mathematik ist einer der Grundsteine der modernen Zivilisation. Einige Vorgehensweisen von Institutionen wie OpenAI werden zu einem Bruch in diesem Bereich führen. Aber der Aufruf, die Zusammenarbeit mit OpenAI einzustellen, ist sinnlos, die Auswirkungen von KI auf alle Bereiche lassen sich nicht aufhalten“, sagt ein Chiphersteller mit mathematischem Hintergrund gegenüber Tencent Tech.

Auf der anderen Seite entwickeln sich die Fähigkeiten der Modelle ständig weiter, KI ist unaufhaltsam, aber das bedeutet nicht, dass Forschung und die physische Welt in kurzer Zeit explodieren werden.

„Stärkere Modelle werden nicht automatisch zu besseren Ergebnissen führen, noch wird die physische Welt mit der gleichen Geschwindigkeit iterieren“, schreibt Feng Yao, Managing Partner von SevenX, in seinem kürzlich erschienenen Interview-Notizbuch über KI in Nordamerika.

Der oben genannte Forscher verweist auf die früher von OpenAI veröffentlichten mathematischen Manuskripte als Beispiel: „Es sieht so aus, als wären mehr als 700 Artikel und Ergebnisse in über 300 Bereichen veröffentlicht worden. Aber es ist sehr wahrscheinlich, dass der Fortschritt für die Gesellschaft am Ende nicht so groß sein wird wie erwartet. Es sieht nach einem großen Boom der Forschungsergebnisse aus, aber kurzfristig wird der Fortschritt für die gesamte Wissenschaft und Technik der Gesellschaft nicht sehr hilfreich sein.“

Man kann sagen, dass Menschen übermäßig ängstlich sind vor dem „falschen Wohlstand“ und der „übertriebenen Substitution“, die KI mit sich bringt.

„Ich vertraue mehr auf menschenzentrierte Forschung, nicht auf ergebniszentrierte Forschung“, fügt der Forscher hinzu, „Ich glaube, dass der Fortschritt der Gesellschaft von Menschen vorangetrieben wird. Das Ziel der Forschung ist auch die Förderung von Menschen, damit Menschen die Entwicklung und den Fortschritt der Gesellschaft vorantreiben können. Forschungsergebnisse sind nur Mittel, der Mensch ist das Ziel.“

Kehren wir zu der Sorge von Mathematikern wie Terence Tao zurück: Da die von KI erzeugten Beweise zunehmend auf maschinelle Überprüfung angewiesen sind, besteht das, was wirklich wachsam sein muss, nicht in der Geschwindigkeit, die durch Rechenleistung gebracht wird, sondern darin, ob Menschen bei der Nutzung dieser Geschwindigkeit noch die Fähigkeit behalten, unabhängig zu beurteilen, ob ein Beweis vertrauenswürdig ist und zu verstehen, warum ein Beweis gültig ist.

Das ist ein neues Thema, dem man sich nicht entziehen kann.

Dieser Artikel stammt aus dem WeChat-Offiziellen Konto „Tencent Tech“, Autor: Sehenswert, veröffentlicht mit Genehmigung von 36Kr.