AIREITERQuando leggete “Claude ha risolto l’Ultimo teorema di Fermat”, soffermatevi su una parola: formalizzato. Anthropic ha pubblicato un artefatto Lean accessibile al pubblico che, secondo l’azienda, verifica il teorema dall’inizio alla fine. Il percorso matematico, però, è quello già noto di Frey–Serre–Ribet–Wiles–Taylor-Wiles: non una nuova dimostrazione scoperta dall’AI.
Prima di tutto, distinguiamo le due affermazioni
La risposta breve è sì: Anthropic ha pubblicato un repository con una formalizzazione in Lean 4 dell’Ultimo teorema di Fermat (FLT), completa di istruzioni per la compilazione e la verifica. È invece fuorviante dire che Claude abbia risolto autonomamente il celebre problema: la svolta matematica risale ad Andrew Wiles e Richard Taylor, diversi decenni fa.
Il teorema di Fermat afferma che non esistono soluzioni negli interi positivi dell’equazione a^n + b^n = c^n quando n > 2. La dimostrazione di Wiles è stata pubblicata nel 1995; il lavoro di Anthropic trasforma quel percorso ormai consolidato in un artefatto verificabile automaticamente. Per il contesto storico, si può consultare l’annuncio del progetto FLT della Lean Community.
Una dimostrazione in Lean risponde a una domanda diversa rispetto a un articolo matematico informale. Può mostrare che una proposizione codificata in modo preciso deriva da definizioni, dipendenze e assiomi verificati all’interno di un ambiente specifico. Non dimostra che l’AI abbia inventato la matematica sottostante, né che i nomi dei teoremi corrispondano sempre alle descrizioni che li accompagnano.
Che cosa ha pubblicato davvero Anthropic
Nel suo post di ricerca del 4 settembre 2026, Anthropic afferma che Claude ha prodotto la prima formalizzazione completa, end-to-end e verificata dal computer dell’FLT in Lean, in 11 giorni. Il post parla di circa 13 milioni di righe di Lean, 30.300 enunciati di teorema dimostrati e 29.500 utilizzati nella dimostrazione finale. Vengono inoltre riportati circa 6 miliardi di token generati.
Il lavoro è stato realizzato con Prove2Me, una piattaforma che Anthropic descrive come un sistema capace di mantenere un grafo aciclico diretto degli enunciati e coordinare più agenti. Secondo Anthropic, la formalizzazione segue una versione semplificata del percorso dimostrativo consolidato associato a Frey, Serre, Ribet, Wiles e Taylor-Wiles.
Per verificare l’affermazione, il repository pubblico su GitHub è più utile dell’annuncio. Il target predefinito è FinalCheck.lean e la dichiarazione del teorema è la seguente:
theorem fermat_last_theorem (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ)
(ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
a ^ n + b ^ n ≠ c ^ nIl repository si presenta come un artefatto di ricerca non mantenuto e che non accetta contributi. Fissa Lean 4.33.1 e Mathlib v4.33.0, include PROOF-PATH.md e offre una versione HTML navigabile offline del grafo di teoremi e definizioni.
Il controllo finale del repository dovrebbe fallire se la dimostrazione dipende da un assioma aggiunto, da sorry, native_decide, unsafe o da una scorciatoia analoga. In questo modo l’artefatto può essere ispezionato direttamente, senza dover fare affidamento su uno screenshot o su un riassunto testuale.
Come ripetere la verifica
Una verifica seria parte dall’ambiente fissato dal repository, non dal copia-incolla di un singolo file .lean in un progetto diverso. La guida alla verifica della Lean Community spiega il motivo: Lean viene rilasciato ogni mese, Mathlib cambia spesso e la compatibilità all’indietro non è garantita.
Bloccare l’ambiente prima della compilazione
Il repository indica Linux o macOS come sistemi di destinazione e richiede elan, Git, Python, GNU coreutils e una connessione di rete, necessaria affinché Lake possa scaricare e compilare le dipendenze fissate. Vengono riportati circa 67 GB nella directory .lake, oltre a circa 220 GB di file C generati, che possono essere eliminati in seguito.
Il repository indica inoltre un consumo di circa 5 GB di memoria per job parallelo, con alcuni moduli che arrivano a richiedere fino a 36 GB. Con 96 job, la compilazione riportata dal progetto ha richiesto 5 ore e 32 minuti e ha raggiunto un picco di 153 GB di memoria. Sono dati dichiarati dal repository, non misurati in questo articolo: vanno quindi considerati un avvertimento utile per pianificare il lavoro, non una durata garantita.
Scegliere il livello di verifica
- Solo ispezione: leggere
FinalCheck.lean,PROOF-PATH.mdeATTRIBUTION.mdsenza compilare. - Build completa in Lean: usare la toolchain fissata dal progetto ed eseguire
lake build. - Riproduzione indipendente: dopo una compilazione e un’ esportazione completate con successo, eseguire gli script comparator e nanoda.
Partendo da un clone pulito, il repository propone questa sequenza generale:
git clone https://github.com/anthropics/fermats-last-theorem.git flt
cd flt
# Lower the number if your machine cannot supply the required memory.
LEAN_NUM_THREADS=96 lake build
# Check the result against a Mathlib-only challenge statement.
verification/comparator/run.sh
# Run after the comparator check.
verification/nanoda/run.shLe varie fasi hanno obiettivi diversi:
| Fase | Dettaglio riportato dal repository | A cosa serve |
|---|---|---|
lake build | 60.475 moduli; 5 ore e 32 minuti con 96 job nella compilazione riportata | Compila il progetto dai sorgenti e consente al kernel di Lean di verificare le dichiarazioni incluse nella build |
| Comparator | 14 ore e 46 minuti nella compilazione riportata; picco di memoria di 230 GB | Verifica che il teorema esposto e le costanti referenziate corrispondano all’enunciato previsto dal test basato solo su Mathlib |
nanoda | Circa 30 minuti con 16 thread dopo l’esportazione | Riproduce un ambiente esportato attraverso un kernel Rust scritto indipendentemente |
Il comparator non sostituisce la lettura dell’enunciato del teorema. Aiuta a ridurre il rischio che il progetto dimostri una proposizione indebolita o leggermente diversa da quella attesa. Il file PROOF-PATH.md collega i passaggi matematici nominati alle dichiarazioni Lean, mentre le pagine HTML generate permettono di esaminare le dipendenze senza avviare un’applicazione web.
Il repository segnala costi aggiuntivi per i controlli successivi: la scrittura di un’esportazione da 37,8 GB può richiedere circa 90 GB di memoria, mentre il flusso di lavoro nanoda può arrivare a richiedere circa 40 GB durante la verifica.
Che cosa dimostrano le verifiche e che cosa non possono dimostrare
| Livello di evidenza | Che cosa stabilisce | Che cosa non stabilisce |
|---|---|---|
| Build del kernel Lean | Che i termini della dimostrazione fornita siano verificabili nell’ambiente Lean fissato | Che Claude abbia scoperto la matematica, o che la spiegazione informale corrisponda a ogni nome di teorema |
FinalCheck.lean e controllo degli assiomi | Che il teorema finale del repository venga verificato rispetto alla lista di assiomi dichiarata e rifiuti diverse scorciatoie elencate | Che il teorema coincida con l’enunciato storico dell’FLT, se non si esamina l’enunciato stesso |
Output di #print axioms | Che, quando il controllo previsto va a buon fine, le dipendenze includano i tre assiomi standard di Lean — propext, Classical.choice e Quot.sound — anziché un assioma utente nascosto | Che l’intera catena di dipendenze software sia stata convalidata indipendentemente |
| Comparator | Che il risultato dimostrato e le costanti referenziate corrispondano al test basato solo su Mathlib utilizzato dal repository | Che ogni descrizione in linguaggio naturale presente nel progetto sia chiara o adeguata dal punto di vista didattico |
| Riproduzione con nanoda | Che un ambiente esportato sia stato accettato da una seconda implementazione del kernel Lean, scritta in Rust | Che l’esportazione, gli script o il sistema operativo siano immuni da qualsiasi possibile errore |
PROOF-PATH.md e attribuzioni | Un percorso che consente alle persone di esaminare la corrispondenza matematica e le fonti precedenti | Che i nomi dei teoremi generati automaticamente descrivano correttamente i relativi enunciati senza revisione umana |
La checklist “Did you prove it?” della Lean Community riassume la regola fondamentale: la compilazione convalida la proposizione codificata, non il fatto che il nome di un teorema corrisponda all’affermazione informale che si intende esprimere. In questo caso, il comparator e il ricorso a Mathlib riducono il rischio, ma non eliminano la necessità di leggere l’enunciato e il percorso della dimostrazione.
Che cosa mostra — e che cosa non mostra — l’artefatto
Il sistema ha prodotto un artefatto Lean verificato formalmente e di dimensioni insolite. Non dimostra però l’esistenza di un nuovo percorso verso l’FLT, di una nuova dimostrazione elementare o di una scoperta matematica indipendente da parte di Claude.
Anthropic afferma che la dimostrazione segue una versione semplificata del percorso di Wiles. Il repository riconosce inoltre il lavoro già esistente: il file ATTRIBUTION.md identifica 106 file che contengono materiale proveniente dal progetto FLT dell’Imperial College London o da flt-regular, oltre a Mathlib. Questa provenienza è essenziale per descrivere correttamente le basi dell’artefatto pubblicato.
Il progetto riporta 30.300 enunciati di teorema dimostrati durante l’esecuzione e circa 29.500 utilizzati nella dimostrazione finale, mentre il repository parla di 29.511 pagine di teoremi. Si tratta di dichiarazioni e dipendenze formali, non di 29.511 nuovi risultati matematici. Una dimostrazione formale esplicita passaggi impliciti, tipi, coercizioni, definizioni e dipendenze dalla libreria che una dimostrazione umana può lasciare alla comprensione di un esperto.
Il repository chiarisce che i sorgenti sono stati scritti per essere verificati, non per essere letti: i nomi sono generati automaticamente, etichette come P2M identificano fasi della pipeline e fa fede l’enunciato, non il nome. Ecco perché il percorso della dimostrazione e il comparator sono importanti quanto il teorema al centro dell’annuncio.
Non bisogna confondere i precedenti lavori in Lean con la dichiarazione del 2026. Un articolo del 2023 sull’Ultimo teorema di Fermat per i primi regolari riportava una formalizzazione completa e priva di sorry del Caso I del teorema di Kummer per i primi regolari, precisando però che il Caso II e il lemma di Kummer richiedevano ancora un lavoro sostanziale. Una revisione del 2025 descriveva la formalizzazione per i primi regolari come una dimostrazione completa di quel caso più circoscritto.
| Lavoro | Ambito | Ruolo pratico |
|---|---|---|
Ricerca su flt-regular | Risultati sui primi regolari e infrastruttura di supporto per la teoria algebrica dei numeri | Primo blocco formale e materiale di partenza |
| Progetto FLT dell’Imperial | Formalizzazione riutilizzabile e di lungo periodo della matematica moderna intorno all’FLT | Infrastruttura per librerie e collaborazione |
| Repository di Anthropic | Teorema FLT dichiarato come completo e end-to-end in Lean 4, con controlli di compilazione e riproduzione | Un grande artefatto di ricerca ottimizzato per ottenere un risultato verificato, non per la manutenzione a lungo termine |
Il progetto FLT di Imperial/Lean descrive la formalizzazione della matematica moderna dei numeri come un’iniziativa infrastrutturale più ampia, non come la semplice traduzione di un singolo teorema. La pubblicazione di Anthropic va quindi vista come un’evidenza complementare delle capacità degli agenti AI coordinati all’interno di un ecosistema formale già esistente, non come la prova che gli obiettivi del progetto precedente abbiano perso rilevanza.
Che cosa è ragionevole considerare verificato
| Se volete sapere… | La risposta corretta è… | Passo successivo |
|---|---|---|
| Se Anthropic ha pubblicato un artefatto reale | Sì: esistono un annuncio ufficiale e un repository pubblico con ambiente fissato | Leggere insieme il post di ricerca e il repository |
| Se il teorema codificato è davvero l’FLT | Il repository fornisce una dichiarazione precisa, un comparator e un percorso della dimostrazione | Esaminare FinalCheck.lean, il comparator e PROOF-PATH.md |
| Se il codice compila senza errori | Il repository documenta una compilazione da zero e ne riporta il risultato | Ricompilare con Lean 4.33.1 e Mathlib v4.33.0, se si dispone dell’hardware necessario |
| Se Claude ha inventato una nuova dimostrazione | Non ci sono prove a sostegno di questa descrizione: il percorso segue la matematica consolidata di Wiles/Taylor-Wiles | Definirlo una formalizzazione assistita dall’AI o un lavoro di proof engineering |
| Se l’artefatto è facile da mantenere | No: il repository si definisce esplicitamente non mantenuto e il codice è generato automaticamente | Considerarlo un artefatto di ricerca, non una libreria Mathlib pronta all’uso |
| Se questo dimostra un’autonomia matematica generale | No: mostra prestazioni su un obiettivo di formalizzazione altamente specifico e sostenuto da un’infrastruttura significativa | Tenere distinta la capacità di verifica formale dalla scoperta di teoremi a problema aperto |
Se vi interessa solo la notizia, l’annuncio ufficiale e il repository confermano che il progetto esiste. Se vi serve un audit, riproducete la compilazione nell’ambiente fissato e controllate l’enunciato. Se state valutando una ricerca sull’AI, considerate parte del sistema anche il coordinamento degli agenti, le librerie esistenti, le formalizzazioni precedenti e la potenza di calcolo.
FAQ
Claude ha scoperto una nuova dimostrazione dell’Ultimo teorema di Fermat?
No. L’artefatto di Anthropic formalizza un percorso dimostrativo consolidato associato a Frey, Serre, Ribet, Wiles e Taylor-Wiles. Il risultato sta nella scala e nella velocità con cui è stato prodotto un artefatto Lean verificabile automaticamente, non in una nuova soluzione matematica.
Una compilazione Lean completata con successo dimostra il teorema informale?
Dimostra che la proposizione codificata deriva dalle dipendenze verificate in quell’ambiente Lean. Occorre comunque controllare che la proposizione e le relative definizioni corrispondano al teorema informale che si intende rivendicare.
Il repository usa sorry o assiomi aggiuntivi?
Il repository afferma che il controllo finale rifiuta sorry, assiomi aggiunti, native_decide, unsafe e diverse scorciatoie correlate. La lista di assiomi prevista contiene i tre assiomi standard di Lean: propext, Classical.choice e Quot.sound. È comunque meglio ripetere il controllo, invece di basarsi soltanto sull’annuncio.
È possibile riprodurre il risultato su un normale portatile?
Si può provare a ispezionare il repository e a compilarne una parte, ma la verifica completa non è un’attività leggera alla portata di qualsiasi computer. Il repository riporta un picco di 153 GB di memoria per la compilazione, fino a 230 GB per il comparator e notevoli requisiti di spazio su disco: l’hardware è quindi un vincolo centrale.
Per valutare correttamente l’affermazione, partite dall’artefatto GitHub con ambiente fissato, leggete la dichiarazione del teorema prima del titolo e descrivete il risultato per quello che è: una grande formalizzazione assistita dall’AI di matematica già nota.