Anthropic hat unter der Apache-2.0-Lizenz einen vollständigen, maschinell geprüften Beweis des großen Fermatschen Satzes in Lean 4 veröffentlicht, aufgebaut auf der Mathematikbibliothek Mathlib. Die im Repository angegebene formale Aussage lautet: Für alle n ≥ 3 und positive ganze Zahlen a, b, c gilt a^n + b^n ≠ c^n. Dieser Satz wurde in Lean als Theorem geschrieben, das der Kernel Schritt für Schritt nachprüfen kann, ohne eine einzige Lücke.
Der Umfang ist der auffälligste Teil dieser Arbeit. Das Repository zählt 60.475 Module, 29.511 Sätze, 1.450 Definitionsmodule; die Exportprüfung deckte 1.052.234 Deklarationen ab. Die erzeugte HTML-Dokumentation ist rund 390 MB groß, der vollständige Export 37,8 GB. Wer das lokal nachvollziehen will, braucht über 300 GB Festplattenspeicher und im Spitzenwert rund 153 GB Arbeitsspeicher.
Drei Prüfläufe, alle dokumentiert
Das Repository begnügt sich nicht mit einem bloßen "kompiliert erfolgreich". Der erste Durchlauf ist die vollständige Kompilierung durch den Kernel von Lean 4.33.1 selbst, auf einer 96-Kern-Maschine in 5 Stunden 32 Minuten. Der zweite Durchlauf nutzt das offizielle Comparator-Werkzeug von leanprover (v4.33.0) zur erneuten Prüfung und dauerte rund 14 Stunden 46 Minuten. Der dritte Durchlauf wechselt zum unabhängigen, in Rust geschriebenen Kernel nanoda 0.4.13, der mit 16 Threads etwa 30 Minuten brauchte und die Ausgabe "Your solution is okay!" lieferte.
Neben den drei Prüfläufen gilt eine harte Nebenbedingung: In keinem der Module dürfen `axiom`, `sorry`, `native_decide`, `unsafe`, `extern`, `implemented_by`, `partial def` oder `#eval` vorkommen. Diese Schlüsselwörter gelten in der Lean-Community als anerkannte Einfallstore für Lücken — `sorry` steht unmittelbar für "hier fehlt noch der Beweis", `native_decide` überträgt einen Teil der Entscheidung an vom Kernel nicht geprüften Maschinencode. Sie vollständig auszuschließen heißt anzuerkennen, dass die Glaubwürdigkeit des Beweises allein auf dem Lean-Kernel und den Prüfwerkzeugen ruht — das steht so auch im README.
Wie viel die KI geschrieben hat, sagt das Repository nicht
Laut README wurde der Lean-Quellcode "von KI-Agenten auf Basis von Menschen geschriebenem Open-Source-Lean-Code erzeugt, wobei Lean als Schiedsrichter fungiert". Ein konkretes Verhältnis wird nicht offengelegt: Welche Module von Menschen stammen und welche vom Modell generiert und dann vom Kernel zurückgewiesen und neu erzeugt wurden, lässt sich aus dem öffentlichen Material nicht ablesen.
Die menschliche Grundlage ist dagegen recht klar ausgewiesen. 106 Abhängigkeitsdateien stammen aus bereits bestehenden akademischen Projekten, vor allem aus dem von Kevin Buzzard am Imperial College geleiteten FLT-Formalisierungsprojekt und aus flt-regular, das den Satz von Kummer behandelt; weitere 23 Module beweisen Inhalte aus Mathlib erneut.
Im Kontext der formalen Mathematik fällt der Sprung in der Größenordnung deutlich auf. Der Vierfarbensatz wurde 2005 von Georges Gonthier in Coq formalisiert, das Flyspeck-Projekt zur Kepler-Vermutung wurde 2014 für abgeschlossen erklärt — beide wurden in Personenjahren gemessen. Auch Buzzards FLT-Projekt ging bei seinem Start von einer ähnlichen, mehrjährigen Zeitspanne aus. Wie stark dieses Repository die Ziellinie vorgezogen hat, hängt vom tatsächlichen Verhältnis zwischen menschlicher und maschineller Arbeit ab — und genau das ist derzeit die einzige Zahl, die sich nicht nachschlagen lässt.
Quellen: öffentliches README und Verifikationsprotokoll von Anthropic, CocoLoop, Mathlib-Projekt, öffentliche Materialien des FLT-Projekts am Imperial College; Modulanzahl, Anzahl der Sätze und die Laufzeiten der drei Prüfungen wurden anhand der Angaben im Repository abgeglichen.