Formalisieren heißt, einen Beweis so umzuschreiben, dass ein Beweisassistent wie Lean ihn Schritt für Schritt automatisch nachrechnet. Im öffentlichen Repository steht die vollständige Aussage: für alle n ab 3 und positive a, b, c gilt, dass a hoch n plus b hoch n ungleich c hoch n ist. Der Build scheitert laut Anthropic, wenn der Beweis nicht auf genau Leans drei Standard-Axiomen ruht; Module mit „axiom“ oder „sorry“ sind ausgeschlossen.
Der neu formalisierte Teil deckt den Satz nicht allein ab. Buzzard beschreibt, dass Anthropics Beitrag Frey-Kurven für Primzahlen ab 17 ausschließt; die kleineren Exponenten stammen aus dem schon vorhandenen Projekt flt-regular, und die kleinste irreguläre Primzahl ist 37. Anthropic nennt beide Vorarbeiten – das Imperial-College-Projekt und flt-regular – als übernommene Bausteine.
Buzzard hat den Code selbst kompiliert und mit dem Vergleichswerkzeug comparator gegen die Fermat-Formulierung der Mathematikbibliothek Mathlib geprüft; er bestätigt das Ergebnis. Er zählt über 13,4 Millionen Zeilen, die auf einer Maschine mit 96 Kernen fast zwanzigmal so lange kompilieren wie Mathlib selbst. Mathematisch sage die Arbeit „essentially nothing“, sie folge der frühen Literatur zum Beweis und füge nichts hinzu.
Anthropic beschreibt Dutzende zusammenarbeitender Claude-Agenten auf Basis von Claude Code. Frühe Anläufe scheiterten, weil die Agenten den Projektstand aus den Augen verloren; ihre verworfenen Ergebnisse steuerten rund 7 Prozent der Zeilen bei. Das eingesetzte Modell bezeichnet das Unternehmen als internes Forschungsmodell, ungefähr vergleichbar mit Claude Fable 5.1. Was der Lauf gekostet hat, nennt es nicht.