Die KI Claude hat Fermats letztes Theorem in nur 11 Tagen vollständig autonom im Proof Assistant Lean formalisiert.
Ein Multi-Agenten-Setup generierte dabei 13 Millionen Zeilen Lean-Code und über 29.500 maschinenprüfbare Zwischentheoreme.
Der vollständige formale Beweis ist als Open-Source-Codebasis auf GitHub für die Forschungsgemeinschaft verfügbar.
Das KI-Unternehmen Anthropic hat Anfang September 2026 den ersten vollständig computergeprüften Lean-Beweis von Fermats letztem Satz veröffentlicht, der die automatisierte formale Verifizierung komplexer logischer Ketten massiv beschleunigt. Im Zentrum dieses Durchbruchs steht ein agentisches Setup, das laut Anthropic in Rekordzeit eine historische mathematische Leistung in maschinenlesbaren Code übersetzt hat.
Die Neuerungen im Detail
Für das Projekt nutzte Anthropic ein Multi-Agenten-Setup auf Basis von Claude Code, das auf der kollaborativen Plattform ‚Prove2Me‘ operierte. Die nackten Zahlen des Projekts setzen neue Maßstäbe für KI-generierte Mathematik:
Zeitaufwand: Die vollständige Formalisierung dauerte lediglich 11 Tage.
Code-Volumen: Das System produzierte rund 13 Millionen Zeilen Lean-Code. Ohne generierten Boilerplate-Code bleiben laut Anthropic immer noch 10,5 Millionen Zeilen übrig.
Mathematische Tiefe: Der Beweis stützt sich auf exakt 29.511 Theoreme und etwa 533.000 unterstützende Lemmas.
Rechenleistung: Für die Generierung wurden schätzungsweise 6 Milliarden Output-Tokens verarbeitet.
Der Beweis beruht ausschließlich auf den drei Standardaxiomen des Proof Assistants Lean. Die KI folgte dabei der klassischen Beweisroute der Mathematiker Andrew Wiles und Richard Taylor und bettete die Ergebnisse nahtlos in die bestehende Mathematik-Infrastruktur von Lean und Mathlib ein. Zum Vergleich: Das generierte Projekt ist laut Berichten mehr als fünfmal so groß wie die gesamte bisherige Mathlib-Bibliothek.
Warum das wichtig ist
Der wahre Durchbruch liegt nicht in der Entdeckung neuer Mathematik, sondern in der massiven Skalierung der Code-Formalisierung durch KI. Fermats letztes Theorem ist seit den 1990er Jahren bewiesen. Die eigentliche Sensation ist, dass autonome KI-Agenten nun in der Lage sind, mehrwöchige bis mehrmonatige formale Mathematikarbeit auf wenige Tage zu verdichten.
Dies ist ein entscheidender Gamechanger für die Softwareentwicklung und IT-Sicherheit. Formale Beweise gelten als der Goldstandard für hochzuverlässige, maschinenprüfbare Systeme. Wenn KI-Modelle komplexe logische Ketten autonom verifizieren können, lassen sich menschliche Review-Prozesse in der Software-Verifizierung künftig drastisch abkürzen.
Gleichzeitig bedient Anthropic hier ein klares Narrativ im Wettstreit mit OpenAI und Google:
Das Projekt demonstriert eindrucksvoll, dass Claude in extrem langen, stark strukturierten Forschungsaufgaben fehlerfrei skalieren kann, ohne in Halluzinationen abzugleiten.
Dennoch gibt es in der Entwickler-Community auch kritische Stimmen. Auf Plattformen wie Hacker News wird die Schlagzeile von 13 Millionen Zeilen teilweise als irreführender journalistischer Hook betrachtet, da maschinell generierter Lean-Code naturgemäß viel Boilerplate-Struktur enthält. Experten betrachten daher die Anzahl der 29.511 formalen Zwischenresultate als die weitaus aussagekräftigere Metrik für die Leistung des Modells.
Verfügbarkeit & Fazit
Anthropic hat den vollständigen, von Lean verifizierten Beweis in einem öffentlichen GitHub-Repository zugänglich gemacht. Damit steht die gigantische Codebasis der Forschung und Entwicklern kostenfrei zur Verfügung. Auch wenn Claude hier kein ungelöstes Mathe-Rätsel geknackt hat, markiert die Arbeit einen historischen Meilenstein für die KI-gestützte formale Verifizierung und beweist die Praxistauglichkeit von Multi-Agenten-Systemen für hochkomplexe Logik-Aufgaben.
FAQ
Hat Claude ein neues mathematisches Problem gelöst?
Nein. Fermats letztes Theorem wurde bereits in den 1990er Jahren von Andrew Wiles bewiesen. Claudes Leistung besteht darin, diesen bestehenden menschlichen Beweis in eine formale, maschinenlesbare Sprache (Lean) übersetzt zu haben, die von Computern Ende-zu-Ende auf logische Fehlerlosigkeit geprüft werden kann.
Warum ist die Zahl von 13 Millionen Codezeilen umstritten?
In der Tech-Community wird angemerkt, dass maschinell generierter Code in Proof Assistants wie Lean sehr viel Boilerplate und repetitive Struktur enthält. Anthropic selbst gibt an, dass der Kerncode ohne diese Strukturen etwa 10,5 Millionen Zeilen umfasst. Die Anzahl der bewiesenen Theoreme gilt als besserer Maßstab.
Was bedeutet dieser Durchbruch für die Softwareentwicklung?
Die Fähigkeit von KI, komplexe logische Ketten formal zu verifizieren, lässt sich direkt auf die Softwareentwicklung übertragen. Künftig könnten ähnliche Multi-Agenten-Setups genutzt werden, um sicherheitskritische Software-Systeme automatisiert auf Schwachstellen zu prüfen und menschliche Code-Reviews massiv zu beschleunigen.
Florian Schröder ist Gründer von AI Rockstars, KI-Stratege und Prompt Engineer. Er berät Unternehmen bei der praktischen Implementierung von generativer KI und Automation.
Wir verwenden Technologien wie Cookies, um Geräteinformationen zu speichern und/oder darauf zuzugreifen. Wir tun dies, um das Surferlebnis zu verbessern und um personalisierte Werbung anzuzeigen. Wenn Sie diesen Technologien zustimmen, können wir Daten wie das Surfverhalten oder eindeutige IDs auf dieser Website verarbeiten. Wenn Sie Ihre Zustimmung nicht erteilen oder zurückziehen, können bestimmte Funktionen beeinträchtigt werden.
Funktional
Immer aktiv
Die technische Speicherung oder der Zugang ist unbedingt erforderlich für den rechtmäßigen Zweck, die Nutzung eines bestimmten Dienstes zu ermöglichen, der vom Teilnehmer oder Nutzer ausdrücklich gewünscht wird, oder für den alleinigen Zweck, die Übertragung einer Nachricht über ein elektronisches Kommunikationsnetz durchzuführen.
Vorlieben
Die technische Speicherung oder der Zugriff ist für den rechtmäßigen Zweck der Speicherung von Präferenzen erforderlich, die nicht vom Abonnenten oder Benutzer angefordert wurden.
Statistiken
Die technische Speicherung oder der Zugriff, der ausschließlich zu statistischen Zwecken erfolgt.Die technische Speicherung oder der Zugriff, der ausschließlich zu anonymen statistischen Zwecken verwendet wird. Ohne eine Vorladung, die freiwillige Zustimmung deines Internetdienstanbieters oder zusätzliche Aufzeichnungen von Dritten können die zu diesem Zweck gespeicherten oder abgerufenen Informationen allein in der Regel nicht dazu verwendet werden, dich zu identifizieren.
Marketing
Die technische Speicherung oder der Zugriff ist erforderlich, um Nutzerprofile zu erstellen, um Werbung zu versenden oder um den Nutzer auf einer Website oder über mehrere Websites hinweg zu ähnlichen Marketingzwecken zu verfolgen.
