StartseiteArtikel

AI "Rohe Beweise" überfüllen GitHub, und Terence Tao spricht aus: Nur Problemlösen reicht nicht mehr.

新智元2026-04-30 15:46
[Einleitung] Tao Zhexuan hat jüngst festgestellt, dass die Mathematik aus der Ära des "Mangels an Beweisen" in die Ära des "Überschusses an Beweisen" eintritt. Die wertvollste Arbeit für Mathematiker besteht nicht mehr nur darin, "Beweise zu führen", sondern darin, sie zu überprüfen, zu verstehen und einen "rohen Beweis", den ein KI-System ausspuckt, in Wissen zu verwandeln, das der Mensch tatsächlich verstehen kann.

In letzter Zeit hat Terence Tao auf Mastodon eine gewichtige Einschätzung abgegeben:

Die Mathematik geht aus einer Ära der Beweisskarcität in eine Ära der Beweisüberfluß (from an era of proof scarcity to an era of proof abundance)!

Auf der Github-Seite zur Beitragsliste der KI bei den Erdős-Problemen stapeln sich derzeit über 20 vollständig oder teilweise von KI gelöste Lösungen in der Kategorie „pending assessment“ (warten auf Bewertung).

Davor befand sich in dieser Kategorie normalerweise nur eine oder zwei Lösungen.

Plötzlich produziert die KI mit atemberaubender Geschwindigkeit mathematische Beweise.

Das Problem ist: Es gibt niemanden, der die Zeit hat, sie zu lesen.

Die drei Schritte bei der Problemlösung: Generierung, Verifizierung und Verarbeitung

Tao basiert seine Überlegungen auf einem einfachen Rahmen.

Er sagt, dass die Lösung mathematischer Probleme nie nur eine Aufgabe ist, sondern drei:

  • Beweisgenerierung (Proof generation): Einem Vermutung von „ungelöst“ zu „gelöst“ zu verhelfen.
  • Beweisverifizierung (Proof verification): Sicherzustellen, dass die Lösung richtig ist und keine logischen Lücken hat.
  • Beweisverarbeitung (Proof digestion): Den Beweis zu verstehen, ihn zu erklären und die Methodik daraus zu extrahieren, damit das gesamte Feld davon profitiert.

In den letzten Jahrhunderten wurden diese drei Schritte im Wesentlichen von derselben Person durchgeführt - Wenn man einen Satz bewiesen hat, versteht man ihn natürlich und erklärt ihn in einer Publikation.

Es gab keine „Engpässe“ zwischen diesen drei Schritten.

Aber seit der Ankunft der KI hat sich die Situation geändert.

Der Generierungsschritt wird von Large Language Models (LLMs) stark beschleunigt, der Verifizierungsschritt wird von formellen Werkzeugen wie Lean und Coq abgesichert. Lediglich der Verarbeitungsschritt - der Schritt, in dem das menschliche Gehirn verstehen muss, was der Beweis eigentlich bedeutet - kann nicht mithalten.

Tao verwendet einen präzisen technischen Begriff, um diese Diskrepanz zu beschreiben: Impedanzfehlanpassung (impedance mismatch).

Die Geschwindigkeiten der drei Schritte stimmen nicht überein: Die Beweise strömen wie eine Flut herein, aber der Damm des Verständnisses ist noch von Hand gebaut.

Er sagt, stellen Sie sich zwei Gesellschaften vor.

In einer Gesellschaft mit Nahrungsmittelknappheit sind die am meisten geehrten Personen Jäger und Bauer - diejenigen, die „das Essen nach Hause bringen“ (bring home the bacon).

Wenn Sie ein Reh erlegen, dankt Ihnen die ganze Tribe, egal wie das Fleisch schmeckt. Es werden Leute sein, die Ihnen helfen, es zu waschen, zu kochen und zu verteilen. Fast jeder Nahrungsmittelbeitrag, der nicht giftig ist, wird willkommen geheißen.

In einer Gesellschaft mit Nahrungsmittelüberfluß ist es völlig anders.

Stellen Sie sich eine Potluck-Party vor (ein Essen, bei dem jeder ein Gericht mitbringt). Wenn ein Fremder hereinkommt und ein Stück Fleisch von unbekannter Herkunft hinwirft und die anderen es selbst zu verarbeiten sollen - wird niemand glücklich sein.

Sogar vorgepackte Lebensmittel aus dem Supermarkt werden nur knapp akzeptiert.

Wirklich beliebt sind die Hausmannsküche, die von vertrauenswürdigen Mitgliedern der Gemeinschaft sorgfältig zubereitet wird - nicht nur, weil sie gut schmeckt, sondern auch, weil das Gespräch um das Gericht selbst ein Teil des Soziallebens ist und eine Gelegenheit ist, die nächste Generation von Küchenchefs zu bilden.

Zurück zur Mathematik - der „rohe Beweis“ (raw proof), den die KI produziert, ist wie das mysteriöse Fleisch, das von einem Fremden auf die Party geworfen wird.

Er kann richtig sein. Er kann die formale Verifizierung bestanden haben.

Aber niemand hat ihn gewaschen, gekocht, und niemand kann Ihnen sagen, ob er gut schmeckt.

Tao sagt direkt: Dieser „Beitrag“ fördert nicht wirklich die Lösung des Problems (do not measurably advance the progress), sondern kann sogar einen „negativen Effekt“ haben - er tötet das Interesse daran, das Problem weiter zu untersuchen.

Das Problem wird als „gelöst“ erklärt, aber niemand versteht die Lösung.

Es ist wie ein Gericht, das auf den Tisch gebracht wird, aber niemand wagt es, es zu probieren.

So kühlt das Gericht - zusammen mit allen möglichen Gesprächen und Inspirationen, die daraus entstehen könnten - ab.

Erdős #1196, das einzige Beispiel, bei dem alle drei Schritte abgeschlossen wurden

Theorien müssen anhand von Beispielen getestet werden.

Das Beispiel, das Tao immer wieder erwähnt, ist das Erdős-Problem #1196.

Dies ist eine Vermutung über „primitive Mengen“ (primitive sets): Wenn in einer Menge von ganzen Zahlen kein Element ein anderes Element teilt, dann ist die Summe aller Elemente a nach 1/(a·log a), wenn die Anzahl der Elemente der Menge gegen unendlich geht, annähernd 1?

1968 haben Erdős, Sárközy und Szemerédi diese Vermutung aufgestellt.

In den folgenden fast 60 Jahren haben Mathematiker ständig an der Lösung herangekommen - Der Mathematiker Jared Lichtman von Stanford hat mehrere Jahre gebraucht, um eine zugehörige obere Schranke (etwa 1,399) zu beweisen, aber die endgültige asymptotische Vermutung blieb ungelöst.

Eines Montagabends im April 2026 hat der 23-jährige Liam Price diese Aufgabe in GPT - 5.4 Pro eingegeben.

Price hat keinen Doktortitel in Mathematik und keine jahrelange professionelle Ausbildung. Er nutzt ein ChatGPT Pro-Abonnement für 20 Dollar pro Monat - ein Werkzeug, das jeder nutzen kann.

80 Minuten.

Das Modell hat einen Weg gefunden, den die Mathematikwelt fast 90 Jahre lang übersehen hat: Mit der von Mangoldt-Funktion (eine klassische Gewichtsfunktion in der analytischen Zahlentheorie) in Kombination mit der Markov-Prozesstheorie wurde ein neues Beweisgerüst konstruiert.

Diese technische Kombination existiert seit Jahrzehnten, aber niemand hat bisher daran gedacht, sie auf das Problem der primitiven Mengen anzuwenden.

Der Beweis ist gefunden.

Aber wenn die Geschichte hier enden würde, wäre es nur ein weiteres „mysterioses Fleisch“.

Der entscheidende Punkt ist, was danach passiert: Terence Tao hat persönlich eingegriffen.

Er hat innerhalb von 24 Stunden den Kern des Beweises verifiziert, ihn dann erweitert, neu strukturiert und verfeinert und schließlich eine tiefere Verbindung aufgedeckt - eine bisher unbeschriebene Brücke zwischen der „Anatomie der ganzen Zahlen“ (integer anatomy) und der Markov-Prozesstheorie.

Dies ist die Beweisverarbeitung (proof digestion).

Es geht nicht nur darum, ob der Beweis richtig ist, sondern auch, was er bedeutet.

Tao sagt, dass #1196 derzeit das einzige Beispiel ist, bei dem alle drei Schritte - Generierung, Verifizierung und Verarbeitung - im Wesentlichen abgeschlossen wurden.

Deshalb betont er immer wieder ein Prinzip: Im Idealfall sollten dieselben Personen alle drei Schritte durchführen.

In der Realität geben immer mehr Menschen Beweise ab, die von KI generiert wurden, ohne die Zeit zu haben, sie zu verifizieren und zu verarbeiten.

Dies ist der direkte Grund für die Anhäufung von über 20 noch zu bewertenden Lösungen bei den Erdős-Problemen.

Drei Stellungnahmen, dieselbe Einschätzung

Tao hat nicht einfach nur irgendwo etwas gesagt.

Innerhalb fast derselben Zeit hat er über drei verschiedene Kanäle dasselbe Signal gesendet.

Am 27. April, in einem langen Beitrag auf Mastodon: Er hat offiziell die Paradigma-Einschätzung „Beweisskarcität → Beweisüberfluß“ aufgestellt.

Am 27. April, in einem Interview für Nature (The job description is changing): Er hat dem Journalisten Davide Castelvecchi gesagt, dass die „Aufgabenbeschreibung“ von Mathematikern sich ändert. Ein Student, der sich weigert, KI-Werkzeuge zu nutzen und nur traditionell Beweise erstellen will, wird in Zukunft möglicherweise feststellen, dass seine Chancen immer geringer werden.

Nur diejenigen, die auf der Grundlage ihrer traditionellen mathematischen Kenntnisse neue Werkzeuge beherrschen, werden wirklich erfolgreich sein.

Am 29. März, in einem langen Blogbeitrag „Mathematical methods and human thought in the age of AI“: Er und Klowden haben über ein Jahr lang an diesem Artikel gearbeitet, um über die technischen Details hinauszuschauen und sich mit grundlegenderen philosophischen Fragen auseinanderzusetzen - Was ist die Essenz eines mathematischen Beweises? Was ist der Zweck einer Publikation? Was ist der Sinn unserer Profession?

Er schreibt im Blog: Wenn wir diese Fragen nicht selbst beantworten, werden sie von Technologieunternehmen oder ökonomischen Anreizsystemen für uns beantwortet.

Die drei Stellungnahmen haben denselben Kern: Der Kernkompetenz von Mathematikern verschiebt sich - von „wer zuerst einen Beweis findet“ hin zu „wer das richtige Problem auswählt, den Arbeitsablauf gestaltet, die Ergebnisse verifiziert und verarbeitet“.

Es fehlt nicht mehr an Antworten, sondern an Verständnis.

Eine größere Veränderung: Das akademische Bewertungssystem muss neu geschrieben werden

Wenn sich nur die Arbeitsweise von Mathematikern ändert, ist das noch ein internes Problem einer Disziplin.

Aber Tao sieht weitaus mehr.

Wenn die Kosten für Beweise durch KI nahezu auf Null reduziert werden und die Beweisverifizierung durch formale Engines wie Lean/Coq stark automatisiert wird - wird der Wert des Beweisverarbeitungsschritts neu bewertet.

In der Vergangenheit war die Verarbeitung von Beweisen „kostenlos“.

Wenn man einen Satz bewiesen hat, versteht man ihn natürlich und erklärt ihn in einer Publikation. Diese Arbeit wurde nie separat bewertet.

Aber wenn die Produzenten der Beweise (KI) und die Versteher (Menschen) getrennt werden, wird die Verarbeitung von unsichtbarer Arbeit zu einer sichtbaren knappen Ressource.

Dies bedeutet, dass die gesamte Logik der Verteilung des akademischen Ruhms sich ändern muss.

Das Zitationssystem, die Kriterien für die Begutachtung von Artikeln, die Regeln für die Vergabe von Preisen, sogar die Grundlage für Einstellungen und Beförderungen - all diese Anreizstrukturen, die auf „wer was zuerst bewiesen hat“ basieren, werden einer Umgestaltung bedürfen.

Tao sagt voraus: Genau wie die moderne Gesellschaft rohe Lebensmittel nicht mehr als eine Mahlzeit ansieht, wird die mathematische Forschungsgemeinschaft „rohe, unverarbeitete Beweise“ (raw, undigested proofs) nicht mehr als Lösung für ein Problem ansehen.

Die zukünftigen Bewertungskriterien werden sich darauf konzentrieren, inwie