Dal 6 al 10 luglio, a Londra, un workshop di Imperial College ha messo alla prova una delle frontiere piu' affascinanti dell'incontro tra intelligenza artificiale e matematica: usare l'IA per autoformalizzare pezzi della dimostrazione dell'Ultimo teorema di Fermat, cioe' tradurli automaticamente in un linguaggio che un computer possa verificare passo dopo passo.
Cos'e' l'autoformalizzazione
Formalizzare una dimostrazione significa riscriverla in un assistente di dimostrazione come Lean, un software in cui ogni singolo passaggio logico viene controllato dalla macchina: se il ragionamento fila, Lean lo accetta; se c'e' un buco, lo segnala. E' un lavoro lento e meticoloso, storicamente svolto a mano da matematici. L'autoformalizzazione punta a delegare parte di questa fatica a un modello di IA, che legge la matematica scritta in linguaggio naturale e produce il corrispondente codice formale.
Il progetto FLT e il ruolo di Kevin Buzzard
Il workshop si inserisce in un'impresa piu' ampia: il progetto FLT (Fermat's Last Theorem), uno sforzo open source guidato dal matematico Kevin Buzzard e finanziato dall'ente britannico EPSRC fino al 2029, che punta a formalizzare in Lean una variante moderna della celebre dimostrazione di Andrew Wiles e Richard Taylor. Il codice del progetto e' pubblico su GitHub e cresce riga dopo riga, con il contributo di una comunita' internazionale di volontari e ricercatori.
L'Ultimo teorema di Fermat - l'affermazione, rimasta senza dimostrazione per oltre tre secoli, che non esistono interi positivi che soddisfino l'equazione x^n + y^n = z^n per n maggiore di 2 - e' un banco di prova ideale proprio per la sua difficolta': la dimostrazione moderna si appoggia a un'enorme mole di matematica avanzata.
Perche' l'approccio e' insolito
La societa' Logos Research, che ha finanziato il workshop, ha proposto un esperimento controcorrente: invece di scegliere aree della matematica in cui l'autoformalizzazione funziona gia' bene, si e' scelto prima l'obiettivo - Fermat - e solo dopo ci si e' chiesti se l'IA fosse all'altezza. L'aspettativa dichiarata dagli organizzatori e' realistica: le parti della dimostrazione ricche di definizioni complesse daranno probabilmente risultati scadenti, mentre i tratti in cui le definizioni sono gia' presenti nella libreria matematica di Lean (mathlib) e le dimostrazioni sono ben documentate nella letteratura potrebbero andare sorprendentemente bene.
Cosa significa per il futuro delle dimostrazioni
Il tema va ben oltre Fermat. Se i modelli di IA diventeranno abbastanza affidabili da tradurre in forma verificabile ampie porzioni di matematica avanzata, cambierebbe il modo stesso in cui le dimostrazioni vengono controllate: non piu' solo la revisione tra pari, ma anche la verifica meccanica riga per riga. E' un percorso ancora agli inizi, costellato di errori e di casi in cui l'IA "inventa" passaggi che sembrano corretti ma non lo sono - ragione per cui un assistente come Lean, che rifiuta ogni passo non giustificato, e' il compagno ideale: fa da rete di sicurezza contro le allucinazioni.
Il valore dell'esperimento di Imperial College sta proprio qui: non promette di "risolvere" Fermat con l'IA - la dimostrazione umana esiste gia' - ma di misurare, su un problema volutamente difficile, quanto lontano possa spingersi oggi l'autoformalizzazione. E' un test onesto, con risultati attesi anche negativi, che dice piu' di molti annunci trionfalistici su quanto l'IA sia davvero utile alla matematica di ricerca.
Le informazioni provengono dal blog Xena di Kevin Buzzard, dal repository pubblico del progetto FLT e dalla documentazione di Lean.
