Teorema di Fermat: Claude lo formalizza in 11 giorni

Lo scorso luglio un premio Nobel per la Fisica aveva raccontato di essersi fatto aiutare dall'intelligenza artificiale Claude per risolvere un problema di fisica. Ora Anthropic annuncia che un modello sperimentale di Claude ha completato in undici giorni la formalizzazione in linguaggio Lean della dimostrazione dell'Ultimo Teorema di Fermat. Si tratta della traduzione di una dimostrazione matematica complessa in un codice che un computer può verificare passo per passo.

Per raggiungere il risultato, Claude ha generato circa 13 milioni di righe di codice e 30.300 teoremi intermedi. Il confronto con il lavoro umano dà la misura dell'impresa: il progetto guidato dal matematico Kevin Buzzard per formalizzare per intero il teorema era stato stimato in circa dieci anni.

L'Ultimo Teorema di Fermat fu formulato nel 1637 da Pierre de Fermat. Afferma che, per ogni numero intero n maggiore di 2, l'equazione xⁿ + yⁿ = zⁿ non ammette soluzioni intere positive diverse da zero. Il problema restò irrisolto per oltre tre secoli, fino alla dimostrazione di Andrew Wiles negli anni Novanta, completata con il contributo di Richard Taylor.

Cosa ha fatto davvero Claude

Il lavoro dell'intelligenza artificiale non consiste nell'aver trovato una nuova dimostrazione: quella di Wiles resta valida e non è stata rimessa in discussione. Claude ha invece trasformato la dimostrazione esistente in una sequenza formale di passaggi controllabile da un computer. È questo lo scopo di Lean, il linguaggio e ambiente usato per formalizzare la matematica.

Il risultato ha però un limite. Il codice prodotto dall'intelligenza artificiale non può ancora essere inserito in Mathlib, la libreria standard di riferimento per la comunità scientifica che si occupa di matematica formale. La formalizzazione è quindi completa, ma non ancora pronta per entrare stabilmente nell'ecosistema condiviso dai matematici.

L'esperimento indica comunque una direzione di lavoro per l'intelligenza artificiale applicata alla matematica: non limitarsi a fornire risposte, ma costruire dimostrazioni verificabili in modo formale. La prossima sfida, secondo quanto emerso dall'annuncio, sarà rendere questi risultati anche leggibili e riutilizzabili dai matematici, non solo veloci da ottenere.