Claude formalizza l’ultimo teorema di Fermat: la prima dimostrazione verificata dal computer

Per oltre tre secoli l’ultimo teorema di Fermat è stato il simbolo delle domande matematiche che sembrano semplici da enunciare ma resistono a ogni tentativo di risposta. Ora Anthropic ha annunciato un risultato che segna un passaggio storico: la prima dimostrazione completa del teorema interamente verificata da un computer. A produrla è stato Claude, che ha lavorato in larga autonomia per undici giorni scrivendo la prova nel linguaggio Lean.

Attenzione però a non fraintendere la portata dell’annuncio. Claude non ha scoperto una nuova dimostrazione del teorema, ma ha tradotto in una forma verificabile dalla macchina la dimostrazione già esistente, quella firmata da Andrew Wiles negli anni Novanta. La novità, e non è poca cosa, sta tutta nella verifica.

Cosa ha fatto davvero Claude con l’ultimo teorema di Fermat

Quando si parla di dimostrazione formalizzata si intende una cosa precisa. Una prova scritta per essere letta dagli esseri umani salta un’enorme quantità di passaggi considerati ovvi e si appoggia a secoli di risultati già pubblicati e dati per acquisiti. Un assistente di dimostrazione come Lean, invece, non concede nulla: ogni singolo passo, anche il più banale, deve essere reso esplicito e controllato dalla logica del programma.

È qui che nasce la difficoltà. Riscrivere una prova complessa in un linguaggio come Lean significa ricostruire da zero gran parte dell’impalcatura matematica su cui poggia, perché solo una frazione minima della matematica è stata finora formalizzata. Per l’ultimo teorema di Fermat si stimava servissero anni di lavoro.

Claude ha completato tutto in undici giorni.

Il modello ha prodotto prove verificabili dal computer di 30.300 teoremi intermedi, 29.500 dei quali utilizzati nella dimostrazione finale, arrivando a scrivere circa 13 milioni di righe di codice Lean. Per darti un’idea della scala, si tratta di una mole oltre cinque volte più grande di Mathlib, la principale libreria di dimostrazioni matematiche costruita dalla comunità su cui lo stesso teorema si appoggia.

Non è un dettaglio marginale: quella appena prodotta è la più grande dimostrazione in Lean mai costruita.

Vale la pena chiarire la differenza rispetto ad altri lavori recenti. Quando un modello contribuisce a un risultato inedito, come è accaduto con alcune ricerche sull’ipotesi di Riemann, la novità sta nella matematica prodotta. Qui invece la matematica c’era già: quello che mancava era la certezza assoluta, riga per riga, che ogni passaggio fosse corretto. Ed è proprio questa certezza che una verifica automatica riesce a garantire.

Non è la prima volta che l’intelligenza artificiale entra nel territorio della matematica formale. Nei mesi scorsi OpenAI aveva mostrato il suo modello Astra mentre affrontava dieci problemi aperti pubblicando le soluzioni in Lean, mentre Mistral aveva rilasciato Leanstral 1.5, un modello aperto pensato proprio per la verifica formale. La differenza, questa volta, sta nella scala e nella completezza del risultato.

Perché questo teorema ha resistito per oltre 350 anni

La storia dell’ultimo teorema di Fermat è una delle più affascinanti della matematica. Intorno al 1637 Pierre de Fermat annotò a margine della sua copia dell’Arithmetica di Diofanto un’affermazione tanto semplice quanto sfuggente: non esistono numeri interi positivi a, b, c che soddisfino l’equazione aⁿ + bⁿ = cⁿ per un qualsiasi esponente n maggiore di due.

Accanto alla formula, Fermat lasciò la nota diventata leggendaria: sosteneva di avere una dimostrazione davvero notevole, ma che il margine era troppo stretto per contenerla.

Quella dimostrazione non fu mai trovata. Per più di trecentocinquant’anni generazioni di matematici ci provarono senza riuscirci. Nel 1908 fu perfino istituito un premio da 100.000 marchi d’oro tedeschi per chi avesse chiuso la questione, e nel solo primo anno arrivarono 621 tentativi errati.

La svolta arrivò con Andrew Wiles. Il matematico britannico presentò la sua prova nel giugno del 1993, ma durante la verifica emerse una lacuna critica. Wiles passò un anno a colmarla, prima da solo e poi con il suo ex studente Richard Taylor, fino a pubblicare la versione corretta nel 1995: 129 pagine che richiesero mesi di controlli.

Proprio quella fatica di verifica è il cuore del problema che Anthropic ha voluto affrontare.

Prove2Me e le decine di agenti al lavoro in parallelo

Il progetto nasce da Tianyi Peng, ricercatore di Anthropic il cui gruppo alla Columbia University sviluppa strumenti per la formalizzazione assistita dall’AI. Peng voleva semplicemente capire se Claude potesse fare progressi sulla formalizzazione del teorema, e il risultato è andato ben oltre le sue aspettative.

I primi tentativi, va detto, fallirono. Gli agenti ottenevano qualche successo iniziale, poi perdevano il filo dello stato del progetto e smettevano di collaborare in modo efficace. Quelle prove andate a vuoto hanno comunque lasciato un segno, contribuendo a circa il 7% delle righe non standard della dimostrazione finale.

La vera svolta è arrivata con Prove2Me, una piattaforma collaborativa aperta per la formalizzazione della matematica progettata dallo stesso Peng insieme ai suoi collaboratori della Columbia. Il suo compito è coordinare il lavoro di decine di agenti Claude in parallelo, evitando che finiscano per ostacolarsi a vicenda.

Il meccanismo ruota attorno a un grafo diretto aciclico dei teoremi da dimostrare, una mappa che indica a ciascun agente quali risultati affrontare per primi e come incastrarli tra loro. Questa struttura ha ridotto il degrado della memoria dei modelli e ha permesso di distribuire il carico, mentre la separazione tra enunciati e dimostrazioni in file distinti accelerava la compilazione di Lean e ne riduceva il consumo di risorse.

Sul piano delle risorse l’impresa è stata imponente ma non irraggiungibile. Il sistema, costruito su un’impalcatura multi-agente basata su Claude Code, ha consumato circa sei miliardi di token in output usando un modello di ricerca interno paragonabile a Claude Fable 5.1. L’apporto umano si è limitato a rare indicazioni di alto livello da parte di Peng, come segnalare quale teorema affrontare con priorità.

Il controllo finale, in ogni caso, spetta alla macchina. La prova è stata validata da Lean usando soltanto i tre assiomi standard del sistema, e un apposito comparatore ha confermato che l’enunciato dimostrato coincide con quello dell’ultimo teorema di Fermat registrato in Mathlib.

Cosa cambia per la matematica e per l’intelligenza artificiale

La velocità con cui è stato raggiunto questo obiettivo racconta qualcosa di più grande del teorema in sé. Se formalizzare una prova complessa come quella di Fermat è oggi possibile in meno di due settimane, allora diventa realistico pensare di verificare automaticamente ampie porzioni della matematica esistente.

Kevin Buzzard, il matematico dell’Imperial College London che dal 2024 guida lo sforzo comunitario per formalizzare il teorema in Lean, ha esaminato il risultato e ha parlato di «un’impresa di autoformalizzazione straordinaria». Secondo lui questo apre la strada alla formalizzazione automatica della letteratura matematica moderna, con la possibilità di scovare errori nel corpus esistente e di alleggerire il carico di lavoro dei revisori.

C’è poi un aspetto che ti riguarda da vicino se segui l’evoluzione dei modelli. Man mano che l’AI produce sempre più dimostrazioni, serve un modo affidabile per controllarle senza affidarsi ogni volta a mesi di lavoro umano. La formalizzazione automatica può diventare esattamente questo: un filtro capace di certificare la correttezza dei risultati generati dalle macchine.

Anthropic mette in evidenza anche un punto interessante sull’accessibilità. In un esperimento parallelo, tre ricercatori hanno formalizzato il teorema dei tre primi di Vinogradov in appena tre giorni usando tre normali abbonamenti Claude Max. Un segnale che questo tipo di collaborazione non richiede per forza risorse fuori portata.

Un tassello verso una matematica più affidabile

La dimostrazione completa è disponibile pubblicamente su GitHub, insieme a una guida che ne ripercorre i passaggi principali. Puoi trovare metodo e risultati descritti in dettaglio nell’annuncio ufficiale di Anthropic.

Resta un punto fermo, che gli stessi ricercatori tengono a ribadire: una prova formalizzata non sostituisce la spiegazione pensata per gli esseri umani, ma la affianca. Serve a dare fiducia, non a togliere significato al lavoro del matematico.

Se ti interessa capire dove sta andando il rapporto tra intelligenza artificiale e ricerca scientifica, questo è uno dei segnali più netti degli ultimi mesi. Continua a seguirci per restare aggiornato sulle prossime tappe di una trasformazione che è appena cominciata.