La formalizzazione dell’ultimo teorema di Fermat in Lean 4: quando l’IA riscrive la pratica matematica

La formalizzazione della matematica in Lean 4 e l’arrivo dell’intelligenza artificiale stanno ridefinendo cosa significa “dimostrare” un teorema. Non si tratta solo di automatizzare un compito tecnico: la possibilità di verificare dimostrazioni complesse con un kernel logico minimo cambia il rapporto tra matematico, macchina e conoscenza.

Dalla verifica alla co-costruzione

Per decenni la formalizzazione è stata vista come un’onerosa traduzione a posteriori: si prende una dimostrazione umana, già accettata dalla comunità, e la si riscrive in un linguaggio formale perché un computer la controlli. Il progetto Flyspeck (2003-2014) per la congettura di Keplero e la formalizzazione del teorema dei quattro colori (2005) hanno mostrato che il processo è possibile ma lentissimo: anni di lavoro per certificare risultati già noti.

Lean, avviato da Leonardo de Moura nel 2013, ha cambiato la scala del fenomeno. Lean 3 (2017) ha introdotto la metaprogrammazione in Lean stesso; Lean 4, sviluppato con Sebastian Ullrich a partire dal 2018 e rilasciato all’inizio del 2021, ha reso Lean un linguaggio di programmazione generale con compilazione a codice nativo. Mathlib, la libreria matematica comunitaria, ha superato il milione di righe di codice verificato e copre gran parte della matematica universitaria più parti di corsi di master e dottorato. La sua architettura — tipizzazione dipendente, metaprogrammazione, tactic framework — rende la formalizzazione più vicina alla pratica matematica reale.

“Formalizzazione di matematica è l’arte di tradurre la matematica su carta in un linguaggio di programmazione abbastanza ricco da capire i concetti di teoremi e dimostrazioni.”
— Kevin Buzzard, The Fermat’s Last Theorem Project, Lean Community Blog, 30 aprile 2024¹

Ma il vero salto è arrivato quando l’IA ha smesso di essere solo un “utente” di Lean per diventare co-autore. Nel settembre 2026 Anthropic ha annunciato che Claude, lavorando in gran parte autonomamente per 11 giorni, ha prodotto la prima dimostrazione formale end-to-end dell’ultimo teorema di Fermat in Lean 4: 13 milioni di righe di codice, 29.500 teoremi intermedi, zero sorry ammessi. Il risultato è stato verificato da Lean e confermato da Comparator, uno strumento che riesegue indipendentemente la compilazione.

Non era la prima volta che l’IA formalizzava matematica. AlphaProof di DeepMind aveva raggiunto l’argento all’IMO 2024; LeanDojo e Lean Copilot (Caltech, 2023-2025) usano modelli linguistici per suggerire tactic; TheoremLlama e LeanAgent esplorano l’autoformalizzazione end-to-end. Ma la dimostrazione di FLT segna una soglia: per la prima volta un sistema IA ha formalizzato da zero un risultato che richiede macchinari di livello ricerca (forme modulari, rappresentazioni di Galois, varietà di Shimura) senza che umani scrivessero i passaggi chiave.

Il collo di bottiglia della verifica

Perché formalizzare FLT ora, quando la dimostrazione di Wiles è accettata dal 1995? La risposta sta in un problema epistemico che la matematica contemporanea sta affrontando: il collo di bottiglia della verifica.

Thomas Hales ha impiegato quattro anni per far accettare la dimostrazione della congettura di Keplero; la congettura di Poincaré di Perelman ha richiesto quattro anni e tre esposizioni da 300 pagine; la congettura debole di Goldbach di Helfgott (2013) è ancora sotto revisione. Vladimir Voevodsky ha documentato personalmente come errori nei propri lavori (e in quelli di altri) siano rimasti scoperti per anni: nel 1999-2000, con Pierre Deligne che controllava i suoi passaggi, scoprì un errore in un lemma chiave del suo paper sul motivic cohomology (corretto nel 2006); nel 2013 riconobbe che un controesempio di Carlos Simpson al paper “∞-groupoids” (1989) con Kapranov era valido, dopo 14 anni in cui l’errore era sfuggito a tutti. La revisione paritaria tradizionale non scala: più la matematica avanza, più le dimostrazioni diventano lunghe, tecniche e frammentate tra sottocampi specializzati.

“Se l’autoformalizzazione di FLT è possibile ora, abbiamo fatto un grande passo verso l’autoformalizzazione della letteratura matematica moderna. Tali tecniche porteranno a nuovi strumenti, per scovare errori nel corpus matematico attuale e alleggerire il carico dei referee.”
— Kevin Buzzard, commento alla formalizzazione Anthropic di FLT, settembre 2026²

La formalizzazione assistita da IA promette di trasformare la verifica da collo di bottiglia a infrastruttura continua. Se ogni nuovo articolo fosse accompagnato da una formalizzazione in Lean (o Coq, Isabelle), la comunità potrebbe fidarsi del risultato senza doverne ricontrollare ogni passo a mano. Il paper diventerebbe “esposizione per umani”, la formalizzazione “certificato per macchine”.

Epistemologia della prova formale

Ma cosa guadagniamo davvero? James Weatherall e Jesse Wolfson (2026) argomentano che “non è né necessario né sufficiente per una dimostrazione matematica avere valore epistemico che sia ‘corretta’, nel senso di formalizzabile in un sistema di prova formale”³. La loro tesi: il valore epistemico di una dimostrazione sta nella comprensione che genera nel matematico, non nella sua verificabilità meccanica. Una dimostrazione formale può essere corretta ma opaca; una dimostrazione informale può essere illuminante pur contenendo passaggi “ovvi” che un kernel richiederebbe di espandere.

Questa tensione non è nuova. Già Turing nel 1939, nella tesi Systems of Logic Based on Ordinals, distingueva tra “intuizione” (fare salti logici non banali, giudizi spontanei non frutto di ragionamento cosciente) e “ingegnosità” (riempire i dettagli, disporre proposizioni per aiutare l’intuizione)⁴. I sistemi formali eccellono nell’ingegnosità; l’IA basata su LLM mostra sorprendente intuizione nel proporre strategie, ma nessuna garanzia di correttezza.

L’integrazione tra LLM e proof assistant cerca di combinare il meglio dei due mondi: l’LLM genera congetture, suggerisce tattiche, scrive bozze di formalizzazione; Lean le controlla, rifiuta quelle errate, costringe a correggere. Il ciclo di feedback — “prova, errore, correzione, riprova” — è ciò che rende sistemi come AlphaProof, HERMES (2025) e Lean Copilot efficaci.

“La dimostrazione matematica è la forma primaria di giustificazione della conoscenza matematica. Ma per contare come una dimostrazione matematica propria, e funzionare quindi propriamente come giustificazione per un pezzo di conoscenza matematica, una dimostrazione matematica deve essere rigorosa.”
— Yacin Hamami, Mathematical Rigor and Proof, The Review of Symbolic Logic 15(2), 409-449, 2022⁵

Il “Standard View” identificato da Hamami — una dimostrazione è rigorosa se può essere routinariamente tradotta in una dimostrazione formale — viene oggi messo alla prova proprio dall’IA: se un LLM può produrre la traduzione formale automaticamente, la distinzione tra “rigoroso informalmente” e “formalmente verificato” si assottiglia. Ma Weatherall e Wolfson avvertono: la formalizzazione rompe il legame con la semantica intesa dell’argomento informale. Il kernel controlla la sintassi logica, non il “significato” matematico.

Il progetto FLT come caso di studio

Il progetto FLT di Kevin Buzzard (Imperial College London, 2024-2029, finanziato EPSRC) illustra la nuova modalità di lavoro. Non si formalizza la dimostrazione originale di Wiles-Taylor, ma una variante moderna basata su forme automorfe quaternioniche (strategia di Khare-Wintenberger, modificata da Taylor). Il blueprint — un documento LaTeX di 86 pagine scritto da Buzzard e Taylor — scompone la dimostrazione in centinaia di lemmi, ciascuno assegnabile a contributori diversi. Il software leanblueprint di Patrick Massot traccia lo stato di ogni nodo (blu = pronto, verde = completato) e genera grafi di dipendenze.

“La bellezza del sistema: non devi capire tutta la dimostrazione di FLT per contribuire. Il blueprint scompone la dimostrazione in molti molti lemmi piccoli, e se riesci a formalizzare la dimostrazione di anche solo uno di quei lemmi, io aspetto con ansia la tua pull request.”
— Kevin Buzzard, The Fermat’s Last Theorem Project, 30 aprile 2024⁶

Questa modularità è cruciale. La formalizzazione tradizionale richiedeva che un singolo esperto (o un piccolo team) padroneggiasse l’intera catena logica. Con i blueprint e l’IA, la conoscenza può essere distribuita: l’esperto di teoria di Galois formalizza i suoi lemmi; l’esperto di forme modulari i suoi; l’IA riempie i passaggi “ovvi” ma noiosi. Il kernel di Lean garantisce che, quando tutti i nodi sono verdi, l’intera dimostrazione regge.

Anthropic ha mostrato che l’IA può andare oltre: invece di riempire i buchi lasciati dagli umani, può scrivere l’intera dimostrazione dato il blueprint. Il loro esperimento ha usato Prove2Me, una piattaforma che mantiene un DAG (grafo aciclico diretto) di enunciati per coordinare decine di agenti Claude in parallelo. Il risultato: 13 milioni di righe in 11 giorni, contro gli anni previsti per l’approccio umano.

Matematica come software

La formalizzazione in Lean ha un effetto collaterale profondo: trasforma la matematica in software. I file .lean sono codice: versionabili, testabili, refactorabili. Quando una definizione in Mathlib viene generalizzata, tutti i teoremi a valle si rompono (errore di compilazione) e vanno aggiornati — esattamente come in un codebase. Questo ha permesso a Bloom e Mehta (2022) di formalizzare il risultato di Erdős-Graham mentre l’articolo era sotto revisione, e a Scholze di verificare l’esperimento del tensore liquido in sei mesi.

Ma rende anche la matematica componibile. Il progetto CSLib (2025) sta costruendo un substrato per l’informatica teorica in Lean; TorchLean (2026) collega PyTorch a Lean per verificare reti neurali; StatLib (2026) formalizza statistica matematica. Ogni nuovo dominio si appoggia a Mathlib senza duplicare lavoro.

Il rischio della scatola nera

C’è un rischio: se l’IA produce dimostrazioni che nessun umano legge né capisce, la matematica diventa una scatola nera. Weatherall e Wolfson notano che “i matematici non sono giustificati nel credere proposizioni perché hanno dimostrazioni formali (quando le hanno). La freccia della dipendenza punta nell’altra direzione”. La fiducia in un risultato nasce dalla comprensione umana, non dal certificato del kernel.

La formalizzazione Anthropic di FLT è un caso limite: 13 milioni di righe che nessun umano leggerà per intero. Buzzard stesso ha detto che il codice generato da Claude “è scritto per essere controllato, non letto: i nomi sono generati, le etichette hanno suffissi esadecimali”⁷. Se questa diventa la norma, la matematica rischia di scindersi in due strati: uno leggibile (paper, esposizioni, blueprint) e uno verificabile (codice Lean generato da IA), con un ponte sempre più sottile tra i due.

La risposta della comunità è duplice. Da un lato, strumenti come Comparator e Lean Kernel Arena (2026) permettono di rieseguire indipendentemente la verifica, riducendo la fiducia richiesta nel generatore. Dall’altro, si insiste sull’importanza dei blueprint leggibili come interfaccia umana: il blueprint di FLT è scritto in LaTeX, con spiegazioni matematiche, non solo elenchi di statement Lean. L’IA riempie i dettagli; l’umano mantiene la mappa concettuale.

Verso una nuova pratica matematica

La convergenza tra formalizzazione, IA e collaborazione distribuita sta creando una “nuova pratica matematica” (Jeremy Avigad, CMU, 2026). Tre pilastri:

1. Formalizzazione come standard: non più opzionale per risultati di frontiera, ma attesa come parte della pubblicazione (analogo: test suite per software).
2. IA come co-autore formale: LLM che scrivono Lean, non solo LaTeX; autoformalizzazione come servizio (Prove2Me, Lean Copilot, HERMES).
3. Collaborazione a scala: blueprint modulari, contributi paralleli, kernel come arbitro finale.

Il caso FLT mostra che siamo all’inizio. La formalizzazione umana di FLT (progetto Buzzard) punta a ridurre il teorema a risultati noti negli anni ’80 entro il 2029; l’autoformalizzazione Anthropic ha saltato la coda e ha prodotto tutto in due settimane. La differenza sta nell’approccio: umano = bottom-up, costruendo librerie riutilizzabili; IA = top-down, generando codice monolitico per un obiettivo specifico.

Il futuro probabile è ibrido: umani definiscono l’architettura (blueprint, definizioni chiave, lemmi strategici); IA riempie i dettagli, suggerisce generalizzazioni, scopre scorciatoie; kernel verifica tutto. Mathlib cresce come infrastruttura condivisa; i paper diventano “blueprint eseguibili”.

Conclusione

La formalizzazione dell’ultimo teorema di Fermat in Lean 4 da parte di un’IA non è solo un record tecnico. È la prova che il collo di bottiglia della verifica può essere rotto. Ma solleva una domanda epistemica: se la matematica diventa verificabile ma non leggibile, abbiamo guadagnato o perso?

La risposta sta nel mantenere il legame con la comprensione umana. I blueprint, le esposizioni, i commenti nel codice, le scelte di denominazione — tutto ciò che rende una formalizzazione leggibile, non solo corretta — sono la garanzia che la matematica resti un’attività umana, anche quando le macchine ne scrivono i passaggi più noiosi.

Come scriveva Turing: “Possiamo vedere solo una breve distanza avanti, ma possiamo vedere abbastanza da capire che c’è molto da fare”⁸. La formalizzazione assistita da IA è il nuovo microscopio: ci mostra dettagli che non avremmo mai potuto controllare a mano. Sta a noi decidere cosa guardare.

Note

1. “Formalisation of mathematics is the art of translating paper mathematics into a computer programming language rich enough to understand the concepts of theorems and proofs.” — Kevin Buzzard, The Fermat’s Last Theorem Project, Lean Community Blog, 30 aprile 2024. https://leanprover-community.github.io/blog/posts/FLT-announcement/ ↩

1. “If the automatic formalization of FLT is possible now, then we have taken a big step towards automatic formalization of the modern mathematical literature. Such autoformalization techniques will lead to new tools, rooting out errors in the current mathematical corpus and lightening the load of referees.” — Kevin Buzzard, commento alla formalizzazione Anthropic di FLT, settembre 2026. https://www.anthropic.com/research/formalizing-fermats-last-theorem ↩

1. “We argue that it is neither necessary nor sufficient for a mathematical proof to have epistemic value that it be ‘correct’, in the sense of formalizable in a formal proof system.” — James Owen Weatherall, Jesse Wolfson, Correctness, Artificial Intelligence, and the Epistemic Value of Mathematical Proof, arXiv:2602.12463, febbraio 2026. ↩

1. “Mathematical reasoning may be regarded rather schematically as the exercise of a combination of two faculties, which we may call intuition and ingenuity. The activity of the intuition consists in making spontaneous judgments which are not the result of conscious trains of reasoning… The exercise of ingenuity in mathematics consists in aiding the intuition through suitable arrangements of propositions, and perhaps geometrical figures or drawings.” — A. M. Turing, Systems of Logic Based on Ordinals, Proc. London Mathematical Society, Series 2, Vol. 45, 1939, pp. 161-228 (PhD thesis, Princeton 1938). ↩

1. “Mathematical proof is the primary form of justification for mathematical knowledge, but in order to count as a proper justification for a piece of mathematical knowledge, a mathematical proof must be rigorous.” — Yacin Hamami, Mathematical Rigor and Proof, The Review of Symbolic Logic 15(2), 409-449, 2022. https://doi.org/10.1017/S1755020321000438 ↩

1. “The beauty of the system: you do not have to understand the whole proof of FLT in order to contribute. The blueprint breaks down the proof into many many small lemmas, and if you can formalise a proof of just one of those lemmas then I am eagerly awaiting your pull request.” — Kevin Buzzard, The Fermat’s Last Theorem Project, Lean Community Blog, 30 aprile 2024. https://leanprover-community.github.io/blog/posts/FLT-announcement/ ↩

1. “is written to be checked, not read: the names are generated, the labels have hexadecimal suffixes” — Kevin Buzzard, commento alla formalizzazione Anthropic di FLT, settembre 2026. https://www.anthropic.com/research/formalizing-fermats-last-theorem ↩

1. “We can only see a short distance ahead, but we can see plenty there that needs to be done.” — A. M. Turing, Computing Machinery and Intelligence, Mind, Vol. 59, No. 236, ottobre 1950, pp. 433-460. ↩

Fonti

• Kevin Buzzard, The Fermat’s Last Theorem Project, Lean Community Blog, 30 aprile 2024. https://leanprover-community.github.io/blog/posts/FLT-announcement/
• Anthropic, Formalizing Fermat’s Last Theorem, 4 settembre 2026. https://www.anthropic.com/research/formalizing-fermats-last-theorem
• James Owen Weatherall, Jesse Wolfson, Correctness, Artificial Intelligence, and the Epistemic Value of Mathematical Proof, arXiv:2602.12463, febbraio 2026.
• Xichen Tang, A Comprehensive Survey of the Lean 4 Theorem Prover: Architecture, Applications, and Advances, arXiv:2501.18639, gennaio 2025.
• Xichen Tang, Mathematical Formalized Problem Solving and Theorem Proving in Different Fields in Lean 4, arXiv:2409.05977, settembre 2024.
• LeanDojo Team, AI-Driven Formal Theorem Proving in the Lean Ecosystem, leandojo.org (accesso settembre 2026).
• Lean FRO, About the Lean FRO, lean-lang.org/fro/about (accesso settembre 2026).
• American Mathematical Society, Mathematics and the formal turn, Bulletin of the AMS, 2024.
• Communications of the ACM, Formal Reasoning Meets LLMs: Toward AI for Mathematics and Verification, febbraio 2026.
• Manooshree Patel et al., LeanTutor: Towards a Verified AI Mathematical Proof Tutor, arXiv:2506.08321v2, marzo 2026.
• Vladimir Voevodsky, The Origins and Motivations of Univalent Foundations, IAS Ideas, 2014. https://www.ias.edu/ideas/2014/voevodsky-origins
• Yacin Hamami, Mathematical Rigor and Proof, The Review of Symbolic Logic 15(2), 409-449, 2022.
• A. M. Turing, Systems of Logic Based on Ordinals, Proc. London Mathematical Society, Series 2, Vol. 45, 1939.
• A. M. Turing, Computing Machinery and Intelligence, Mind, Vol. 59, No. 236, ottobre 1950.