In questo articolo Indice dei contenuti 2 sezioni
Undici giorni contro dieci anni di lavoro previsti: è questo il divario che ha reso notevole l’impresa legata al teorema di Fermat, tradotto in codice informatico da un modello sperimentale di Claude, l’intelligenza artificiale sviluppata da Anthropic. La notizia è arrivata dal blog ufficiale dell’azienda, che ha raccontato come il sistema abbia prodotto circa 13 milioni di righe scritte in Lean, il linguaggio pensato apposta per mettere nero su bianco i ragionamenti matematici in una forma che un computer possa verificare riga per riga.
Il confronto con i tempi umani è la parte che colpisce di più. Lo stesso obiettivo era al centro di un progetto guidato dal matematico Kevin Buzzard, con una tabella di marcia stimata intorno ai dieci anni. Undici giorni di elaborazione contro un decennio di lavoro accademico: numeri che raccontano da soli il tipo di salto che si sta consumando nel rapporto tra matematica e automazione.
Cosa dice davvero il teorema di Fermat
Conosciuto anche come Ultimo Teorema di Fermat, il problema venne formulato nel 1637 ed è diventato negli anni una specie di leggenda tra gli appassionati di numeri. La sua formulazione parte da un terreno familiare, molto vicino a quello del Teorema di Pitagora, e proprio questa apparente semplicità ha alimentato per secoli il fascino attorno alla sua dimostrazione. Semplice da enunciare, durissimo da dimostrare.
La svolta arrivò negli anni Novanta con Andrew Wiles, affiancato poi dal contributo di Richard Taylor. Una costruzione complessa, stratificata, che ora per la prima volta è stata trasformata in codice controllabile da una macchina. Non si tratta quindi di una nuova dimostrazione, ma della sua traduzione formale, un passaggio che la comunità matematica considera tutt’altro che banale, perché costringe a esplicitare ogni singolo passaggio logico che un essere umano darebbe per scontato.
Nel percorso che ha portato al risultato, Claude ha elaborato e prodotto qualcosa come 30.300 teoremi intermedi. Un numero che dà la misura di quanto sia articolata la struttura sottostante, fatta di passaggi minori che sorreggono l’impalcatura complessiva.
I limiti tecnici e i tentativi andati a vuoto
Il lavoro, però, non è completo nel senso pieno del termine. Il materiale generato dall’intelligenza artificiale porta con sé una limitazione tecnica precisa: al momento il codice prodotto non può essere integrato all’interno della libreria standard MathLib, quella che la comunità accademica usa abitualmente per questo tipo di formalizzazioni. Tradotto in pratica, il risultato esiste e funziona, ma resta in una sorta di zona separata rispetto al patrimonio condiviso su cui lavorano i matematici di mezzo mondo.
C’è poi il capitolo dei fallimenti, che l’azienda non ha nascosto. Prima di arrivare al traguardo ci sono stati vari tentativi andati a vuoto, dovuti al fatto che gli agenti impegnati nel progetto smettevano di collaborare tra loro dopo le fasi iniziali. Un problema di coordinamento più che di calcolo, che racconta quanto sia ancora delicato far lavorare insieme più sistemi automatici su un compito lungo e stratificato.
La formalizzazione della dimostrazione di Wiles resta comunque uno dei banchi di prova più duri immaginabili per un sistema di intelligenza artificiale applicato alla matematica. E il fatto che undici giorni abbiano sostituito una previsione decennale segna un punto di riferimento concreto, con tutti i suoi asterischi, per chi lavora sulla verifica automatica delle dimostrazioni in Lean.
Fonte: TecnoAndroid
