Non è stata l’AI a scoprire la soluzione del teorema di Fermat. Il vero passo avanti è un altro: riuscire a trasformare una dimostrazione matematica complessa in qualcosa che una macchina può verificare autonomamente.
Quella del 4 settembre sembrerebbe, a prima vista, l’ennesima notizia su quanto sia diventata intelligente l’AI: Anthropic ha annunciato la prima formalizzazione completa e verificata dal computer dell’Ultimo Teorema di Fermat, realizzata da Claude in circa 11 giorni.
Ma non è stata l’AI a dimostrare per la prima volta il celeberrimo teorema.
La dimostrazione era già arrivata nel 1995, quando Andrew Wiles pubblicò la prova che aveva richiesto anni di lavoro e una lunga fase di verifica da parte della comunità matematica.
Quello che è successo oggi è diverso, e forse ancora più interessante per capire dove può andare l’AI.
Claude ha preso una dimostrazione matematica esistente e l’ha trasformata in una formalizzazione nel linguaggio Lean, producendo una prova che può essere verificata automaticamente da un computer. Secondo Anthropic, il sistema ha lavorato per 11 giorni, generando circa 13 milioni di righe di codice Lean e dimostrando 30.300 teoremi lungo il percorso, 29.500 dei quali utilizzati nella prova finale.
Il punto, quindi, non è che l’AI abbia risolto un problema matematico rimasto irrisolto per secoli.
Il punto è che ha contribuito a trasformare una dimostrazione comprensibile e verificabile dagli esseri umani in una dimostrazione verificabile formalmente da una macchina.
Ed è qui che la storia diventa interessante anche al di fuori della matematica.
Il problema non è solo generare una risposta, ma sapere se è corretta
Uno dei limiti più evidenti degli LLM è ormai noto.
Un modello può produrre una risposta estremamente convincente e, allo stesso tempo, completamente sbagliata.
Il problema non è necessariamente la capacità di generare testo. È la difficoltà di stabilire, in modo autonomo e affidabile, se quello che è stato generato corrisponda effettivamente alla realtà.
In molti ambiti non esiste infatti un meccanismo formale che permetta alla macchina di controllare automaticamente il proprio output.
Se chiediamo a un LLM di scrivere una spiegazione, elaborare un’analisi o proporre un’interpretazione, possiamo farla controllare da un essere umano. Ma il controllo umano rimane necessario proprio perché non esiste sempre un criterio automatico e rigoroso con cui stabilire che la risposta sia corretta.
In matematica, almeno in parte, questo problema può essere affrontato diversamente.
Esiste infatti la possibilità di rappresentare concetti, assunzioni e passaggi logici all’interno di un sistema formale.
È quello che permette di fare un proof assistant come Lean.
Che cosa significa “formalizzare” una dimostrazione
Una dimostrazione matematica scritta per un essere umano non contiene necessariamente ogni singolo passaggio.
Il matematico può dare per scontate alcune implicazioni, utilizzare risultati già dimostrati o saltare passaggi che considera evidenti per chi legge.
Per un computer non funziona così.
Per poter verificare una dimostrazione, ogni passaggio deve essere espresso in una forma che il sistema sia in grado di controllare.
Lean è un linguaggio e un ambiente per la formalizzazione della matematica che permette di rappresentare definizioni, teoremi e dimostrazioni in una forma verificabile. Il sistema può quindi controllare che i passaggi rispettino le regole logiche previste.
Ed è proprio qui che si trova la difficoltà.
Formalizzare una dimostrazione già esistente non significa semplicemente “tradurre un testo”.
Significa trasformare il ragionamento matematico in una sequenza di elementi formalmente verificabili.
Nel caso dell’Ultimo Teorema di Fermat, l’impresa è particolarmente significativa perché la dimostrazione di Wiles è estremamente complessa e utilizza risultati provenienti da diversi ambiti della matematica.
Anthropic racconta che il progetto di formalizzazione della comunità matematica, avviato nel 2024 sotto la guida di Kevin Buzzard all’Imperial College London, era stato concepito come un lavoro destinato a durare anni. Il solo blueprint utilizzato per descrivere la fase iniziale del progetto conta 86 pagine.
Claude ha completato questo processo in 11 giorni.
Fermat non è stato “risolto” dall’AI
Vale la pena fermarsi su questo punto, perché è facile che il titolo della notizia generi una percezione sbagliata.
L’Ultimo Teorema di Fermat era già stato dimostrato da Andrew Wiles nel 1995.
La novità non è quindi una nuova dimostrazione del teorema.
È la formalizzazione automatizzata della dimostrazione.
Anthropic stessa sottolinea che ciò che è nuovo in questo lavoro non è una nuova scoperta matematica, ma la verifica: una dimostrazione che viene trasformata in una forma che il computer può controllare.
La distinzione è importante.
Da una parte abbiamo un sistema che genera un possibile ragionamento.
Dall’altra abbiamo un sistema che può verificare formalmente se quel ragionamento soddisfa determinate regole.
Questa seconda capacità è particolarmente interessante perché introduce un meccanismo di controllo sul lavoro prodotto dall’AI.
Il salto interessante: dall’AI che genera all’AI che verifica
È qui che il caso Fermat diventa più interessante rispetto alla semplice dimostrazione delle capacità matematiche di un LLM.
Gli LLM sono molto bravi a produrre ipotesi, testo, codice e percorsi di soluzione.
Ma generare qualcosa e verificarne autonomamente la correttezza sono due problemi diversi.
Nel caso di Lean, il sistema fornisce un ambiente formale nel quale la validità della dimostrazione può essere controllata.
Claude non si è quindi limitato a produrre una lunga sequenza di passaggi e a dichiararla corretta.
Ha lavorato all’interno di un sistema nel quale quei passaggi dovevano essere accettati dal proof assistant.
Secondo Anthropic, il processo ha coinvolto decine di agenti Claude che hanno collaborato nella definizione dei concetti, nella dimostrazione dei teoremi intermedi e nella costruzione progressiva della prova. Il lavoro è stato coordinato attraverso Prove2Me, una piattaforma sviluppata da Tianyi Peng e dai suoi collaboratori alla Columbia University.
Questo introduce un modello di lavoro interessante:
generare → verificare → correggere → proseguire.
È molto diverso dal semplice “fai una domanda all’AI e ricevi una risposta”.
Il ruolo dell’harnessing: l’autonomia non nasce dal nulla
C’è però un altro aspetto importante.
Non stiamo osservando un’intelligenza artificiale completamente autonoma che decide da sola cosa fare dall’inizio alla fine.
Il risultato è stato possibile grazie a un ambiente costruito dagli esseri umani.
Anthropic descrive infatti l’utilizzo di un multi-agent harness basato su Claude Code e Prove2Me. La piattaforma mantiene un grafo delle dipendenze tra i teoremi, permette agli agenti di decidere quali dimostrazioni affrontare successivamente e facilita il lavoro parallelo e il riutilizzo dei risultati già ottenuti.
Questo punto è fondamentale.
L’autonomia che vediamo non è separata dall’infrastruttura che la rende possibile.
Gli esseri umani definiscono il problema, costruiscono gli strumenti, stabiliscono il contesto e forniscono indicazioni di alto livello. Gli agenti operano poi all’interno di questo ambiente e ricevono un criterio esterno con cui verificare il proprio lavoro.
È una forma di autonomia vincolata e verificabile.
Ed è probabilmente questa, più che l’autonomia assoluta, la direzione interessante per molti sistemi AI.
Quando l’AI può iniziare a controllare il proprio lavoro
Qui possiamo tornare al concetto di “autocontrollo”.
Usarlo non significa dire che Claude abbia sviluppato coscienza o consapevolezza di sé.
Non abbiamo elementi per affermarlo.
Possiamo però parlare di qualcosa di più concreto: la capacità di utilizzare un meccanismo esterno e formale per verificare i propri risultati e modificare il percorso quando questi non vengono accettati dal sistema di controllo.
Anthropic osserva che la formalizzazione sembra aiutare Claude anche nel lavoro matematico originale: alcune prove parziali possono essere utilizzate come una forma di controllo indipendente delle ipotesi, analogamente a come un ricercatore può utilizzare una simulazione numerica per verificare se una certa direzione sembra plausibile.
Questo non è autocoscienza.
È qualcosa di più limitato, ma anche molto più concreto: un ciclo di produzione e verifica incorporato nel processo di ragionamento.
Ed è un concetto che può avere implicazioni ben oltre la matematica.
Dalla matematica alla ricerca scientifica
La matematica è un caso particolarmente favorevole perché dispone di sistemi formali.
Molte altre forme di conoscenza non hanno la stessa caratteristica.
In matematica possiamo arrivare, almeno idealmente, a una situazione in cui una dimostrazione viene accettata o rifiutata sulla base di regole formali.
Nella ricerca scientifica il problema è più complesso.
Un’ipotesi può essere plausibile, ma non esiste necessariamente un sistema formale capace di stabilire automaticamente se sia vera.
Servono esperimenti, osservazioni, dati, simulazioni, confronto con la letteratura e valutazione umana.
L’AI può quindi contribuire a formulare ipotesi e ad analizzare risultati, ma il meccanismo di verifica dipende dal campo.
Ed è proprio questo che rende interessante il caso Fermat.
Non dimostra che l’AI sia diventata capace di verificare qualsiasi cosa.
Dimostra invece che quando riusciamo a costruire un ambiente formale adeguato, possiamo trasformare una parte del controllo del lavoro dell’AI in un processo automatico.
E se lo stesso principio arrivasse nel business?
La domanda successiva riguarda naturalmente le applicazioni pratiche.
Pensiamo a un agente AI che deve eseguire un processo aziendale.
Un agente potrebbe, per esempio, leggere una richiesta, recuperare informazioni da sistemi diversi, elaborare una decisione e proporre o eseguire un’azione.
Il problema non è soltanto fare bene ogni singolo passaggio.
È poter verificare che l’intero processo abbia rispettato determinate regole.
Quali dati poteva utilizzare?
Quali strumenti poteva chiamare?
Quali azioni era autorizzato a eseguire?
Quali condizioni dovevano essere rispettate prima di procedere?
Quale risultato doveva essere prodotto?
In un sistema di questo tipo, un meccanismo di verifica formalizzato potrebbe diventare una sorta di arbitro del processo.
Non stabilirebbe necessariamente se la decisione è “giusta” in senso assoluto.
Potrebbe però stabilire se rispetta le regole definite per quel processo.
È una differenza fondamentale.
Il vero limite: non tutto può essere formalizzato
Ed è qui che arriviamo al limite più interessante.
La matematica permette un livello di formalizzazione che non possiamo semplicemente trasferire a ogni ambito della conoscenza.
Non tutto può essere espresso attraverso regole rigorose e verificabili automaticamente.
Una decisione strategica, una valutazione creativa, una relazione con un cliente, una scelta manageriale o un giudizio etico possono dipendere da contesto, esperienza e interpretazione.
In questi casi non esiste necessariamente un equivalente di Lean che possa dire alla macchina: “questa risposta è matematicamente corretta”.
Il problema quindi non scompare.
Si sposta.
La sfida diventa capire quali parti di un processo possono essere formalizzate, quali possono essere sottoposte a controlli automatici e quali devono invece continuare a prevedere un giudizio umano.
Ed è probabilmente proprio questa combinazione a rendere più affidabili i sistemi agentici.
Non una macchina cosciente, ma una macchina con criteri di controllo
La tentazione, davanti a risultati come quello di Fermat, è parlare di AI che “ragiona”, “capisce” o addirittura “diventa consapevole”.
Sono formule affascinanti, ma rischiano di portarci troppo avanti rispetto a ciò che possiamo realmente dimostrare.
Il risultato di Anthropic è interessante proprio senza bisogno di attribuire alla macchina una coscienza.
Per la prima volta abbiamo un esempio particolarmente evidente di un LLM che lavora per un periodo prolungato all’interno di un ambiente strutturato, produce una quantità enorme di formalizzazione, utilizza agenti collaborativi e soprattutto dispone di un meccanismo rigoroso che gli permette di sapere se ciò che sta costruendo soddisfa i requisiti formali del problema.
È un passo importante.
Non verso una macchina necessariamente “cosciente”, ma verso sistemi AI più capaci di controllare e verificare il proprio lavoro.
E questa potrebbe essere una delle condizioni necessarie per passare da AI che generano contenuti a sistemi AI che possono partecipare in modo più affidabile a processi complessi.
Il vero salto, forse, non sarà quando l’AI saprà fare sempre più cose.
Sarà quando sapremo darle criteri affidabili per capire quando ciò che ha fatto è accettabile, quando non lo è e cosa deve fare per correggersi.
Il caso Fermat ci mostra che, almeno in alcuni domini, questo futuro non è più soltanto teorico.