13 Millionen Zeilen Lean: KI formalisiert Fermat-Beweis
Anthropic legt eine maschinell geprüfte Fassung von Wiles' Beweis vor – erstellt von Claude-Agenten in 11 Tagen, mit rund 29.500 Zwischentheoremen.
Symbolbild: In einem Rechenzentrum schiebt eine Person ein Servermodul in ein Rack, während Statusleuchten einen laufenden Prüfdurchlauf anzeigen.
Nein, eine KI hat Fermats letzten Satz nicht neu bewiesen – Claude-Agenten haben Andrew Wiles' Beweis von 1995 in 13 Millionen Zeilen Lean-Code übersetzt, den ein Rechner Schritt für Schritt nachprüfen kann.
Auf einen Blick
- 13 Millionen Zeilen Lean-Code und rund 29.500 Zwischentheoreme, erzeugt in 11 Tagen von Dutzenden Claude-Agenten.
- Rechenaufwand: rund 6 Milliarden Output-Token, von Anthropic auf 100.000 bis 300.000 US-Dollar geschätzt.
- Vorlage war nicht Wiles' 129-seitiges Original, sondern die vereinfachte Darstellung von Darmon, Diamond und Taylor.
- Kevin Buzzard vom Imperial College London kompilierte den Code selbst; er nutzt nur die drei Standardaxiome von Lean.
- Buzzards eigenes FLT-Projekt läuft seit 2024, ist bis 2029 finanziert und hat einen Blueprint von 86 Seiten.
Anthropic hat nach eigenen Angaben erstmals eine vollständig maschinell geprüfte Fassung von Fermats letztem Satz vorgelegt. Erzeugt haben sie Dutzende Claude-Agenten, die den Beweis in die Sprache des Beweisassistenten Lean übertrugen. Herausgekommen sind 13 Millionen Zeilen Code mit rund 29.500 Zwischentheoremen. Neue Mathematik steckt darin nicht.
Warum ein längst bewiesener Satz noch einmal geprüft wird
Andrew Wiles bewies den Satz 1995, rund 358 Jahre nach Fermats Randnotiz. Für Menschen geschriebene Beweise überspringen jedoch Schritte, die Fachleute als offensichtlich ansehen. Lean akzeptiert das nicht: Jeder Schluss muss ausformuliert sein, bevor die Maschine ihn abnimmt. Genau diese Lücken zu füllen war die Aufgabe der Agenten.
Wie die Agenten gearbeitet haben
Als Grundlage diente nicht Wiles' 129-seitiges Original, sondern die vereinfachte Darstellung von Darmon, Diamond und Taylor. Die Agenten liefen auf der Plattform Prove2Me, die von Forschenden der Columbia University stammt, und griffen auf die Gemeinschaftsbibliothek Mathlib zu. Koordiniert wurde die Arbeit von Tianyi Peng, der laut Anthropic nur gelegentlich grobe Vorgaben machte. Nach 11 Tagen lag der Code vor.
Was geprüft ist – und was offen bleibt
Der Code kompiliert in Lean und kommt mit den drei Standardaxiomen des Systems aus. Kevin Buzzard vom Imperial College London hat ihn selbst übersetzt und mit einem Comparator gegen die Formulierung in Mathlib abgeglichen. Buzzard spricht von einem „großen Schritt“ hin zur automatischen Formalisierung mathematischer Literatur, betont aber, dass inhaltlich nichts Neues entstanden sei. Eine breitere Bewertung durch die Fachgemeinde steht weitgehend aus.
Was der Durchlauf gekostet hat
Anthropic beziffert den Verbrauch auf rund 6 Milliarden Output-Token und schätzt die Rechenkosten auf 100.000 bis 300.000 US-Dollar. Eine exakte Summe nennt das Unternehmen nicht. Auch welche Claude-Version die Agenten antrieb, geht aus der Berichterstattung nicht hervor. Der Beweis selbst liegt öffentlich in einem GitHub-Repository von Anthropic.
Der Vergleich mit Buzzards eigenem Projekt
Buzzard leitet seit 2024 ein eigenes Vorhaben zur Formalisierung von Fermats letztem Satz, finanziert bis 2029. Dessen Blueprint umfasst 86 Seiten und zielt auf den modernen, deutlich umfangreicheren Beweisweg. Anthropics Lauf deckt den älteren, engeren Pfad ab. Er ersetzt das Projekt also nicht, zeigt aber, wie schnell Formalisierungsarbeit inzwischen laufen kann.
Bestätigt ist bislang vor allem die technische Seite: Der Code lässt sich übersetzen und prüfen. Ob die Fachgemeinde die Formalisierung als vollwertig anerkennt, ist noch nicht entschieden. Diese Meldung stützt sich auf eine einzige unabhängige Redaktion.
Häufige Fragen
Hat eine KI Fermats letzten Satz bewiesen?
Nein. Der Beweis stammt von Andrew Wiles aus dem Jahr 1995. Die Claude-Agenten haben ihn nur so umgeschrieben, dass ein Rechner jeden Schritt nachprüfen kann.
Was ist Lean?
Lean ist ein Beweisassistent: eine Programmiersprache samt Prüfsystem, in der mathematische Aussagen so formuliert werden, dass eine Maschine sie lückenlos kontrollieren kann.
Was hat die Formalisierung gekostet?
Anthropic schätzt die Rechenkosten auf 100.000 bis 300.000 US-Dollar bei rund 6 Milliarden Output-Token. Eine genaue Summe nennt das Unternehmen nicht.
