Lean convalida la prova di Fermat di Claude

Lean, il software di verifica delle dimostrazioni utilizzato dai matematici di tutto il mondo, ha accettato una versione formale completa dell’ultimo teorema di Fermat. La formalizzazione, realizzata dal sistema Claude di Anthropic e pubblicata in un repository aperto, non contiene passaggi provvisori irrisolti, assiomi aggiuntivi né scorciatoie computazionali estranee ai fondamenti standard di Lean (repository). Kevin Buzzard, matematico dell’Imperial College London che guidava un proprio progetto di formalizzazione, ha compilato autonomamente il codice e confermato che la verifica va a buon fine, definendo il risultato «uno straordinario traguardo di autoformalizzazione» (Buzzard).

La questione matematica era risolta da tempo: Andrew Wiles dimostrò il teorema nel 1995 e nessun matematico serio ne metteva in dubbio la validità. Restava però da riscrivere la dimostrazione sotto forma di istruzioni per un verificatore letterale, esplicitando ogni definizione e ogni passaggio intermedio che l’autore originale poteva lasciare sottinteso. Anthropic sostiene che decine di agenti di intelligenza artificiale abbiano completato questa trasposizione in undici giorni nell’agosto scorso, lavorando in parallelo attraverso una piattaforma chiamata Prove2Me (Anthropic).

Quegli undici giorni descrivono tuttavia un processo che soggetti esterni non possono riprodurre, poiché il modello interno, l’infrastruttura di orchestrazione, le decisioni degli operatori e le risorse di calcolo impiegate non fanno parte del materiale pubblicato. È invece riproducibile il risultato finale: chiunque disponga di hardware sufficiente può ricompilare il progetto Lean e verificare che la dimostrazione superi i controlli. Un secondo verificatore, scritto in Rust da Anthropic, ha esaminato lo stesso artefatto formale e confermato la coerenza di tutte le 1.052.234 dichiarazioni (technical report); si tratta però di una seconda lettura del medesimo testo, non di una ricostruzione indipendente della campagna durata undici giorni.

Come hanno lavorato gli agenti

Formalizzare una dimostrazione significa riscrivere l’argomentazione di un matematico affinché un programma privo di intuizione matematica possa controllarne ogni passaggio logico. L’enunciato è ingannevolmente semplice: per qualsiasi esponente intero pari o superiore a tre, non esistono tre interi positivi che soddisfino aⁿ + bⁿ = cⁿ; la dimostrazione, invece, attraversa strati profondi della teoria dei numeri e si sviluppa lungo centinaia di pagine.

Claude non ha scoperto nuova matematica, ma ha formalizzato la catena già nota di risultati che conduce alla dimostrazione di Wiles, seguendo una trattazione dei matematici Henri Darmon, Fred Diamond e Richard Taylor (Anthropic, technical report). L’intuizione creativa apparteneva a Wiles e ai suoi predecessori; il contributo di Claude è consistito nel tradurla in circa 10,5 milioni di righe di codice verificabile da una macchina (technical report).

La piattaforma Prove2Me, progettata dal ricercatore di Anthropic Tianyi Peng insieme a collaboratori della Columbia University, ha scomposto la dimostrazione in un grafo di dipendenze formato da circa 29.511 proposizioni autonome (technical report). Gli agenti sceglievano le proposizioni pronte per essere affrontate, ne scrivevano le dimostrazioni in Lean e controllavano a vicenda gli enunciati proposti, procedendo in parallelo; nel complesso, la campagna ha consumato circa sei miliardi di token in uscita generati da un modello di ricerca interno (technical report).

Secondo Anthropic, durante l’esecuzione gli operatori umani non hanno scritto codice Lean, sebbene abbiano scelto il teorema, fornito il percorso dimostrativo già noto, progettato l’infrastruttura degli agenti e, in alcune occasioni, modificato le priorità (Anthropic). L’azienda non ha pubblicato né la trascrizione completa degli interventi degli operatori né i costi di calcolo.

Il risultato poggia su anni di lavoro umano

Il progetto si è appoggiato a Mathlib, la vasta libreria di matematica formalizzata mantenuta dalla comunità, utilizzando inoltre materiale proveniente da due iniziative precedenti. Dalla fine del 2023 il gruppo di Buzzard all’Imperial lavorava a una formalizzazione in Lean dell’ultimo teorema di Fermat, sostenuta da un finanziamento EPSRC di un milione di sterline previsto fino al 2029 (EPSRC award); un altro progetto comunitario aveva già formalizzato il teorema per un sottoinsieme di casi. Il file delle attribuzioni di Anthropic segnala 106 file contenenti materiale ripreso o adattato da questi lavori (attribution).

L’esecuzione in parallelo rende gli undici giorni di calendario incomparabili con le ore di lavoro umano investite dal gruppo di Buzzard, che all’inizio della campagna di Claude operava con finanziamenti da circa 22 mesi (EPSRC award). Anthropic non ha comunicato né le ore di utilizzo delle GPU né il consumo energetico.

Prima di questa pubblicazione, l’ultimo teorema di Fermat era l’unica voce ancora incompleta nell’elenco di Freek Wiedijk dei cento teoremi importanti da formalizzare, un parametro di riferimento che da vent’anni misura i progressi del settore (Buzzard).

La prova più severa della possibilità di generalizzare questo risultato sarà la formalizzazione di matematica recente e meno documentata, per la quale non esistano un percorso già tracciato, librerie mature o precedenti lavori formali. In questo caso gli agenti si sono misurati con un teorema celebre, sostenuti da un’infrastruttura già consistente: hanno così dimostrato di poter produrre, quando dispongono di una strategia nota e di formalizzazioni precedenti, una versione completa che Lean accetta e che soggetti esterni possono verificare. Il processo che l’ha generata, sulla base dei materiali pubblicati, rimane invece irriproducibile.