Secondo Anthropic, il teorema di Fermat formalizzato in Lean

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.

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 è 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.

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.

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.