In questo articolo Indice dei contenuti 2 sezioni
Il Teorema di Fermat è finito sotto la lente di un computer, e il risultato ha qualcosa di clamoroso: la dimostrazione storica firmata da Andrew Wiles è stata tradotta per la prima volta in codice verificabile da una macchina, con un prototipo avanzato di Claude che ha macinato in undici giorni un lavoro immaginato su una scala di anni. Circa 13 milioni di righe prodotte in Lean, il linguaggio che permette di scrivere ragionamenti matematici in forma rigorosamente formale. Un numero che da solo racconta la dimensione dell’impresa.
Vale la pena ricordare da dove parte tutto. L’enunciato risale al 1637 e nella sua semplicità è quasi provocatorio: non esistono numeri interi positivi capaci di soddisfare xⁿ + yⁿ = zⁿ quando n è maggiore di 2. Frase corta, conseguenze enormi. Per oltre tre secoli la matematica ci ha sbattuto la testa, fino agli anni Novanta, quando Wiles, con il contributo successivo di Richard Taylor, è arrivato alla dimostrazione attraverso una costruzione di rara complessità.
Perché serviva una verifica al millimetro
Qui sta il punto che spesso sfugge a chi guarda la faccenda da fuori. Dimostrare un teorema è un mestiere, controllare che ogni singolo passaggio regga è un altro mestiere. Quando una prova si estende su centinaia di pagine, poggia su risultati precedenti e incrocia ragionamenti che pochissimi al mondo padroneggiano, anche la revisione degli esperti più scrupolosi può lasciare spiragli a piccoli errori. Non necessariamente errori fatali, ma abbastanza per lasciare un margine di dubbio.
I sistemi di verifica computerizzata nascono proprio per chiudere quel margine. Scrivere una dimostrazione in Lean significa spezzarla in passaggi elementari, ognuno controllabile in modo meccanico, senza spazio per l’intuizione o per il “questo è ovvio” che nei testi matematici compare più spesso di quanto si pensi. Ed è esattamente per questo che il Teorema di Fermat rappresenta un banco di prova quasi perfetto: complessità altissima, notorietà assoluta, una prova già accettata dalla comunità scientifica ma mai passata al setaccio automatico.
Undici giorni e 29.500 teoremi intermedi
Il dato che colpisce di più, oltre alle dimensioni del codice, riguarda i tempi. Anthropic parla di undici giorni per completare il lavoro, con la generazione di circa 29.500 teoremi intermedi lungo il percorso. Quei teoremi intermedi non sono un dettaglio tecnico da archiviare in fretta: sono i gradini che collegano un passaggio all’altro, i mattoni che permettono al sistema di verifica di seguire la catena logica senza salti.
Undici giorni contro una stima di dieci anni di lavoro umano. Il confronto è brutale e dice molto su cosa stia diventando l’intelligenza artificiale applicata alla matematica formale, un ambito in cui la pazienza e la precisione contano più della creatività pura. Non si tratta di aver trovato una nuova dimostrazione, chiariamolo. Si tratta di aver reso quella esistente controllabile riga per riga da un computer, cosa che nessuno aveva ancora fatto.
La formalizzazione, del resto, è da anni uno dei terreni più battuti da chi lavora sull’incrocio tra matematica e calcolo automatico. Tradurre in Lean risultati storici serve a costruire una base solida su cui appoggiare lavori futuri, perché un teorema formalizzato diventa un pezzo riutilizzabile, verificato una volta per tutte. Con 13 milioni di righe e quasi trentamila risultati intermedi, il patrimonio che resta a disposizione è tutt’altro che simbolico.
