Claude formalizza il Teorema di Fermat

Lo speciale martedì di questa settimana analizza un caso che unisce due mondi solitamente distanti: la matematica pura e l'ingegneria della verifica AI. Il rapporto pubblicato da Anthropic il 4 settembre 2026 documenta la prima dimostrazione end-to-end, verificata da computer, dell'Ultimo Teorema di Fermat, prodotta in gran parte in autonomia da Claude nell'arco di 11 giorni.

Il caso della settimana: metodologia e origine del test

Il progetto è stato guidato da Tianyi Peng, ricercatore Anthropic il cui gruppo alla Columbia University costruisce strumenti per la formalizzazione assistita da AI. L'obiettivo iniziale era verificare qualora un modello linguistico potesse contribuire alla codifica in Lean di una dimostrazione già esistente, quella firmata da Andrew Wiles nel 1995, estesa per 129 pagine e verificata manualmente per mesi dalla comunità matematica.

Il teorema, annotato da Pierre de Fermat intorno al 1637 a margine di una copia dell'Arithmetica di Diofanto, afferma che l'equazione a^n + b^n = c^n manca di soluzioni tra interi positivi per ogni valore di n superiore a due.

Il finding centrale: numeri esatti e verificabili

L'evidenza riportata è quantitativa e tracciabile: in 11 giorni di lavoro condotto in gran parte in autonomia, Claude ha prodotto 13 milioni di righe di codice Lean e dimostrato 29.500 teoremi intermedi, secondo quanto documentato da Anthropic^[1].

Il codice risultante costituisce la prima dimostrazione end-to-end del teorema controllata integralmente da un assistente di verifica formale.

Kevin Buzzard, animatore del progetto comunitario di formalizzazione avviato nel 2024 all'Imperial College London, ha definito il risultato un traguardo straordinario di autoformalizzazione, sottolineando che la dimostrazione poggia esclusivamente sugli assiomi della matematica.

Perché la verifica conta più della scoperta

La distinzione tra scoperta e verifica è metodologicamente rilevante per chi valuta investimenti in AI applicata alla ricerca. Diversamente dai lavori recenti sull'ipotesi di Riemann, che hanno prodotto matematica inedita, il contributo qui documentato riguarda la capacità di controllare una dimostrazione esistente, componendola in passaggi verificabili uno a uno dal sistema Lean.

Ogni teorema intermedio rappresenta un anello di una catena logica: qualora un singolo passaggio risultasse fallace, l'intera struttura successiva perderebbe validità.

Questo meccanismo di verifica automatica è quanto rende il risultato replicabile, a differenza di un benchmark che misura prestazioni in condizioni standardizzate e privo di legame diretto con l'affidabilità in produzione. La distanza tra un punteggio benchmark e una dimostrazione controllata riga per riga è dove si gioca l'intera questione della fiducia nei sistemi AI.

Error compounding lungo catene lunghe di ragionamento

Le 29.500 dimostrazioni intermedie costituiscono un campione naturale per osservare cosa accade quando gli errori si propagano lungo catene lunghe di ragionamento composto. La letteratura sull'affidabilità degli agenti multi-step documenta un pattern strutturale ricorrente: gli errori raramente si sommano in modo lineare, tendono piuttosto a moltiplicarsi.

Un agente con il 90% di accuratezza su cinque passaggi consecutivi raggiunge un'accuratezza composta del 59% sul task complessivo, un dato che riguarda direttamente sistemi che incatenano migliaia di passaggi come quello descritto qui.

Nel caso della formalizzazione di Fermat, il sistema Lean funge da meccanismo di controllo che intercetta l'errore prima che si propaghi, un'infrastruttura di verifica che manca nella maggioranza dei deployment aziendali attuali.

Cosa significa per CRO, CDO e Investment Committee

Per chi siede in un investment committee, il dato rilevante riguarda dove indirizzare il budget R&D destinato all'AI applicata a compiti complessi e a lunga catena.

Il caso Fermat mostra che l'autonomia prolungata, 11 giorni consecutivi secondo il rapporto Anthropic, diventa gestibile qualora esista un livello di verifica formale capace di controllare ogni singolo passaggio intermedio, invece di limitarsi a valutare l'output finale.

L'allocazione di capitale su agenti multi-step privi di un layer di verifica equivalente resta un'ipotesi metodologicamente debole: il risultato documentato vale per un dominio, la matematica formale, dotato di un linguaggio di verifica nativo come Lean. Estendere la conclusione ad altri domini privi di tale infrastruttura eccede quanto gli autori stessi dichiarano nel rapporto.

Infrastruttura dati per il Chief Analytics Officer

Il Chief Analytics Officer legge questo caso come indicazione infrastrutturale, ancora prima che come indicazione di prodotto.

Il repository pubblico della dimostrazione, disponibile su GitHub^[2], rende ispezionabile ogni passaggio intermedio, un requisito che raramente accompagna i risultati AI comunicati al pubblico.

Costruire capacità equivalenti in ambito aziendale richiede un sistema di tracciamento granulare dei passaggi intermedi, non unicamente dell'output finale: è la differenza tra misurare il risultato di un pilot in un ambiente controllato e misurare l'intera catena che lo produce sotto carico reale.

Quale thesis tecnologica regge per il Board

Per il board, il caso Fermat sostiene una thesis tecnologica precisa: l'autoformalizzazione può ridurre il tempo di verifica di risultati complessi, un processo che tradizionalmente richiede anni di lavoro collettivo della comunità scientifica.

Kevin Buzzard osserva che gli artefatti prodotti dall'autoformalizzazione risultano abbastanza robusti da poter essere costruiti sopra, una condizione che rende plausibile un'accelerazione della verifica scientifica su larga scala.

Resta da rivedere la thesis opposta, quella che tratta i benchmark come proxy sufficiente per la readiness produttiva: il caso qui descritto dimostra l'esatto contrario, ovvero che la verifica formale, e non il punteggio su un test standardizzato, costituisce la metrica rilevante per l'allocazione di capitale su sistemi AI a lunga catena.