Il mondo FQ

Claude formalizza in undici giorni la dimostrazione del Teorema di Fermat, il progetto umano prevedeva 10 anni

Il modello di Anthropic ha prodotto circa 13 milioni di righe di codice Lean e 30.300 teoremi intermedi. Non è una nuova dimostrazione, ma la formalizzazione informatica di una prova già nota.
Claude formalizza in undici giorni la dimostrazione del Teorema di Fermat, il progetto umano prevedeva 10 anni
Icona dei commenti Commenti

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.

Il risultato presenta però ancora un limite: il codice prodotto dall’IA non può essere integrato, allo stato, nella libreria standard Mathlib, utilizzata dalla comunità scientifica. La formalizzazione, quindi, è stata completata ma non è ancora pronta per entrare stabilmente nell’ecosistema condiviso della matematica formale. L’esperimento mostra così una delle direzioni più promettenti dell’IA applicata alla matematica: non soltanto generare risposte, ma costruire dimostrazioni formalmente verificabili. La sfida, ora, sarà rendere questi risultati non solo ottenibili rapidamente, ma anche leggibili, riutilizzabili e integrabili nel lavoro dei matematici.

Gentile lettore, la pubblicazione dei commenti è sospesa dalle 20 alle 9, i commenti per ogni articolo saranno chiusi dopo 72 ore, il massimo di caratteri consentito per ogni messaggio è di 1.500 e ogni utente può postare al massimo 150 commenti alla settimana. Abbiamo deciso di impostare questi limiti per migliorare la qualità del dibattito. È necessario attenersi Termini e Condizioni di utilizzo del sito (in particolare punti 3 e 5): evitare gli insulti, le accuse senza fondamento e mantenersi in tema con la discussione. I commenti saranno pubblicati dopo essere stati letti e approvati, ad eccezione di quelli pubblicati dagli utenti in white list (vedere il punto 3 della nostra policy). Infine non è consentito accedere al servizio tramite account multipli. Vi preghiamo di segnalare eventuali problemi tecnici al nostro supporto tecnico La Redazione