Il risultato annunciato da Anthropic il 4 settembre 2026 non è la scoperta di una nuova soluzione al teorema di Fermat. Il teorema era già stato dimostrato nel 1994 da Andrew Wiles. La novità riguarda il modo in cui una macchina può verificare una dimostrazione. Agenti basati su Claude hanno lavorato per 11 giorni, autonomamente, per trasformare il teorema in una versione scritta nel linguaggio Lean, progettato per verificare i passaggi matematici. Anthropic lo presenta come la prima dimostrazione completa del teorema verificata da un computer. L’esperimento sposta così l’attenzione dall’AI che risponde a un problema all’AI che costruisce un oggetto matematico controllabile da un sistema indipendente.
Il teorema, formulato da Pierre de Fermat nel Seicento, afferma che non esistono tre interi positivi x, y e z capaci di soddisfare x alla n più y alla n uguale z alla n quando n è maggiore di 2. La frase è semplice, la dimostrazione no. Wiles arrivò alla soluzione dopo anni di lavoro. Il risultato, completato con Richard Taylor, valse a Wiles l’Abel Prize nel 2016. Claude non ha quindi sostituito quella scoperta. Ha preso un percorso già noto e lo ha tradotto in una forma che Lean può verificare riga per riga. È una distinzione importante. Non siamo davanti a una nuova soluzione del problema di Fermat, ma alla sua formalizzazione automatica.
La scala del lavoro spiega l’attenzione della comunità matematica. Per Anthropic, Claude ha prodotto circa 13 milioni di righe di codice Lean, dimostrando circa 30.300 teoremi intermedi, dei quali circa 29.500 sono confluiti nella versione finale. Il risultato è nato da più agenti che hanno suddiviso il problema, provato strategie e corretto gli errori. Una prova formalizzata deve rispettare regole verificabili automaticamente. L’obiettivo non è chiedere fiducia al chatbot, ma ridurre il più possibile la necessità di fidarsi del chatbot.
La reazione degli esperti mostra la portata del passaggio. Nature ha raccolto il commento di Alex Kontorovich, matematico della Rutgers University, che ha detto che la capacità di una macchina di trasformare il lavoro dei matematici in una prova di questa scala lo ha “completamente lasciato senza parole”. Kevin Buzzard, matematico dell’Imperial College London, ha definito il problema affrontato da Claude un ordine di grandezza più difficile di altri esperimenti recenti. Daniel Litt, matematico dell’Università di Toronto, ha sintetizzato l’impressione con una frase: “Se riescono a formalizzare l’ultimo teorema di Fermat, probabilmente possono formalizzare qualsiasi cosa”. I giudizi mostrano una crescente capacità di tradurre ragionamenti complessi in strutture verificabili.
Resta però un punto essenziale. La prova prodotta da Claude è enorme e non rappresenta una nuova dimostrazione matematica nel senso classico. Le circa 13 milioni di righe comprendono anche il codice necessario alla formalizzazione. La forza sta nella verificabilità. Il codice è stato controllato attraverso Lean e la catena di verifica serve a stabilire che il risultato corrisponda al teorema. È diverso da una spiegazione plausibile generata da un chatbot, che potrebbe contenere errori. Qui il controllo finale non dipende dal fatto che Claude abbia ragione quando lo afferma, ma dal fatto che il sistema formale accetti la prova.
Il vero interesse emergerà nei prossimi anni. Se strumenti di questo tipo riuscissero a formalizzare rapidamente nuove dimostrazioni, potrebbero aiutare i matematici a controllare risultati e individuare errori. Anthropic aveva già mostrato progressi di Claude nella ricerca matematica. Il caso Fermat aggiunge un tassello: l’AI non sta semplicemente cercando una risposta, ma sta imparando a costruire dimostrazioni che una macchina può verificare senza affidarsi alla sua parola. Per ora è un esperimento di formalizzazione, non una sostituzione dei matematici. Se il processo diventasse più compatto ed economico, il confine tra strumento e collaboratore scientifico potrebbe diventare più sottile.
Le aziende tech sono la "nuova Accademia": il vincitore del Nobel per la Matematica si unisce a OpenAI
Jacob Tsimerman, folgorato dall'AI Safety, aveva già calcolato in un…
