Claude ha prodotto una formalizzazione completa dell’ultimo teorema di Fermat nel linguaggio Lean, consentendo a un assistente automatico di verificare l’intera catena logica. È un risultato tecnico rilevante, ma va descritto con precisione: non è una nuova dimostrazione matematica del teorema e non sostituisce il lavoro di Andrew Wiles. L’innovazione sta nell’aver trasformato una prova nota in codice controllabile da un computer, su una scala che fino a poco tempo fa avrebbe richiesto anni di lavoro specialistico.

Anthropic, la società che sviluppa Claude, ha pubblicato il progetto il 4 settembre. Secondo il resoconto tecnico dell’azienda, più agenti basati sul modello hanno lavorato in gran parte autonomamente per 11 giorni, generando circa 13 milioni di righe di Lean. Il sistema ha dimostrato 30.300 teoremi intermedi, 29.500 dei quali utilizzati nel percorso finale.

Il codice è stato reso disponibile pubblicamente e il matematico Kevin Buzzard, che guida un progetto accademico di formalizzazione dello stesso teorema, ha esaminato il risultato. La verifica indipendente più ampia da parte della comunità resta comunque un passaggio naturale per un artefatto di queste dimensioni.

Dimostrare e formalizzare non sono la stessa cosa

L’ultimo teorema di Fermat afferma che non esistono interi positivi che soddisfino l’equazione aⁿ + bⁿ = cⁿ quando n è maggiore di 2. Dopo più di tre secoli di tentativi, Wiles completò la prima prova accettata nel 1994, con una correzione sviluppata insieme a Richard Taylor; gli articoli definitivi furono pubblicati nel 1995.

Una dimostrazione scritta per matematici contiene passaggi che il lettore esperto può ricostruire. Una formalizzazione deve invece esplicitare ogni inferenza in un linguaggio regolato, collegando definizioni e lemmi fino agli assiomi di base. Il proof assistant non decide che l’argomento “sembra” corretto: controlla se ogni passaggio segue dalle regole dichiarate.

Claude non ha trovato un’alternativa sconosciuta alla prova di Wiles. Il progetto segue un’esposizione semplificata dovuta a Henri Darmon, Fred Diamond e Richard Taylor e riutilizza parti di precedenti lavori in Lean. Come riconosce la stessa Anthropic, la novità è la verifica automatica end-to-end.

Perché servono 13 milioni di righe

La dimensione del codice non è direttamente confrontabile con il numero di pagine di un articolo matematico. Una prova umana si appoggia a una vasta letteratura e omette molti passaggi considerati standard. Lean può utilizzare soltanto risultati già formalizzati nella libreria disponibile oppure richiede che vengano dimostrati all’interno del progetto.

Per arrivare al teorema finale, gli agenti hanno quindi costruito una grande infrastruttura intermedia in algebra, geometria, analisi armonica e teoria dei numeri. Anthropic stima che il risultato sia più di cinque volte più grande di Mathlib, la principale libreria comunitaria su cui si basa.

La lunghezza segnala anche inefficienza. L’azienda osserva che il codice è probabilmente molto più esteso del necessario. Un lavoro successivo potrà semplificare le dipendenze, eliminare duplicazioni e rendere le parti riutilizzabili da altri progetti.

Come hanno collaborato gli agenti

I primi tentativi non hanno funzionato bene. Gli agenti perdevano traccia dello stato complessivo e faticavano a coordinarsi; circa il 7% delle righe non standard del risultato finale proviene da tentativi inizialmente falliti.

Il cambio decisivo è stato l’uso di Prove2Me, una piattaforma collaborativa sviluppata da Tianyi Peng e colleghi alla Columbia University. Il sistema rappresenta i teoremi come un grafo di dipendenze: ogni agente può vedere quali risultati sono disponibili, scegliere un sottoproblema e pubblicare una prova che gli altri riutilizzano.

La separazione tra enunciati e dimostrazioni ha inoltre accelerato la compilazione di Lean e ridotto il costo di coordinamento. Il progetto ha consumato circa sei miliardi di token di output, un dato che mostra tanto la capacità raggiunta quanto l’intensità di calcolo richiesta.

Che cosa controlla Lean

Anthropic afferma che il risultato finale è stato verificato da Lean usando i tre assiomi standard del sistema. Un programma di confronto ha inoltre controllato che l’enunciato conclusivo corrisponda alla formulazione dell’ultimo teorema di Fermat presente in Mathlib.

Questo doppio controllo è importante. Una lunga sequenza può essere formalmente corretta ma dimostrare un enunciato diverso da quello desiderato; confrontare la formulazione finale riduce quel rischio. Restano però altri aspetti che la comunità valuterà: qualità del codice, chiarezza delle dipendenze, facilità di manutenzione e possibilità di riutilizzo.

Un proof assistant riduce drasticamente il rischio di un errore logico nascosto, ma non rende superflua la lettura umana. I matematici devono ancora capire quali idee usa la prova, se la formalizzazione rappresenta correttamente i concetti e come inserirla nel corpo della letteratura.

Perché il risultato conta per l’IA scientifica

La verifica formale potrebbe diventare un’infrastruttura centrale per la matematica assistita dall’intelligenza artificiale. Se i modelli producono un numero crescente di congetture e dimostrazioni, la revisione manuale può diventare un collo di bottiglia. Accompagnare un testo leggibile con un artefatto controllabile da Lean offre un secondo livello di fiducia.

Il risultato non dimostra però che un modello sappia sostituire il giudizio creativo di un matematico. Qui il percorso concettuale era noto e definito da decenni; l’IA ha svolto soprattutto un enorme lavoro di traduzione, completamento e coordinamento formale.

Il passo successivo sarà misurare quanto di questa infrastruttura sia generalizzabile. Una formalizzazione utile non deve soltanto arrivare alla casella “provato”: deve diventare comprensibile, stabile e integrabile nelle librerie condivise.

Fonti e metodo

ASTER ha esaminato il rapporto tecnico di Anthropic, il repository pubblico della formalizzazione, il progetto FLT coordinato da Imperial College London e la precedente formalizzazione in Lean del caso dei primi regolari. I dati su tempi, righe di codice e consumo di token provengono da Anthropic e sono attribuiti come tali; il testo distingue la verifica formale dalla scoperta di una nuova dimostrazione.