Lo scorso luglio fu il premio Nobel per la Fisica ad annunciare che aveva aiutato l’Intelligenza artificiale Claude a risolvere un enigma della fisica. Adesso Anthropic ha annunciato che un modello sperimentale di Claude ha completato in undici giorni la formalizzazione in linguaggio Lean della dimostrazione del Teorema di Fermat. Il risultato, annunciato dall’azienda, consiste nella traduzione di una complessa dimostrazione matematica in codice verificabile da un computer.
Claude ha generato circa 13 milioni di righe di codice e 30.300 teoremi intermedi. Un risultato che assume particolare rilievo se confrontato con il progetto umano guidato dal matematico Kevin Buzzard, per il quale la formalizzazione completa del teorema era stata stimata in circa dieci anni.
L’Ultimo Teorema di Fermat fu formulato nel 1637 da Pierre de Fermat e afferma che, per ogni intero n maggiore di 2, l’equazione xⁿ + yⁿ = zⁿ non ha soluzioni intere positive non nulle. Il problema rimase irrisolto per oltre tre secoli, fino alla dimostrazione di Andrew Wiles negli anni Novanta, completata con il contributo di Richard Taylor.
Il lavoro di Claude non consiste dunque nell’aver scoperto una nuova prova del teorema, già dimostrato da Wiles, ma nell’aver trasformato una dimostrazione matematica in una sequenza formale di passaggi che un sistema informatico può controllare. È proprio questa la funzione di Lean, un linguaggio e ambiente dedicato alla formalizzazione della matematica.
