Anthropic gibt an, dass seine KI Claude den ersten vollständig computergeprüften Beweis des Großen Fermatschen Satzes erstellt hat – in 11 Tagen, weitgehend eigenständig, und damit den längsten mathematischen Beweis überhaupt hervorgebracht.

Ein von Menschen geleitetes Projekt am Imperial College London arbeitet seit 2024 an exakt derselben Aufgabe und ist noch nicht annähernd fertig. Claude war schneller. Kevin Buzzard, der Mathematiker, der das Imperial-Projekt leitet, überprüfte Claudes Beweis und bestätigte, dass er ausschließlich mit den grundlegendsten logischen Regeln der Mathematik standhält.

Laut Anthropic schrieb Claude den längsten je erstellten mathematischen Beweis und nutzte ihn, um den Großen Fermatschen Satz formal zu beweisen – ein Problem, das Mathematiker 358 Jahre lang vor Rätsel stellte. Die KI erledigte dies in 11 Tagen, größtenteils eigenständig, und produzierte 13 Millionen Zeilen Code, die ein Computer Zeile für Zeile prüfen kann, statt auf das Wort eines Mathematikers vertrauen zu müssen.

Der Große Fermatsche Satz besagt, dass es keine drei positiven ganzen Zahlen gibt, die jeweils mit einem Exponenten größer als 2 potenziert werden können, sodass die ersten beiden die dritte ergeben. Pierre de Fermat notierte diese Behauptung 1637 in den Rand eines Mathe­matikbuchs und fügte hinzu, er verfüge über einen „wahrhaft wunderbaren Beweis“, für den der Rand jedoch zu klein sei. Dann starb er. Die Mathematiker verbrachten die folgenden 358 Jahre damit, zu rekonstruieren, was er wohl im Sinn gehabt hatte.

Beweisen und Prüfen sind zwei verschiedene Dinge

Ein mathematischer Beweis ist eine Kette logischer Schritte – bricht ein Glied, kollabiert das Ganze. Dieses eine fehlerhafte Glied, irgendwo in hundert Seiten dichtem Argument verborgen, zu finden, kann anderen Mathematikern Jahre ihres Lebens kosten.

Die Formalisierung eines Beweises bedeutet, ihn in eine derart wörtliche Sprache zu übersetzen, dass ein Computer jeden Schritt selbstständig überprüfen kann, ohne in subjektive Bewertungen zu geraten.

Mit der Verifikation tun sich Mathematiker schon lange schwer. Ein deutscher Preis von 1908 – heute rund 1 bis 2 Millionen Dollar wert, ausgelobt für den ersten gültigen Beweis des Satzes – zog allein im ersten Jahr 621 falsche Einsendungen an.

Wie Anthropic auf X schrieb:

Checking that a major mathematical proof is correct can take years. Formalization—converting the mathematical reasoning into a form computer proof assistants like Lean can verify—can help. Last month, Claude completed the first formalized proof of Fermat's Last Theorem, one of… pic.twitter.com/pdT8zwlV4A

— Anthropic (@AnthropicAI) September 4, 2026

Der eigentliche Beweis erschien erst 1995 durch den britischen Mathematiker Andrew Wiles – und mit einer Wendung. Wiles kündigte seine Lösung in drei Vorlesungen im Juni 1993 an, bis ein Gutachter später eine Lücke darin fand. Er verbrachte fast ein Jahr damit, sie mit seinem ehemaligen Studenten Richard Taylor zu beheben, war kurz davor aufzugeben und veröffentlichte schließlich im Mai 1995 einen korrigierten, 129-seitigen Beweis. Dieser stützte sich auf Mathematik, die zu Fermats Lebzeiten nicht existierte – ein wesentlicher Grund, warum Mathematiker heute daran zweifeln, dass Fermats „wunderbarer Beweis“ jemals funktionieren konnte.

Computerverifizierte Mathematik selbst ist Jahrzehnte alt. Der erste berühmte Fall war der computerunterstützte Beweis des Vier-Farben-Satzes von 1976, der eine bis heute andauernde Debatte darüber auslöste, ob ein Beweis, den kein Mensch vollständig von Hand nachlesen kann, als solcher gelten soll. Formale Beweissprachen wie Lean – entwickelt von Leonardo de Moura, ursprünglich bei Microsoft Research – entstanden genau aus dieser Spannung: Die Software übernimmt das Prüfen, sodass Menschen dem Ergebnis dennoch vertrauen können.

Im Jahr 2024 startete Kevin Buzzard vom Imperial College London ein Projekt mit exakt dem Ziel, das Claude gerade erreicht hat: Wiles' Beweis in Lean zu übersetzen, eine Sprache, die Computer prüfen können. Es ist die Art von Aufgabe, die ein Heer freiwilliger Mathematiker erfordert – die Projektskizze selbst umfasst 86 Seiten, und die Finanzierung ist bis 2029 gesichert. Claude erledigte das Ganze in 11 Tagen.

Wie Claude es tatsächlich geschafft hat

Anthropic erläutert in einem ausführlicheren Beitrag, dass Tianyi Peng, der an der Columbia University mit einem Team KI-Formalisierungswerkzeuge entwickelt, herausfinden wollte, wie weit Claude eigenständig kommen kann. Dutzende Claude-Agenten arbeiteten parallel, schrieben Definitionen, bewiesen kleine Resultate und bauten diese zu größeren auf – mit fast keiner menschlichen Beteiligung außer gelegentlichen Hinweisen wie „priorisiere als Nächstes dieses Theorem“.

Anfangs lief es nicht reibungslos. Die Agenten verloren früh den Überblick über bereits Bewiesenes und hörten auf zu kooperieren; diese Fehlversuche machen noch immer etwa 7 % der Zeilen im endgültigen Beweis aus.

Abhilfe schuf ein Werkzeug namens Prove2Me, ebenfalls von Pengs Team entwickelt, das jedem Agenten dieselbe Live-To-do-Liste der noch ausstehenden kleineren Beweise gab, sodass niemand Arbeit duplizierte oder abschweifte. Es organisierte zudem die Dateien, damit Lean alles schneller prüfen konnte, und führte Notizen in einfachem Englisch zu jedem Resultat, damit Agenten die Arbeit anderer wiederverwenden statt sie neu erfinden konnten.

Am Ende hatte Claude mehr als 30.000 unterstützende Theoreme bewiesen und Milliarden von Tokens verbraucht – auf einem Forschungsmodell, das laut Anthropic in etwa Claude Fable 5.1 entspricht, der Version, die das Unternehmen später veröffentlichte. Der fertige Beweis umfasst 13 Millionen Zeilen – mehr als fünfmal so groß wie Mathlib, die gemeinsame Bibliothek, die Mathematiker für solche Arbeiten bereits nutzen.

Ein typischer Roman umfasst 80.000 Wörter. Claudes Beweis entspricht 160 Romanen voller rein logischer Argumentation.

Ist das wirklich bedeutsam?

Buzzard – dessen eigene Version dieses Projekts bis 2029 finanziert ist – überprüfte Claudes Beweis und segnete ihn ab, mit der Aussage, er beweise den Satz „with no assumptions other than the axioms of mathematics“ (ohne Annahmen außer den Axiomen der Mathematik).

Das ist nicht dasselbe wie wenn Claude völlig neue Mathematik entdeckt hätte – was Anthropic in diesem Jahr auch mit seiner Kryptografieforschung beanspruchte. Wiles bewies den Fermatschen Satz bereits vor drei Jahrzehnten – Claude erstellte lediglich eine maschinell prüfbare Bestätigung dafür. Das ist bedeutsam, weil Mathematiker zunehmend von unverifizierten Beweisen überschwemmt werden, darunter KI-generierte, die schneller eintreffen, als Menschen sie von Hand prüfen können. Solche formalisierten Beweise sind zudem deterministisch und anfällig für keine menschlichen Fehler – was in der Mathematik sehr wichtig ist.

Das ist kein neues Problem. Ein computerunterstützter Beweis der Kepler-Vermutung brauchte vier Jahre, bis sich ein Prüfungsgremium nur zu „99 % sicher“ erklären wollte, und Grigori Perelmans Beweis der Poincaré-Vermutung brauchte etwa genauso lange, um vollständig verstanden zu werden.

Wer Anthropics Wort nicht nehmen möchte, muss das auch nicht. Der vollständige Beweis mit 13 Millionen Zeilen liegt jetzt auf GitHub – frei zugänglich für jeden Mathematiker mit genug Zeit, ihn Zeile für Zeile zu zerpflücken.