Le due versioni sono allineate blocco per blocco, nell’ordine del testo: titolo, l’essenziale, poi paragrafo per paragrafo. Quando la traduzione ha fuso o diviso un paragrafo, la casella corrispondente resta vuota — non accostiamo mai due passaggi a occhio.
Der entscheidende Moment dieses Fermat-Projekts ist unspektakulär: In Lean kompiliert ein Beweis – oder er tut es nicht. Im GitHub-Repository von Anthropic liegt nach Angaben des Unternehmens nun eine vollständig computergeprüfte Fassung von Fermats letztem Satz. Der Mathematiker Kevin Buzzard hat den Code inzwischen selbst kompiliert und den zugehörigen Komparator ausgeführt.
Il momento decisivo di questo progetto su Fermat è tutt'altro che spettacolare: in Lean una dimostrazione viene compilata, oppure no. Nel repository GitHub di Anthropic si trova ora, secondo l'azienda, una versione interamente verificata dal computer dell'ultimo teorema di Fermat. Il matematico Kevin Buzzard ha nel frattempo compilato personalmente il codice ed eseguito il comparatore associato.
Mathematisch ist der Satz nicht neu. Andrew Wiles bewies 1995 auf 129 Seiten, dass die Gleichung xⁿ + yⁿ = zⁿ für ganzzahlige Exponenten n > 2 keine ganzzahligen Lösungen hat. Neu ist die Formalisierung: Der Beweis wird so in Code übersetzt, dass ein Computer jeden einzelnen Schritt kontrollieren kann, statt sich auf übersprungene, für Menschen offensichtliche Zwischenschritte zu verlassen.
Dal punto di vista matematico, il teorema non è nuovo. Nel 1995, Andrew Wiles ha dimostrato in 129 pagine che l'equazione xⁿ + yⁿ = zⁿ non ha soluzioni intere per esponenti interi n > 2. La novità è la formalizzazione: la dimostrazione viene tradotta in codice in modo che un computer possa controllare ogni singolo passaggio, invece di affidarsi a passaggi intermedi omessi perché ovvi per gli esseri umani.
Lean ist dabei Programmiersprache und Prüfsystem zugleich. Mathematische Aussagen und ihre Herleitungen werden gegen ein festes logisches Regelwerk geprüft; wenn auch nur eine Lücke bleibt, kompiliert der Beweis nicht. Vertrauen muss dann vor allem dem kleinen Kern von Lean und seinen Axiomen gelten. Die verfügbare Bibliothek Mathlib begrenzt den Spielraum allerdings auf den Teil der Mathematik, der bereits formalisiert wurde.
Lean è al tempo stesso linguaggio di programmazione e sistema di verifica. Gli enunciati matematici e le relative deduzioni vengono verificati sulla base di un insieme fisso di regole logiche; se rimane anche una sola lacuna, la dimostrazione non viene compilata. La fiducia deve quindi essere riposta soprattutto nel piccolo nucleo di Lean e nei suoi assiomi. La libreria disponibile, Mathlib, limita tuttavia il campo alla parte della matematica già formalizzata.
Anthropic zufolge arbeiteten Dutzende Claude-Agenten elf Tage lang an einer vereinfachten Fassung von Wiles’ Beweis nach Darmon, Diamond und Taylor. Heraus kamen 13 Millionen Zeilen Lean-Code und rund 29.500 Zwischentheoreme. Erste Teams scheiterten laut dem Unternehmen am Projektüberblick; vorangekommen sei die Arbeit erst mit Prove2Me, einer von Tianyi Pengs Gruppe an der Columbia University entwickelten Plattform, die nächste Beweisschritte in einem gerichteten azyklischen Graphen verwaltet. Der Aufwand lag laut Anthropic bei rund sechs Milliarden Output-Token; daraus lassen sich Kosten zwischen 100.000 und 300.000 US-Dollar hochrechnen.
Secondo Anthropic, decine di agenti Claude hanno lavorato per undici giorni a una versione semplificata della dimostrazione di Wiles, basata sui lavori di Darmon, Diamond e Taylor. Il risultato è stato di 13 milioni di righe di codice Lean e circa 29.500 teoremi intermedi. Secondo l'azienda, i primi gruppi non sono riusciti a mantenere una visione d'insieme del progetto; il lavoro ha fatto progressi solo con Prove2Me, una piattaforma sviluppata dal gruppo di Tianyi Peng alla Columbia University, che gestisce i passaggi successivi della dimostrazione in un grafo aciclico diretto. Secondo Anthropic, il lavoro ha richiesto circa sei miliardi di token di output; da questa cifra si possono ricavare costi compresi tra 100.000 e 300.000 dollari USA.
Konkret ändert sich damit schon jetzt etwas für die Formalisierung mathematischer Literatur: Dritte können den offengelegten Code kompilieren und die logische Kette prüfen. Das schafft eine technisch reproduzierbare Kontrolle, ersetzt aber keine unabhängige Bewertung, die bislang weitgehend aussteht. Buzzard hält die Formalisierung für einen großen Schritt hin zur automatischen Formalisierung moderner Mathematik; zugleich folgt sie der frühen Literatur und liefert keine neue mathematische Aussage über Fermats letzten Satz.
Per la formalizzazione della letteratura matematica, qualcosa cambia già da ora: terzi possono compilare il codice reso pubblico e verificare la catena logica. Questo crea un controllo tecnicamente riproducibile, ma non sostituisce una valutazione indipendente, che finora manca in gran parte. Buzzard considera la formalizzazione un grande passo verso la formalizzazione automatica della matematica moderna; al tempo stesso, essa segue la letteratura precedente e non fornisce alcuna nuova affermazione matematica sull'ultimo teorema di Fermat.