Gerade eben hat Claude den Großen Fermatschen Satz erstmals bewiesen, das herausragende Genie aus der Yao-Klasse der Tsinghua-Universität hat zugeschlagen.
Gerade eben gibt es wieder eine aufsehenerregende Nachricht im Mathematik-Kreis.
Ein Spitzenfachmann der Yao-Klasse der Tsinghua-Universität hat das Team angeführt und die Große Fermatsche Satz mit Claude vollständig gelöst.
Damit hat die KI den größten Beweis in der Geschichte der Mathematik abgeschlossen.
Früher hat die Große Fermatsche Satz die Menschheit mehr als 350 Jahre lang gequält: Mathematiker mussten Jahre an harter Arbeit aufwenden und 129 Seiten unverständlichen Inhalts schreiben, um sie zu beweisen.
Heute gibt Anthropic bekannt, dass Claude in nur 11 Tagen den ersten end-to-end maschinell überprüften Beweis für die Große Fermatsche Satz abgeschlossen hat!
Dafür hat Claude wahnsinnig 13 Millionen Zeilen Code geschrieben, 30300 überprüfbare Sätze erzeugt, von denen schließlich 29500 angenommen und direkt in den endgültigen Beweis aufgenommen wurden.
Dieses Volumen ist mehr als das Fünffache von Mathlib, der weltweit größten Bibliothek für mathematische Sätze! Außerdem wurden im gesamten Prozess ganze 6 Milliarden Token verbraucht.
Das ist der größte Lean-Beweis, der bisher verfasst wurde.
Sobald die Nachricht veröffentlicht wurde, ist das gesamte Internet in Aufregung geraten. Jemand rief aus: „Die Große Fermatsche Satz wurde in nur einem Monat formalisiert? Diese Art von Kraftprobe lässt die Mathematikwelt wie eine Schnecke aussehen, die kriecht.“
Peng Tianyi, der Spitzenfachmann aus der Yao-Klasse
Ein jahrhundertelanges Rätsel, das 350 Jahre dauerte, wurde von Claude in 11 Tagen gelöst
1637 schrieb der französische Mathematiker Fermat beim Lesen eines Buches spontan eine Zeile in den leeren Rand der Seite:
Wenn die ganze Zahl n > 2 ist, hat die Gleichung xⁿ + yⁿ = zⁿ bezüglich x, y, z keine positiven ganzzahligen Lösungen.
Dann fügte er noch hinzu: „Ich bin überzeugt, dass ich eine wunderbare Beweismethode entdeckt habe, aber leider ist der Platz im Rand zu klein, um sie aufzuschreiben.“
Mit dieser einzigen Zeile quälte er die nachfolgenden Mathematiker mehr als dreihundert Jahre lang bis zur Erschöpfung.
Erst 1995 konnte der britische Mathematiker Wiles mit fortgeschrittenen modernen mathematischen Werkzeugen eine 129-seitige Beweispapier erstellen und damit diesen mehr als 350 Jahre alten unerledigten Fall endgültig abschließen.
Aber das Problem tauchte auf: Der Beweis von Wiles ist wirklich zu kompliziert.
Die moderne Mathematik hat sich bereits zu einem Punkt entwickelt, an dem gewöhnliche Menschen die Aufgabenstellung nicht einmal verstehen können. Einen Satz zu beweisen ist wie das Aufbauen einer überkomplizierten logischen Kette: Sobald ein Glied in der Kette bricht, bricht das Ganze zusammen.
Als Wiles seinen Beweis 1993 zum ersten Mal vorstellte, wurde ein tödlicher Fehler gefunden. Er musste sich dann ein Jahr lang in Abgeschiedenheit quälen, um ihn zu beheben. Bei solchen erstklassigen mathematischen Beweisen brauchen Menschen normalerweise mehrere Monate oder sogar Jahre, um ihre Richtigkeit zu überprüfen.
Gibt es eine Methode, mit der ein Computer wie bei der Überprüfung eines Taschenrechnerergebnisses durch einmaliges Ausführen feststellen kann, ob das Ergebnis richtig ist?
Ja! Das ist die sogenannte „Formalisierung“.
Einfach ausgedrückt: Man schreibt den von Menschen verfassten mathematischen Beweis in eine Programmiersprache, die von Computern ausgeführt werden kann (z. B. Lean), und lässt die Maschine Schritt für Schritt ableiten. Wenn das Programm erfolgreich durchläuft, ist der Beweis absolut korrekt.
Aber die Formalisierung der Großen Fermatsche Satz wird in der Mathematikwelt allgemein als ein riesiges Projekt angesehen, das „in Jahren gemessen“ wird.
Allein das Projekt, das von Professor Kevin Buzzard des Imperial College London geleitet wird, hat bereits eine 86-seitige Blaupause für die erste Phase!
Dann kam Claude.
Für eine Arbeit, für die Menschen voraussichtlich mehrere Jahre brauchen würden, hat es nur 11 Tage gebraucht, und es hat „im Wesentlichen selbstständig gearbeitet“.
13 Millionen Zeilen Code, 6 Milliarden Token
„11 Tage, 13 Millionen Zeilen Code“ – dahinter steckt die doppelte Wirkung aus der brutalen Ästhetik der KI und dem präzisen Systemdesign.
Schauen wir uns an, was Claude genau getan hat:
Es hat nicht nur die Große Fermatsche Satz selbst bewiesen.
Da der formalisierte Beweis von den grundlegendsten Axiomen ausgehen und schicht für schicht nach oben aufgebaut werden muss, hat Claude nebenbei auch mehr als 29000 andere mathematische Sätze bewiesen, die für den Prozess benötigt werden.
Darin sind Bereiche wie Algebra, Geometrie, Zahlentheorie, harmonische Analyse usw. enthalten – viele Teilgebiete wurden zuvor überhaupt nicht formalisiert, und Claude hat sie direkt „neu erschlossen“.
Im gesamten Prozess haben die Menschen kaum eingegriffen.
Die Forscher haben nur einige hochgradige Anweisungen gegeben, zum Beispiel „Die Jacobi-Varietät als Schema hat hohe Priorität“ oder „Schreiten Sie so schnell wie möglich mit dem Satz von Mazur voran“.
Der Rest bestand daraus, dass Dutzende von Claude-Agenten wild miteinander kommunizierten, Begriffe definierten, Zwischensätze bewiesen und diese dann schicht für schicht stapelten.
Schließlich wurde alles vom Lean-Compiler überprüft und akzeptiert, wobei nur drei grundlegendste Standardaxiome verwendet wurden.
Als das Programm durchlief und die Konsole die heilige Meldung „PROVED“ (bewiesen) ausgab, war das interne Protokoll von Claude selbst aufgeregt:
„!!! Der Wurzelknoten der Großen Fermatsche Satz wird als PROVED angezeigt … Das ist das Ziel dieser Kampagne … Ein historischer Moment.“
Man sieht, selbst die KI weiß, wie beeindruckend diese Sache ist.
Der Meister hinter den Kulissen: Ein Spitzenstudent, der aus der „Yao-Klasse“ der Tsinghua-Universität stammt
Wer Claude dazu bringen kann, solch ein Wunder zu vollbringen, ist sicher kein gewöhnlicher Mensch.
Der Leiter ist Peng Tianyi, Assistenzprofessor an der Columbia Business School und Forscher bei Anthropic.
Der Lebenslauf dieses Mannes ist einfach „übermenschlich“:
Von 2013 bis 2017 studierte er im Bachelor-Studium in der „Yao-Klasse“ der Tsinghua-Universität, erhielt die beste Abschlussarbeit und wurde in das nationale Trainingslager für Informatik-Olympiade aufgenommen.
Für das Doktoratsstudium ging er an das MIT im Fachbereich Operations Research und schloss mit einem perfekten GPA von 5,0 ab.
Jetzt arbeitet er sowohl als Assistenzprofessor an der Columbia University als auch bei Anthropic an KI-Agenten und Formalisierungswerkzeugen.
Interessanterweise stammt seine Hartnäckigkeit gegenüber der „automatischen Überprüfung mathematischer Beweise durch KI“ eigentlich aus einer „schmerzhaften Erfahrung“ während seines Bachelor-Studiums.
Damals wollte sein Betreuer die Ergebnisse aus seiner Arbeit in der Zeitschrift *Nature* veröffentlichen, aber er fragte ihn: „Bist du dir zu 100 % sicher, dass der Beweis korrekt ist?“
Er antwortete ehrlich: „Ich bin zu 99 % sicher, aber bei einer so langen Arbeit kann ich nicht zu 100 % sicher sein.“
Wegen dieser 1 % Unsicherheit verpasste er die Chance, in *Nature* veröffentlicht zu werden.
Jetzt hat er diese „1 %“ mit KI eigenhändig beseitigt.
Vom Fehlschlag zum Erfolg: Wie die Plattform Prove2Me die KI rettete
Glauben Sie, dass man eine KI dazu bringen kann, einen Satz zu beweisen, indem man einfach die Anweisung „Bitte beweise die Große Fermatsche Satz“ eingibt, und sie dann sofort 13 Millionen Zeilen Code ausgibt?
Völlig falsch.
Am Anfang wäre das Experiment fast gescheitert.
Anthropic gab bekannt, dass Dutzende von Claude-Agenten in der frühen Phase der Zusammenarbeit bald völlig durcheinander gerieten, wie kopflose Fliegen agierten, nicht mit dem Fortschritt der anderen Schritt halten konnten und die Effizienz der Zusammenarbeit extrem niedrig war. Der Code, der aus frühen fehlgeschlagenen Versuchen stammte, machte am Ende nur 7 % des Gesamten aus.
Die „Vergesslichkeit“ und „Halluzinationen“ von großen Modellen sind vor der strengen Mathematik tödliche Mängel: Eine einzige falsche Zeile macht Millionen von Zeilen danach nutzlos.
In der kritischen Phase entwickelte das Team von Peng Tianyi die Plattform Prove2Me.
Dieses Werkzeug ist wie ein „Super-Projektmanager“ für die KI-Agenten, der alle Probleme löst:
Satz-DAG (Aufgabenbaum): Jede KI erhält eine klare Karte, die ihr sagt, welcher Zwischenknoten als Nächstes bewiesen werden soll. Das lindert die Gedächtnisverschlechterung erheblich, sodass Dutzende von Agenten effizient parallel arbeiten können.
Trennung von Aussage und Beweis: Beschleunigt die Kompilierungsgeschwindigkeit und spart Ressourcen.
Natürlichsprachlicher Index: Jeder Satz hat eine Beschreibung in menschlicher Sprache, sodass die KI die Ergebnisse viel leichter abrufen und wiederverwenden kann.
Mit dem Multi-Agenten-Framework von Claude Code sind die KI-Agenten wie Pioniere mit Navigation, die im mathematischen Labyrinth voranschreiten und das gesamte Level in 11 Tagen abschließen.
Die Mathematikwelt ist überzeugt
Sobald die Ergebnisse veröffentlicht wurden, brach auf X und allen großen technischen Foren eine Welle der Begeisterung aus.
Der Professor des Imperial College, der ursprünglich plante, mehrere Jahre für die Formalisierung aufzuwenden, war nach dem Lesen der Ergebnisse überzeugt und äußerte eine hohe Bewertung: „Das ist ein großer Schritt für die automatische Formalisierung moderner mathematischer Literatur! In Zukunft kann es verwendet werden, um Fehler in menschlichen mathematischen Bibliotheken zu finden und die mathematischen Schlussfolgerungen zu überprüfen, die von großen Modellen erzeugt werden.“
Aber die Vorstellungen der Netznutzer sind noch origineller.
Jemand kommentierte scherzhaft: „Die Art und Weise, wie KI Mathematik löst, ist: Sie gibt dir eine extrem komplizierte Antwort (13 Millionen Zeilen Code). Es ist schwieriger, zu beweisen, dass sie falsch ist, als das Problem selbst zu lösen. Also kannst du nur den Widerstand aufgeben und akzeptieren, dass sie richtig ist. Ist das nicht eine Art PUA in der Mathematikwelt?“
Ein anderer sagte: „13 Millionen Zeilen Code zu schreiben, nur um einen 350 Jahre alten Satz dazu zu bringen, sich vor der Maschine zu beugen … Der menschliche Tisch ist noch nicht bereit, etwas von diesem Ausmaß zu akzeptieren.“
Noch beeindruckender: Anthropic hat nebenbei ein kleines Experiment durchgeführt, um seine Stärke zu demonstrieren.
Mit 3 gewöhnlichen Konten auf Prove2Me wurde in nur 3 Tagen der berühmte „Satz von Winogradow über drei Primzahlen“ in der Zahlentheorie ebenfalls formalisiert!
Das heißt: Mit den passenden Werkzeugen können in Zukunft auch zivile Wissenschaftler mit einigen Konsum-KI-Konten die erstklassigsten mathematischen Sätze der Menschheit überprüfen!
KI wird Mathematiker nicht ersetzen, aber die Mathematik vollständig verändern
Also werden Mathematiker bald arbeitslos?
Anthropic hat offiziell die Antwort gegeben: Sie werden nicht ersetzt, aber die Art und Weise der Arbeit wird vollständig verändert.
In der Geschichte gab es viele „Tragödien“ bei der mathematischen Überprüfung.
Zum Beispiel bewies jemand 1998 die Keplersche Vermutung, das Gutachtergremium brauchte 4 Jahre und konnte am Ende nur sagen, es sei „zu 99 % sicher“. Perelman bewies die Poincaré-Vermutung, die gesamte Mathematikwelt brauchte 4 Jahre, um 3 Bücher mit mehr als 300 Seiten zu schreiben, um sie annähernd zu verstehen. Und manche Sätze wurden jahrelang als Wahrheit akzeptiert, auf denen andere Menschen weitere Erkenntnisse