Anthropic ha annunciato il 4 settembre un risultato che merita molta più attenzione di quanto suggerisca il titolo spettacolare con cui è stato raccontato: Claude ha prodotto in undici giorni la prima formalizzazione completa e verificabile da computer del Teorema di Fermat, traducendo in Lean la dimostrazione matematica e arrivando a circa 13 milioni di righe di codice, con 29.500 teoremi intermedi utilizzati nella prova finale. Non ha quindi “scoperto” il Teorema di Fermat e non ha risolto un problema matematico rimasto aperto per 358 anni. Il problema era già stato risolto da Andrew Wiles nel 1995. La novità è diversa, e probabilmente più importante per il futuro dell’intelligenza artificiale: Claude ha trasformato una dimostrazione matematica estremamente complessa in un oggetto che un sistema formale può controllare passo dopo passo.

Il Teorema di Fermat afferma che non esistono interi positivi a, b e c tali che aⁿ + bⁿ = cⁿ per n maggiore di 2. Pierre de Fermat annotò l’enunciato nel XVII secolo, sostenendo di possedere una dimostrazione troppo lunga per essere contenuta nel margine del libro. La storia ha poi assunto una forma quasi crudele: quella dimostrazione non è mai comparsa e, dopo secoli di tentativi, Wiles riuscì a dimostrare il teorema utilizzando strumenti matematici che Fermat non avrebbe potuto conoscere. La prova di Wiles, pubblicata nel 1995, occupava 129 pagine e aveva richiesto una revisione sostanziale dopo che era stato individuato un problema nella prima versione.

La distinzione fondamentale riguarda la differenza tra dimostrare e verificare. Una dimostrazione matematica destinata agli esseri umani contiene inevitabilmente passaggi lasciati impliciti, risultati precedenti, convenzioni condivise e salti logici che un matematico esperto può ricostruire. Un proof assistant come Lean non concede questo privilegio. Ogni passaggio deve essere espresso in una forma sufficientemente precisa perché il kernel del sistema possa verificarlo. È una differenza apparentemente tecnica, ma con conseguenze industriali enormi: la matematica diventa, almeno in parte, un software eseguibile e verificabile. Non basta più dire che la dimostrazione è corretta. Bisogna consegnare un artefatto che una macchina possa ricompilare e controllare.

Il progetto di formalizzazione del Teorema di Fermat esisteva già prima dell’intervento di Anthropic. Kevin Buzzard dell’Imperial College London aveva avviato nel 2024 un’iniziativa per tradurre la dimostrazione di Wiles in Lean, con un lavoro previsto su più anni. La difficoltà non consisteva semplicemente nel copiare 129 pagine dentro un linguaggio formale. La prova di Wiles si appoggia a una vasta infrastruttura matematica, dalla teoria dei numeri alla geometria, dall’analisi armonica alla teoria delle rappresentazioni. Formalizzare significa ricostruire quella rete in una forma che il computer possa verificare, spesso partendo da una quantità molto più limitata di matematica già codificata.

Claude ha affrontato il problema con un’architettura multi-agente. Decine di agenti hanno lavorato contemporaneamente su definizioni, lemmi e teoremi intermedi, costruendo progressivamente una struttura che seguiva in larga misura la strategia matematica di Frey, Serre, Ribet, Wiles e Taylor-Wiles. Il problema iniziale era molto poco glamour: gli agenti perdevano memoria del lavoro già svolto, duplicavano attività e prendevano strade che conducevano a vicoli ciechi. Circa il 7% delle righe non boilerplate della versione finale deriva proprio da questi tentativi falliti. La soluzione è arrivata attraverso Prove2Me, uno strumento sviluppato dal gruppo di Tianyi Peng alla Columbia University, che ha fornito agli agenti una struttura condivisa delle dipendenze e dei teoremi ancora da dimostrare.

Il risultato è impressionante anche per una ragione quasi paradossale. La prova finale contiene circa 13 milioni di righe di Lean, oltre cinque volte la dimensione della Mathlib, la principale libreria matematica open source su cui il progetto si appoggia. Anthropic afferma che il sistema ha prodotto circa 30.300 teoremi verificabili durante il lavoro, dei quali 29.500 sono confluiti nella dimostrazione finale, consumando circa sei miliardi di token generati da un modello interno di ricerca comparabile, secondo l’azienda, a Claude Fable 5.1.

La cosa interessante, tuttavia, è ciò che il numero di 13 milioni di righe nasconde. La lunghezza non misura la profondità matematica. Un codice formale può essere enormemente più verboso della matematica che rappresenta, perché deve esplicitare ogni dettaglio che un matematico umano normalmente comprime in una frase. Dire che Claude ha prodotto la “più lunga dimostrazione matematica mai realizzata” è quindi giornalisticamente efficace ma concettualmente fuorviante. Più precisamente, ha prodotto una delle più grandi formalizzazioni matematiche generate con un processo largamente automatizzato. Il valore sta nella verificabilità, nella velocità e nella capacità di orchestrare migliaia di passaggi, non nella quantità di testo.

La verifica indipendente è il punto che rende l’annuncio particolarmente interessante. Il repository pubblico di Anthropic dichiara che la prova è stata costruita con Lean 4.33.1 e Mathlib 4.33.0. Il progetto non utilizza sorry, non introduce assiomi aggiuntivi e il controllo finale mostra che il teorema dipende dai tre assiomi standard di Lean, propext, Classical.choice e Quot.sound. Anthropic riporta inoltre che un secondo kernel indipendente, Nanoda, ha accettato l’ambiente esportato, controllando oltre un milione di dichiarazioni senza errori.

Questo dettaglio modifica radicalmente la natura della notizia. Se Claude avesse semplicemente prodotto una spiegazione convincente della dimostrazione di Wiles, sarebbe stato un altro esempio di un modello linguistico capace di imitare il linguaggio della matematica. Il problema sarebbe rimasto quello che conosciamo bene nel mondo dei chatbot: una risposta può essere elegante, autorevole e completamente sbagliata. Qui invece il modello deve produrre un artefatto che supera un controllo formale. Il compilatore diventa il revisore più spietato della stanza, e soprattutto non si lascia impressionare dalla sicurezza con cui il modello racconta la propria soluzione.

È una distinzione che dovrebbe interessare anche il management tecnologico. L’AI generativa ha passato anni a convincere le imprese che la capacità di produrre testo, codice o immagini equivaleva a capacità cognitiva. Il passaggio più significativo potrebbe essere invece l’opposto: costruire sistemi nei quali l’output dell’AI venga sottoposto automaticamente a un ambiente formale capace di respingerlo. Nel software questo principio esiste da decenni attraverso compilatori, test e sistemi di verifica. La formalizzazione matematica porta la stessa filosofia dentro un dominio nel quale l’autorità dell’esperto umano è stata tradizionalmente fondamentale.

La parte più interessante, quindi, non riguarda Fermat. Riguarda il possibile emergere di una nuova pipeline scientifica nella quale gli esseri umani definiscono problemi, architetture concettuali e criteri di validazione, mentre agenti AI producono, scompongono, verificano e ricompongono enormi quantità di lavoro formale. In questo scenario l’AI non sostituisce necessariamente il matematico. Cambia il rapporto tra intuizione e verifica. Il ricercatore potrebbe concentrarsi sempre più sulla scoperta delle idee e sempre meno sulla trasformazione manuale di quelle idee in migliaia di passaggi verificabili.

C’è anche un risvolto economico. La formalizzazione matematica è tradizionalmente costosa perché richiede competenze estremamente rare e migliaia di ore di lavoro. Se un sistema multi-agente può comprimere un progetto previsto su più anni in undici giorni, il valore marginale dell’automazione diventa enorme. Ma il conto non è semplicemente “AI contro matematici”. Claude ha avuto a disposizione Mathlib, risultati matematici formalizzati da comunità umane, codice open source e un progetto costruito da ricercatori. Il capitale umano non è scomparso dalla catena del valore; è stato incorporato nell’infrastruttura sulla quale gli agenti hanno potuto correre.

Per questo la notizia va letta con maggiore precisione rispetto alla formula “l’AI ha risolto Fermat”. Fermat era già stato risolto. Claude ha fatto qualcosa di diverso: ha dimostrato che un sistema AI può prendere una delle dimostrazioni più sofisticate della matematica moderna, decomporla in migliaia di obiettivi, coordinarne automaticamente la soluzione e produrre un artefatto formalmente verificabile. È un risultato meno cinematografico della scoperta di un nuovo teorema, ma forse più significativo per l’evoluzione dell’AI scientifica.

Il passaggio successivo potrebbe essere molto più interessante del record appena stabilito. Se gli agenti diventano capaci non soltanto di formalizzare matematica esistente, ma di proporre nuove congetture, costruire dimostrazioni originali e sottoporle immediatamente a proof assistant indipendenti, la distinzione tra “modello linguistico” e “strumento di ricerca” comincia a perdere significato. A quel punto non avremo semplicemente macchine che scrivono matematica. Avremo sistemi che producono oggetti matematici verificabili, falliscono pubblicamente quando sbagliano e possono riprovare senza chiedere ferie al proprio responsabile. È una forma di automazione scientifica decisamente più concreta dell’ennesima demo in cui un chatbot scrive una poesia su Fermat.