Claude di Anthropic ha completato in 11 giorni la prima formalizzazione end-to-end verificata al computer dell’Ultimo Teorema di Fermat, trasformando una delle dimostrazioni più complesse della matematica moderna in codice controllabile automaticamente dal proof assistant Lean. Il lavoro è stato svolto in larga parte autonomamente da decine di agenti Claude che hanno collaborato per definire concetti matematici, dimostrare risultati intermedi e combinarli progressivamente fino alla prova completa. Il risultato finale comprende circa 13 milioni di righe di codice Lean, oltre cinque volte la dimensione di Mathlib, la principale libreria matematica comunitaria su cui la formalizzazione stessa si basa. Nel corso del progetto Claude ha prodotto prove verificabili per circa 30.300 teoremi intermedi, 29.500 dei quali sono stati utilizzati direttamente nella dimostrazione finale, consumando complessivamente circa 6 miliardi di token di output.
L’Ultimo Teorema di Fermat afferma che non esistono interi positivi a, b e c tali che aⁿ + bⁿ = cⁿ per valori interi di n superiori a 2. Pierre de Fermat formulò la congettura intorno al 1637 annotandola sul margine di una copia dell’Arithmetica di Diofanto e sostenendo di aver trovato una dimostrazione troppo lunga per essere contenuta nello spazio disponibile. Il problema rimase aperto per oltre 350 anni, fino a quando Andrew Wiles presentò nel 1993 una prima versione della dimostrazione. Durante la revisione emerse però una lacuna importante e Wiles impiegò circa un anno, lavorando anche con Richard Taylor, per correggerla. La dimostrazione definitiva venne pubblicata nel 1995 e occupava 129 pagine, facendo ricorso a strumenti avanzati di teoria dei numeri molto lontani dalla matematica disponibile all’epoca di Fermat.
La formalizzazione realizzata da Anthropic non costituisce una nuova dimostrazione matematica dell’Ultimo Teorema di Fermat, ma una ricostruzione della dimostrazione esistente in un linguaggio che un computer può verificare passo per passo. Claude ha seguito una versione semplificata dell’approccio di Wiles esposta da Henri Darmon, Fred Diamond e Richard Taylor. In una dimostrazione destinata a matematici umani è normale omettere molti passaggi considerati evidenti o fare riferimento a risultati precedenti senza esplicitare ogni dettaglio; Lean, invece, richiede che ciascun collegamento logico venga reso formalmente verificabile. Proprio questa trasformazione è tradizionalmente molto laboriosa: prima dell’esperimento di Anthropic, la completa formalizzazione del teorema era considerata un progetto potenzialmente pluriennale, e una delle sole blueprint utilizzate dalla comunità per descriverne una fase iniziale raggiungeva già 86 pagine.
Le prime prove effettuate con gruppi di agenti non hanno funzionato correttamente. Gli agenti riuscivano inizialmente a risolvere alcuni sottoproblemi, ma con l’aumentare delle dimensioni del progetto tendevano a perdere traccia dello stato complessivo della formalizzazione e a collaborare in modo inefficiente. Parte del codice generato durante questi tentativi falliti è comunque rimasta nel risultato conclusivo, rappresentando circa il 7% delle righe non boilerplate della dimostrazione finale. Per superare questo limite è stato utilizzato Prove2Me, un sistema collaborativo per la formalizzazione matematica sviluppato dal ricercatore Anthropic Tianyi Peng insieme a ricercatori della Columbia University.
Prove2Me organizza i teoremi e le relative dipendenze all’interno di un grafo aciclico diretto, consentendo agli agenti di verificare quali risultati siano già stati ottenuti e quali passaggi debbano ancora essere dimostrati. La piattaforma separa inoltre le dichiarazioni dei teoremi dalle relative prove, permettendo di compilare più rapidamente il codice Lean e di ridurre il consumo di risorse. Per ciascun teorema mantiene anche una descrizione in linguaggio naturale che semplifica la ricerca e il riutilizzo dei risultati già disponibili. In questo modo più agenti possono lavorare contemporaneamente su parti differenti della stessa dimostrazione senza duplicare il lavoro e senza dover conservare integralmente nella propria memoria contestuale lo stato di un progetto composto da milioni di righe.
La supervisione matematica umana durante il progetto è rimasta limitata principalmente a indicazioni di alto livello sulle priorità. Tianyi Peng ha fornito occasionalmente suggerimenti su quali strutture o teoremi affrontare per primi, mentre la produzione delle definizioni, delle dimostrazioni intermedie e delle connessioni tra i risultati è stata affidata agli agenti. Il sistema multi-agent era costruito su Claude Code e utilizzava un modello interno di ricerca general purpose indicato come approssimativamente comparabile a Claude Fable 5.1. Con questa configurazione il gruppo di agenti è riuscito a completare la formalizzazione in poco meno di due settimane.
La correttezza finale non è stata stabilita leggendo manualmente tutte le 13 milioni di righe generate. Lean ha verificato meccanicamente ciascun passaggio della dimostrazione e la prova finale utilizza soltanto i tre assiomi standard previsti dal sistema. Un comparatore separato ha inoltre verificato che il teorema dimostrato dal progetto corrispondesse effettivamente alla definizione dell’Ultimo Teorema di Fermat contenuta in Mathlib, evitando il rischio che gli agenti avessero formalmente dimostrato una proposizione simile ma non equivalente. È stata effettuata anche un’ulteriore verifica attraverso un’implementazione indipendente del kernel di Lean.
Kevin Buzzard, matematico dell’Imperial College London e responsabile di un progetto comunitario dedicato alla formalizzazione dell’Ultimo Teorema di Fermat avviato nel 2024, ha esaminato il risultato. Buzzard ha sottolineato che la dimostrazione formalizzata non introduce nuove ipotesi oltre agli assiomi matematici utilizzati da Lean e attraversa numerosi ambiti della matematica moderna, tra cui algebra, analisi armonica, geometria e teoria dei numeri. Ha inoltre evidenziato che artefatti di autoformalizzazione di questa dimensione possono ormai diventare sufficientemente robusti da essere utilizzati come base per ulteriori costruzioni formali.
Il risultato va quindi distinto dagli esperimenti nei quali i modelli AI producono matematica realmente nuova. Nel caso dell’Ultimo Teorema di Fermat, la conoscenza matematica fondamentale e la dimostrazione erano già disponibili: il contributo di Claude riguarda la capacità di convertire rapidamente una quantità estremamente ampia di ragionamento matematico umano in una struttura formalmente verificabile. Questo passaggio è rilevante perché il controllo delle dimostrazioni matematiche complesse può richiedere mesi o anni e un singolo errore in una lunga catena logica può compromettere tutti i risultati successivi. Con una prova formalizzata, invece, il proof assistant può controllare algoritmicamente ogni passaggio.
Il problema della verifica non riguarda soltanto il teorema di Fermat. Anthropic richiama diversi precedenti nei quali la comunità matematica ha impiegato anni per raggiungere un livello sufficiente di fiducia in dimostrazioni particolarmente complesse. La prova della congettura di Keplero presentata da Thomas Hales nel 1998 rimase in revisione per quattro anni e il gruppo di dodici revisori arrivò inizialmente a dichiararsi sicuro soltanto al 99%; Hales guidò successivamente il progetto Flyspeck, composto da circa venti persone, per formalizzare completamente la dimostrazione. Anche la dimostrazione della congettura di Poincaré di Grigori Perelman richiese diversi anni di verifica da parte della comunità matematica.
Anthropic ha sperimentato la stessa infrastruttura anche su scala molto più ridotta. Utilizzando soltanto tre normali account Claude Max e facendo collaborare gli agenti attraverso Prove2Me, un piccolo gruppo ha formalizzato applicazioni del metodo del cerchio di Hardy-Littlewood e completato in tre giorni la formalizzazione del Teorema dei tre primi di Vinogradov. Questo secondo test è stato utilizzato per verificare se l’approccio multi-agent potesse funzionare anche senza l’infrastruttura di ricerca interna utilizzata per Fermat, mostrando che alcuni progetti di formalizzazione avanzata possono essere affrontati anche con accesso a prodotti AI disponibili agli utenti.
Il progetto sull’Ultimo Teorema di Fermat mostra quindi una modalità di utilizzo dei sistemi multi-agent nella quale il problema principale non consiste soltanto nell’aumentare le capacità del singolo modello, ma nel coordinare decine di istanze che lavorano per giorni sullo stesso obiettivo mantenendo coerenti dipendenze, risultati intermedi e priorità. In questo caso l’elemento decisivo è stato affiancare Claude a un’infrastruttura capace di rappresentare esplicitamente lo stato del progetto e di assegnare ai diversi agenti sottoproblemi verificabili. Il risultato finale è una dimostrazione già conosciuta dalla matematica, ma trasformata in 13 milioni di righe di Lean controllabili automaticamente, ottenute in 11 giorni anziché attraverso un lavoro di formalizzazione stimato in anni.
Questo articolo è stato redatto con il supporto di strumenti di intelligenza artificiale (AI)