Ein Beweis, für dessen Erstellung ein Mathematiker sieben Jahre brauchte und für dessen Formalisierung ein anderer Forscher voraussichtlich fünf Jahre veranschlagte, wurde nun von einem Team aus KI-Agenten in elf Tagen fertiggestellt. Das Claude-Modell von Anthropic hat eine formale Version des Großen Fermatschen Satzes erstellt, eines der berühmtesten Probleme in der Geschichte der mathematischen Wissenschaften. Dies ist kein neuer Beweis. Es ist etwas, das weitaus nützlicher ist: eine maschinenlesbare und maschinell verifizierte Bestätigung, dass der menschliche Beweis korrekt ist, aufgebaut von Grund auf in einer Programmiersprache namens Lean.
Ein 350 Jahre altes Problem und was „Formalisierung“ eigentlich bedeutet
Der Große Fermatsche Satz besagt, dass keine ganzen Zahlen a, b und c die Gleichung aⁿ + bⁿ = cⁿ erfüllen können, wenn n eine ganze Zahl größer als 2 ist. Pierre de Fermat warf dieses Rätsel im 17. Jahrhundert auf und bemerkte berühmt in einem Rand eines Lehrbuchs, er habe einen Beweis gefunden, doch der Raum sei zu klein, um ihn aufzuschreiben. Diese Notiz verfolgte die Mathematik etwa dreieinhalb Jahrhunderte lang.
Andrew Wiles bewies den Satz schließlich im Jahr 1995, nachdem er sieben Jahre lang im geheimen an dem Problem gearbeitet hatte. Sein Beweis war nicht frei von Schwierigkeiten: Ein Fehler wurde entdeckt, und es dauerte rund ein Jahr, bis Wiles und sein Kollege Richard Taylor diesen behoben hatten. Diese Episode veranschaulicht eine strukturelle Anfälligkeit in traditionellen mathematischen Beweisen. Sie sind in natürlicher Sprache und logischer Notation verfasst, werden von menschlichen Experten überprüft und sind anfällig für Fehler, die sich in langen Argumentationsketten verstecken können.
Die Formalisierung begegnet dieser Anfälligkeit direkt. Sie bedeutet, dass ein Beweis in Computercode übersetzt wird, genauer gesagt in eine formale Sprache, die eine Maschine Schritt für Schritt verifizieren kann. Im Code gibt es keine Mehrdeutigkeit. Entweder hält die Logik stand oder eben nicht. Ein zentrales Repository namens Mathlib speichert bereits rund 2 Millionen Zeilen an formalisierter Mathematik. Der neue Beweis von Anthropic fügt dieser Landschaft 13 Millionen Zeilen hinzu und deckt dabei etwa 29.500 Zwischensätze ab, die für das Erreichen des Endergebnisses notwendig waren. Damit ist er mehr als fünfmal so groß wie der gesamte bisherige Mathlib-Inhalt zusammen und der größte Lean-Beweis, der jemals geschrieben wurde.
Wie die Agenten tatsächlich gearbeitet haben (und wo sie zu kämpfen hatten)
Das System von Anthropic nutzte kein einzelnes KI-Modell, das isoliert arbeitete. Mehrere separate Agenten wurden eingesetzt, von denen jeder bestimmten Teilen des Problems zugewiesen war, um kleinere Brocken des Satzes parallel zu bearbeiten. Der Prozess lief elf Tage lang kontinuierlich und autonom ab.
Menschliche Experten waren nicht abwesend. Sie lieferten das, was Anthropic als „High-Level-Anweisungen“ bezeichnet, um die Arbeit auf Kurs zu halten. Das ist erwähnenswert: Die Agenten verloren zeitweise den Überblick über den Gesamtzustand des Projekts und hörten auf, effektiv zusammenzuarbeiten. Das System benötigte externe Anleitung, um sich von diesen Zusammenbrüchen zu erholen. Was letztlich half, war ein Tool, das ursprünglich für die menschliche mathematische Zusammenarbeit entwickelt wurde und Prove2Me heißt. Sobald die Agenten begannen, es zur Nachverfolgung ihrer Arbeit und zur Koordination der nächsten Schritte zu nutzen, kam das Projekt zuverlässiger voran.
Kevin Buzzard, ein Mathematiker am Imperial College London, der ein fünfjähriges Projekt zur Formalisierung desselben Wiles-und-Taylor-Beweises geleitet hatte, äußerte sich zu dem Ergebnis. Er stellte fest, dass der Beweis auf „keinen anderen Annahmen als den Axiomen der Mathematik“ beruht, und beschrieb die Arbeit als vielschichtig, die Algebra, harmonische Analyse, Geometrie und Zahlentheorie berühre. Seine Einschätzung ist bedeutsam: Buzzard war kein unbeteiligter Zuschauer. Er hatte Anfang dieses Jahres eine Konferenz in London organisiert, auf der KI-Experten, Informatiker und Mathematiker zusammenkamen, um genau an diesem Problem zu arbeiten. Die Ankündigung von Anthropic hat diese Bemühungen komplett überholt.
Warum das über den Satz selbst hinaus von Bedeutung ist
Hier ist, was die meiste Berichterstattung über diese Geschichte übersieht. Der Satz selbst ist nicht der Punkt. Der Große Fermatsche Satz war bereits bewiesen. Was Anthropic demonstriert hat, betrifft etwas über die Natur des mathematischen Wissens und wie es verifiziert, erweitert und darauf aufgebaut werden kann.
Buzzard brachte es auf den Punkt: Wenn KI nun einen Beweis dieser Komplexität automatisiert formalisieren kann, dann wird die automatische Formalisierung der breiteren modernen mathematischen Literatur zu einem realistischen Nahziel. Das ist eine signifikante Verschiebung. Die Mathematik ist das Fundament der Physik, Kryptographie, Informatik und des Ingenieurwesens. Ein formalisierter, maschinell verifizierbarer Bestand an mathematischem Wissen würde es Forschern ermöglichen, mit viel größerem Vertrauen auf früheren Ergebnissen aufzubauen, Fehler abzufangen, die eine menschliche Überprüfung übersehen könnte, und das Tempo zu beschleunigen, mit dem neue Ergebnisse erzielt werden können.
Die Episode veranschaulicht zudem etwas Wichtiges darüber, wie KI-Systeme derzeit bei intellektueller Arbeit mit hohem Einsatz agieren. Sie sind nicht in der Weise autonom, wie das Wort manchmal lose verwendet wird. Sie erforderten menschliche Aufsicht, brachen bei der Koordination zusammen und benötigten Tools, die für die menschliche Zusammenarbeit entwickelt wurden, um effektiv zu funktionieren. Der elftägige Zeitrahmen ist bemerkenswert. Die Notwendigkeit menschlicher Anleitung während des gesamten Prozesses ist gleichermaßen lehrreich.
KI ersetzt hier keine Mathematiker. Sie bewältigt ein Volumen und eine Granularität logischer Verifikation, die kein menschliches Team in diesem Maßstab aufrechterhalten könnte, wodurch Forscher den Kopf frei haben für die übergeordneten Fragen danach, was bewiesen werden soll und warum das wichtig ist.
Kurz gefasst
Die KI-Agenten von Anthropic haben den größten formalen Beweis erstellt, der jemals geschrieben wurde, und den Großen Fermatschen Satz in maschinenlesbarem Lean-Code über 13 Millionen Zeilen und 29.500 Zwischenschritte verifiziert. Das Ergebnis ist weniger als mathematische Entdeckung von Belang, sondern vielmehr als Demonstration, dass KI nun komplexe, vielschichtige Beweise in einem Ausmaß und einer Geschwindigkeit formalisieren kann, die zuvor unerreichbar waren. Der Prozess erforderte menschliche Anleitung und brach mehr als einmal zusammen. Dieser Kontext gehört ebenfalls in die Geschichte.
Basierend auf Berichten von New Scientist.