Assistente di dimostrazione Lean e IA: come le dimostrazioni diventano verificabili dalle macchine

Undici giorni, uno sciame di agenti, 13 milioni di righe di codice: un'IA ha reso la dimostrazione dell'ultimo teorema di Fermat verificabile dalle macchine. A fare la differenza non è stata tanto la potenza di calcolo, quanto un verificatore che non lascia passare nessun errore.

Intorno al 1637 Pierre de Fermat annotò a margine di un libro un'affermazione per la quale diceva di possedere una dimostrazione. Non fu mai ritrovata. Solo nel 1995 Andrew Wiles pubblicò una dimostrazione completa. Il 4 settembre 2026 Anthropic ha annunciato che uno sciame di agenti Claude ha formalizzato per intero questa dimostrazione nel linguaggio Lean. Ciò è stato possibile grazie all'assistente di dimostrazione Lean, che verifica meccanicamente ogni passaggio di una dimostrazione.

Questo articolo inquadra l'annuncio. Spiega che cos'è un assistente di dimostrazione e perché un risultato ottenuto in Lean è considerato affidabile. Descrive come hanno collaborato gli agenti e colloca l'annuncio accanto ai problemi delle Olimpiadi e ai problemi di Erdős. Dati verificati, dichiarazioni dei produttori e questioni aperte restano distinti. La tesi: la novità non è solo che un'IA fa matematica. La novità è la combinazione di un modello libero di sperimentare e di un programma che approva ogni passaggio senza compromessi.

L'ultimo teorema di Fermat: che cosa ha annunciato davvero Anthropic

Il teorema afferma che l'equazione aⁿ + bⁿ = cⁿ non ha soluzioni in numeri interi positivi per un esponente n maggiore di 2. L'enunciato è facile da capire ed è stato per secoli estremamente difficile da dimostrare. Nel 1908 fu istituito un premio di 100.000 marchi d'oro e, secondo Anthropic, nel primo anno arrivarono 621 dimostrazioni errate. Wiles presentò una dimostrazione nel 1993, trovò una lacuna e la colmò insieme a Richard Taylor. La pubblicazione seguì nel maggio 1995.

L'annuncio più recente riguarda la domanda su quanto sia sicura questa dimostrazione quando ogni passaggio viene verificato da una macchina. I dati principali della pubblicazione di Anthropic sono riportati nella tabella.

Un token è una piccola unità di testo generata da un modello linguistico, per esempio una parte di parola. La fonte non indica costi in denaro. Tutti i dati provengono dal produttore e in questa forma non sono stati ricontati in modo indipendente.

La distinzione è importante. Si tratta di una formalizzazione, non di una nuova dimostrazione. Il teorema era dimostrato dal 1995. Secondo Anthropic, gli agenti si sono basati su una versione semplificata della dimostrazione di Wiles ad opera di Darmon, Diamond e Taylor e hanno ripreso parti del progetto di formalizzazione dell'Imperial College e del progetto flt-regular. Chi legge di una soluzione dell'ultimo teorema di Fermat da parte di un'IA dovrebbe quindi pensare a una verifica, non a una nuova scoperta matematica. Anthropic distingue esplicitamente il risultato dal lavoro dell'IA sull'ipotesi di Riemann, in cui sarebbe stato scoperto qualcosa di nuovo.

Che cos'è Lean? Un assistente di dimostrazione che non salta nessun passaggio

L'assistente di dimostrazione Lean è un linguaggio di programmazione open source con cui si possono scrivere dimostrazioni matematiche in una forma che un computer è in grado di verificare. Il sito del progetto lean-lang.org descrive Lean come linguaggio di programmazione e assistente di dimostrazione con un nucleo minimo e affidabile che garantisce la correttezza. Lean è stato sviluppato da Leonardo de Moura e rilasciato come open source nel 2013, come riferisce la Simons Foundation. Dal 2023 l'organizzazione non profit Lean FRO ne cura lo sviluppo, sostenuta tra l'altro con 5 milioni di dollari dalla Simons Foundation International.

Il principio si può spiegare in parole semplici. Una dimostrazione in Lean è un programma. Il nucleo di Lean verifica passo dopo passo se ogni deduzione discende dagli assiomi e dai teoremi già verificati. Gli assiomi sono le ipotesi di base della matematica, che valgono senza dimostrazione. Un passaggio che non segue viene rifiutato, per quanto convincente possa sembrare. Dove manca ancora una dimostrazione, Lean usa il segnaposto «sorry». Una dimostrazione con tali segnaposto è considerata incompleta.

Proprio questo rende Lean così utile per i modelli di IA. I modelli linguistici sanno esprimersi in modo convincente e tuttavia sbagliare. In matematica è un problema, perché un errore al passaggio 400 può invalidare tutto ciò che segue. Con un assistente di dimostrazione come Lean la questione se credere al modello non si pone più.

La revisione umana funziona in modo diverso. Gli esperti leggono una dimostrazione, la ritengono plausibile e si affidano alla propria esperienza. È prezioso, ma richiede tempo e lascia spazio a sviste. Già nel 2021 un progetto collettivo ha convalidato in Lean una dimostrazione complessa di Peter Scholze, come descrive la Simons Foundation. Il controllo dell'assistente di dimostrazione non sostituisce la comprensione matematica, ma offre certezza sulla correttezza.

Il processo nella figura 1 mostra la divisione dei compiti: il modello avanza proposte, il nucleo di Lean decide. Che una proposta provenga da una persona, da un modello o da un generatore casuale non incide sul verdetto.

Mathlib e la questione di chi verifica ciò che è stato verificato

Lean da solo non contiene matematica. Questa si trova in Mathlib, la libreria sviluppata dalla comunità su cui si basano quasi tutte le formalizzazioni. Il sito di Lean parla di più di un milione di righe. La pagina delle statistiche della comunità riportava al momento della consultazione 139.391 definizioni, 290.502 teoremi e 772 collaboratori. Chi dimostra qualcosa in Lean può attingere a questi mattoni già verificati invece di partire da zero.

Per confronto: la dimostrazione di Fermat conta, secondo Anthropic, circa 13 milioni di righe, ed è quindi più di cinque volte più grande di Mathlib. Sembra un'enorme costruzione ex novo, ma mostra anche quanto costi la verifica formale di teoremi profondi, anche quando Mathlib fornisce le fondamenta. La dimostrazione dipende da ciò che è già stato formalizzato in Mathlib.

Vanno poste separatamente due domande di verifica. Primo: la dimostrazione è corretta? A questo risponde Lean. Anthropic dichiara che vengono usati solo i tre assiomi standard. Secondo: è stato dimostrato davvero l'ultimo teorema di Fermat e non un enunciato modificato? Qui è stato impiegato uno strumento di confronto, che ha confermato che l'enunciato formalizzato coincide con la formulazione in Mathlib. Questa separazione è decisiva. Una dimostrazione impeccabile di un enunciato sbagliato sarebbe inutile.

La dimostrazione completa, con una spiegazione scritta, è disponibile secondo Anthropic su GitHub e vi si può consultare. Non è pubblico solo il modello utilizzato.

Kevin Buzzard dell'Imperial College London, che dirige il progetto di formalizzazione dal 2024, ha controllato la dimostrazione. Secondo Anthropic, egli afferma che il teorema è dimostrato senza ipotesi diverse dagli assiomi della matematica. Resta un limite: Lean verifica la correttezza, non il significato. Se un risultato sia interessante, elegante o importante, lo strumento non lo giudica. La Simons Foundation riporta valutazioni in questo senso di Alex Kontorovich.

IA agentica: perché lo sciame ha funzionato

Diverse decine di agenti hanno lavorato in parallelo. In questo contesto un agente è un modello linguistico che non si limita a rispondere, ma usa autonomamente strumenti, modifica file e controlla risultati intermedi. La struttura multi-agente si basava su Claude Code. Gli agenti hanno definito concetti, dimostrato risultati intermedi e li hanno usati per enunciati più difficili. Un'introduzione generale è offerta dall'articolo Das Zeitalter der KI-Agenten.

Secondo Anthropic, la svolta non è arrivata da un modello più potente, ma da un'organizzazione migliore. La piattaforma Prove2Me, una piattaforma di collaborazione aperta di Tianyi Peng e colleghi della Columbia University, offriva tre caratteristiche:

• Un grafo aciclico orientato degli enunciati dei teoremi dava orientamento: ogni enunciato mostra da che cosa dipende e non ci sono cicli.
• Enunciati e dimostrazioni si trovavano in file separati. Questo accelera la compilazione di Lean, perché a ogni modifica non occorre ricontrollare tutto.
• I teoremi già dimostrati potevano essere cercati e riutilizzati tramite descrizioni in linguaggio naturale.

I tentativi precedenti, privi di questa struttura, fallirono perché gli agenti perdevano il filo dello stato del progetto. È significativo che questi tentativi abbiano comunque fornito circa il 7 per cento delle righe non banali della dimostrazione finale. La lezione: nei compiti grandi la struttura batte la pura potenza del modello. Chi impiega molti agenti ha bisogno di un piano comune, di un archivio condiviso e di responsabilità chiare. Gli sviluppatori fanno la stessa esperienza in ogni progetto di agenti di una certa dimensione.

Il contributo umano è stato ridotto, ma non nullo. Tianyi Peng ha dato di tanto in tanto istruzioni di livello superiore, per esempio dare priorità alla varietà jacobiana come schema o concludere presto il teorema di Mazur. Secondo l'output citato degli agenti, il sistema ha segnalato il risultato radice come dimostrato il 18 agosto alle 02:00:57 UTC.

Dalle Olimpiadi ai problemi di Erdős: le dimostrazioni dell'IA dal 2024

L'annuncio su Fermat non è isolato. Dal 2024 diversi risultati mostrano che l'IA sa dimostrare in matematica, e si differenziano per l'uso o meno di Lean.

Nel luglio 2024 AlphaProof insieme ad AlphaGeometry 2 ha risolto quattro problemi su sei delle Olimpiadi Internazionali della Matematica, ottenendo 28 punti su 42, livello argento. La soglia dell'oro era di 29 punti. AlphaProof dimostra in Lean e ha risolto, tra l'altro, il problema più difficile della gara. Tuttavia i problemi erano stati prima tradotti a mano in linguaggio formale e il tempo di calcolo è stato fino a tre giorni per problema. I concorrenti hanno due sessioni di 4,5 ore.

Nel luglio 2025 Gemini Deep Think ha ottenuto 35 punti su 42, livello oro, valutato ufficialmente dai coordinatori delle Olimpiadi. Il sistema ha lavorato in linguaggio naturale entro il limite di tempo e senza Lean. È un contrasto voluto: anche senza verifica formale l'IA diventa forte, ma i risultati non sono allora verificati meccanicamente e devono essere letti da persone. L'azienda Harmonic descrive in una pubblicazione su arXiv il suo sistema Aristotle, che unisce la ricerca di dimostrazioni basata su Lean, il ragionamento informale e un risolutore di geometria e, secondo l'abstract, raggiunge prestazioni di livello oro sui problemi del 2025.

All'inizio del 2026 sono finiti sotto i riflettori i problemi di Erdős, una vasta raccolta di questioni aperte del matematico Paul Erdős. Un esempio è il problema 728, la cui dimostrazione da parte di Aristotle in Lean è documentata in una elaborazione su arXiv. Secondo la Simons Foundation, inoltre, un ventitreenne ha risolto all'inizio del 2026 il problema 1196 con ChatGPT e Lean.

La valutazione è prudente. Il wiki di Terence Tao sui contributi dell'IA ai problemi di Erdős dichiara espressamente di non essere un benchmark. Segnala un bias di selezione, perché i successi vengono documentati più dei fallimenti. Osserva che la mancanza di progressi precedenti indica spesso scarsa notorietà e non difficoltà, che a posteriori è emersa spesso letteratura già esistente e che un problema risolto non è automaticamente un lavoro pronto per la pubblicazione. Allo stesso tempo il wiki raccomanda di verificare formalmente in Lean le dimostrazioni dell'IA.

Il campo delle dimostrazioni dell'IA in matematica va dai problemi di gara ai problemi marginali fino alle grandi formalizzazioni. Lo sviluppo procede in fretta; se ogni annuncio mantenga ciò che il titolo promette va verificato caso per caso. È proprio a questo che serve uno strumento di verifica come Lean.

Quanto valgono 11 giorni? Un confronto temporale senza esagerazioni

I numeri invitano a grandi paragoni. Fermat formulò il teorema nel 1637, Wiles lo dimostrò nel 1995: sono 358 anni. Il progetto di formalizzazione all'Imperial College è stato avviato nel 2024, con un blueprint di 86 pagine, ed era pensato in origine per durare diversi anni. La formalizzazione dell'IA è durata 11 giorni.

Questo confronto zoppica per diversi motivi:

• Gli 11 giorni sono la durata di esecuzione di uno sciame di agenti, non il tempo di calcolo di un singolo modello.
• La dimostrazione era nota. L'IA non doveva trovare un'idea nuova, ma tradurre in Lean una struttura di dimostrazione esistente.
• C'era un lavoro preliminare: Mathlib, materiale del progetto dell'Imperial College e di flt-regular, oltre a un blueprint.
• Lo sforzo di circa sei miliardi di token di output di un modello interno è considerevole. I costi in denaro non sono indicati.

Equiparare 11 giorni di lavoro dell'IA a secoli di lavoro umano sul problema è quindi solo un paragone retorico. È vero invece che un lavoro che un progetto collettivo aveva pianificato su più anni è stato in sostanza completato in pochi giorni.

Un esperimento collaterale porta lo sguardo sull'uso quotidiano. Secondo Anthropic, tre abbonamenti personali a Claude Max hanno formalizzato in tre giorni il teorema dei tre numeri primi di Vinogradov. Gli autori ritengono possibile una formalizzazione collettiva con abbonamenti consumer, se la struttura è adeguata. Si tratta di una valutazione degli autori e non di un risultato verificato in modo indipendente.

Limiti e punti aperti: che cosa l'annuncio non mostra

Anthropic stessa indica dei limiti. La dimostrazione è probabilmente molto più lunga del necessario, perché Mathlib è più compatta e meglio rivista. Dipende da ciò che è già stato formalizzato in Mathlib. Il modello usato è un modello di ricerca interno, non pubblico, per cui il risultato non può essere ripetuto dall'esterno con gli stessi mezzi.

Restano aperti altri punti:

• Non è stata prodotta nuova matematica. La formalizzazione accresce la certezza, non la conoscenza.
• Una dimostrazione in Lean non è automaticamente comprensibile. Nessuno legge 13 milioni di righe dall'inizio alla fine.
• Lean non dice nulla sul significato di un teorema, ma solo sulla sua correttezza.
• Quanto sia indipendente la verifica oltre alla valutazione di Buzzard non emerge dall'annuncio.

Per altri annunci singoli, per esempio sui progressi nell'ipotesi di Riemann o sugli agenti di autoformalizzazione di singole aziende, in questa ricerca non sono disponibili fonti primarie verificabili in autonomia. Questi annunci restano quindi qui senza numeri. Anche le valutazioni di singoli esperti vengono riprese solo se è disponibile la dichiarazione originale.

Che cosa significa l'approccio di Lean oltre la matematica

Lo schema alla base del progetto Fermat è generalizzabile: libera sperimentazione da una parte, rigorosa approvazione dall'altra. Si adatta ovunque un risultato possa essere verificato da una macchina. Come applicazioni al di fuori della matematica il sito di Lean cita la verifica di ArkLib, una libreria per SNARK (prove crittografiche compatte), e di Cedar, il linguaggio di autorizzazione di AWS. Nello sviluppo software il principio è noto: anche un compilatore e un'esecuzione di test approvano ciò che ha scritto una persona o un'IA.

Per il modo di trattare gli output dell'IA ne deriva una regola pratica. Quanto meglio un risultato si lascia verificare in automatico, tanto più sicuramente un modello può lavorare liberamente. Per testi, valutazioni e raccomandazioni questa approvazione rigorosa di solito manca. Lì il verificatore resta l'uomo.

La stessa logica vale per sicurezza e protezione dei dati: le proprietà dimostrabili contano più delle semplici affermazioni. Se un sito web carichi tracker o imposti header di sicurezza, per esempio, si può misurare in modo automatizzato. Per questo il Webseiten-Check di Dr. DSGVO offre una possibilità, e le proprietà tecniche di sicurezza si possono controllare con i Security-Checks. Entrambi non sono dimostrazioni formali nel senso di Lean, ma seguono la stessa idea: misurare invece di credere.

Esperimenti di Dr. DSGVO

Con l'aiuto dell'IA è stata fornita (probabilmente) la dimostrazione matematica, poi formalizzata, che gli esagoni magici secondo una certa regola di costruzione esistono per qualsiasi n (n = lunghezza del lato di un esagono in celle a nido d'ape).

Il tempo di calcolo complessivo dell'IA è stato di poco inferiore a 9 ore. Di queste, il sistema ha lavorato in autonomia per quasi il 99,9% del tempo, senza bisogno di input. I file della dimostrazione occupavano 173 MB! La formalizzazione con Lean, comprese le librerie, ha consumato quasi 8 GB di spazio su disco, nei passaggi intermedi! L'intera dimostrazione si è estesa su un arco di 5 giorni. È stata interrotta a causa di limiti d'uso e simili.

A breve la dimostrazione sarà pubblicata qui. Se sia corretta dovranno giudicarlo persone competenti, che capiscono di matematica più dell'autore, che ha usato l'IA 😉

Conclusione: la rivoluzione è la verificabilità

L'IA non ha dimostrato di nuovo l'ultimo teorema di Fermat, ma ha formalizzato per intero in Lean la dimostrazione di Wiles, secondo Anthropic in 11 giorni con diverse decine di agenti in parallelo. Il successo poggia su due cose: un'organizzazione che mantiene visibile lo stato del progetto e l'assistente di dimostrazione Lean, che accetta solo ciò che discende logicamente.

Gli sviluppi dal 2024 mostrano che l'IA fornisce sempre più dimostrazioni matematiche. Quanto ci sia di nuovo e quanto di materiale noto va giudicato caso per caso, come ammonisce anche il wiki di Tao. Dove c'è Lean, la correttezza resta verificabile. È questo il vero progresso: non più affermazioni, ma certezza verificata meccanicamente.