The Pulse
Claude trasforma la dimostrazione di Wiles dell’Ultimo teorema di Fermat in 13 milioni di righe di Lean
Secondo Anthropic, Claude ha prodotto in 11 giorni la prima formalizzazione completa dell’Ultimo teorema di Fermat verificata al computer. Il sistema ha generato 13 milioni di righe di codice Lean e dimostrato 30.300 teoremi intermedi, trad
AI.info Team ·
13 milioni di righe di codice Lean separano ora uno dei teoremi più famosi della matematica dall’approvazione definitiva di un computer. Anthropic afferma che Claude ha prodotto in 11 giorni la prima formalizzazione completa, dall’inizio alla fine e verificata al computer, dell’Ultimo teorema di Fermat, trasformando la celebre dimostrazione di Andrew Wiles in un artefatto leggibile da una macchina, che Lean può esaminare un passaggio logico alla volta.
Claude non ha scoperto una nuova dimostrazione del teorema. Wiles, lavorando con Richard Taylor, dimostrò l’Ultimo teorema di Fermat negli anni 1990, dopo oltre tre secoli di tentativi falliti. Il risultato di Anthropic è diverso: i suoi ricercatori hanno usato una rete di agenti Claude per tradurre in Lean la dimostrazione esistente, colmare migliaia di dettagli omessi e produrre una versione che un assistente alla dimostrazione potesse verificare senza affidarsi al giudizio di un revisore umano.
Il risultato è enorme. Nel corso del progetto Claude ha dimostrato 30.300 teoremi intermedi, 29.500 dei quali compaiono nella dimostrazione finale. Il codice completo è oltre cinque volte più grande di Mathlib, la principale libreria comunitaria di matematica formalizzata su cui si basa il lavoro.
Undici giorni per ricostruire una dimostrazione di 129 pagine
L’Ultimo teorema di Fermat afferma che non esistono interi positivi a, b e c che soddisfino an + bn = cn quando n è maggiore di 2. Pierre de Fermat annotò l’affermazione intorno al 1637 sul margine di una copia dell’Arithmetica di Diofanto, aggiungendo di aver trovato una «dimostrazione davvero meravigliosa» che il margine non poteva contenere.
La presunta dimostrazione di Fermat non venne mai alla luce. Wiles presentò una dimostrazione in una serie di lezioni nel giugno 1993, ma durante la verifica i matematici vi trovarono una lacuna. Trascorse un altro anno a correggere la dimostrazione insieme a Taylor, prima di pubblicare il risultato corretto nel maggio 1995. La dimostrazione pubblicata occupava 129 pagine e si basava su concetti avanzati di geometria algebrica, teoria dei numeri e teoria delle curve ellittiche.
I matematici possono leggere una dimostrazione del genere, completare i passaggi di routine e confrontarne le affermazioni con risultati consolidati. Un assistente alla dimostrazione non può farlo. Lean richiede che ogni definizione, inferenza e dipendenza sia espressa in un linguaggio formale verificabile dal suo kernel. Una frase che un matematico considera ovvia può richiedere un teorema a sé, un oggetto con un tipo definito con precisione o diversi livelli di codice di supporto.
Secondo Anthropic, la comunità matematica in generale si aspettava che una formalizzazione completa dell’Ultimo teorema di Fermat richiedesse anni. Kevin Buzzard, matematico dell’Imperial College London che ha guidato un importante progetto comunitario per formalizzare il teorema, ha esaminato il repository dopo che Claude ha completato il lavoro.
«Questo straordinario risultato di formalizzazione automatica, che secondo i ricercatori di Anthropic ha richiesto soltanto 11 giorni, dimostra l’Ultimo teorema di Fermat senza altre assunzioni oltre agli assiomi della matematica. Lungo il percorso vediamo la formalizzazione automatica di algebra, analisi armonica, geometria e teoria dei numeri, e scopriamo che gli artefatti prodotti dalla formalizzazione automatica con l’IA sono ormai abbastanza solidi da poter essere usati come base per altri lavori; la dimostrazione si articola su più livelli.»
Kevin Buzzard, matematico, Imperial College London
La valutazione di Buzzard riguarda la verifica formale, non la scoperta di nuova matematica. Claude segue una versione semplificata della dimostrazione sviluppata da Henri Darmon, Fred Diamond e Richard Taylor, attingendo anche a precedenti progetti Lean scritti da esseri umani nell’ambito del progetto di formalizzazione dell’Imperial College e del progetto separato flt-regular.
Claude aveva bisogno di una mappa condivisa della dimostrazione
I primi tentativi fallirono per una ragione pratica: gli agenti perdevano il filo di ciò che era già stato definito, di quali enunciati dipendessero gli uni dagli altri e di quali parti del teorema restassero da dimostrare. Secondo Anthropic, quei tentativi falliti hanno contribuito a circa il 7% delle righe del risultato finale che non erano codice ripetitivo o predefinito, ma la lezione più importante è venuta dal problema di coordinamento.
Il tentativo riuscito ha usato Prove2Me, una piattaforma collaborativa aperta sviluppata da Tianyi Peng e collaboratori della Columbia University. Il sistema manteneva un grafo diretto aciclico degli enunciati dei teoremi, permettendo agli agenti di individuare le dipendenze ancora da risolvere e scegliere nuovi obiettivi senza dover ricostruire ripetutamente lo stato del progetto.
Prove2Me separava inoltre gli enunciati dei teoremi dalle rispettive dimostrazioni. Questa organizzazione consentiva agli agenti di compilare unità più piccole, lavorare in parallelo e riutilizzare risultati già stabiliti senza dover caricare in memoria l’intero progetto per ogni compito. Descrizioni in linguaggio naturale associate agli enunciati offrivano agli agenti un altro modo per cercare risultati pertinenti e scegliere un percorso più breve nella dimostrazione.
Decine di agenti Claude hanno lavorato su parti distinte della formalizzazione. Alcuni definivano oggetti matematici, altri dimostravano lemmi intermedi e altri ancora usavano quei lemmi per affrontare enunciati via via più difficili. Secondo Anthropic, il lavoro ha consumato circa sei miliardi di token di output di un modello di ricerca interno paragonabile al suo sistema Claude Fable 5.1.
Il coinvolgimento umano è rimasto limitato, ma importante. Peng ha fornito occasionalmente indicazioni generali, tra cui istruzioni come «Il Jacobiano come schema sembra una priorità alta» e «portate a termine presto [il] teorema di Mazur». Quei prompt non sostituivano i singoli passaggi della dimostrazione. Aiutavano a decidere quale ramo del grafo delle dipendenze meritasse attenzione per primo.
Lean ha verificato l’enunciato, non la descrizione che lo accompagna
Il repository pubblico definisce l’Ultimo teorema di Fermat per i numeri naturali e include un obiettivo di compilazione finale che verifica le dipendenze del teorema. La verifica fallisce se la dimostrazione si basa su un assioma aggiuntivo, su un segnaposto non completato come sorry o su diverse forme di calcolo non verificato. Secondo Anthropic, il teorema completato poggia sui tre assiomi standard di Lean: estensionalità proposizionale, correttezza dei quozienti e assioma della scelta classico.
I ricercatori hanno anche sottoposto il codice allo strumento comparator di Lean. Comparator ha verificato che il teorema dimostrato nel repository corrispondesse all’enunciato dell’Ultimo teorema di Fermat presente in Mathlib e ha ripercorso la dimostrazione attraverso il kernel di Lean. Un secondo verificatore, nanoda, ha accettato indipendentemente un’esportazione dello stesso ambiente dopo aver elaborato oltre 1 milione di dichiarazioni senza errori.
Il repository documenta la portata dello sforzo di verifica. Per compilare il progetto completo è stato necessario compilare tutti i 60.475 moduli. Nella prova riportata da Anthropic, il controllo con comparator ha richiesto circa 14 ore e 46 minuti, mentre la compilazione completa ha richiesto 5 ore e 32 minuti usando 96 processi paralleli. Il progetto ha richiesto risorse hardware considerevoli: Anthropic riporta un utilizzo massimo di memoria di 153 gigabyte per la compilazione e di 230 gigabyte per comparator.
Questi controlli stabiliscono che l’enunciato formale discende dai fondamenti ammessi, a condizione che gli utenti si fidino del kernel di Lean, del verificatore indipendente e del software e dell’hardware circostanti. Non stabiliscono che il nome di ogni teorema descriva accuratamente il contenuto matematico che un lettore umano potrebbe aspettarsi. Il repository di Anthropic precisa che i nomi e le etichette generati sono pensati per le macchine e che è l’enunciato formale, non il suo nome, a determinare ciò che è stato dimostrato.
La distinzione è importante. La verifica formale può mostrare che una catena di definizioni e deduzioni dotate di tipo è internamente valida. Non può dire al lettore se un teorema intermedio esprime l’idea matematica prevista, se l’esposizione è comprensibile o se una dimostrazione breve ed elegante è stata sepolta sotto strati di codice generato.
Il risultato è una verifica, non una scoperta matematica
Anthropic traccia un netto contrasto con recenti lavori sull’ipotesi di Riemann condotti con l’IA, nei quali i ricercatori hanno presentato sistemi capaci di generare nuovo materiale matematico. L’Ultimo teorema di Fermat era già stato dimostrato da Wiles. Il contributo di Claude è stato formalizzare la dimostrazione esistente con un livello di dettaglio verificabile da un computer.
La formalizzazione offre da tempo una seconda via per acquisire fiducia nei risultati matematici difficili. La dimostrazione della congettura di Keplero di Thomas Hales rimase per anni in fase di revisione prima che un grande gruppo creasse il progetto Flyspeck per verificarla. Il lavoro di Grigori Perelman sulla congettura di Poincaré richiese diverse lunghe esposizioni prima che i matematici ne accettassero i dettagli. La revisione umana resta essenziale per comprendere quei risultati, ma è lenta e può lasciarsi sfuggire delle lacune.
Il progetto di Claude su Fermat rende più evidente questa tensione. Un computer può elaborare milioni di dichiarazioni senza stancarsi, eppure il risultato è troppo grande perché un matematico possa leggerlo come una dimostrazione convenzionale. Il sistema rende la verifica formale più rapida sotto un certo aspetto, ma crea una nuova esigenza di strumenti che spieghino ciò che la macchina ha verificato.
Secondo Anthropic, il progetto potrebbe rendere praticabile la produzione di una formalizzazione di accompagnamento per i futuri articoli di matematica, soprattutto quelli che contengono dimostrazioni lunghe o ampie componenti computazionali. Una dimostrazione formale non sostituirebbe un’esposizione leggibile dalle persone. Fornirebbe un oggetto separato che i ricercatori potrebbero compilare, esaminare e rieseguire nel valutare le affermazioni.
I ricercatori dovranno comunque decidere quanto del processo possa essere automatizzato senza indebolire la comprensione matematica. Lo stesso repository su Fermat avverte che il codice formalizzato è scritto per essere verificato, non per essere letto. Questa limitazione non è un difetto di Lean: riflette la differenza tra una dimostrazione pensata per la comprensione umana e una pensata per un verificatore deterministico.
Una nuova prova per la matematica generata dall’IA
L’esperimento di Anthropic cambia anche l’unità di misura della matematica prodotta dall’IA. Il dato principale non è un teorema scoperto da Claude, ma una grande quantità di codice che ha superato diverse forme di verifica meccanica. La domanda pertinente diventa se un sistema di IA sia in grado di portare avanti un lungo progetto formale, mantenere le dipendenze attraverso migliaia di compiti e riprendersi dai tentativi falliti.
In questa prova, l’architettura del sistema è stata importante quanto il modello. Prove2Me ha fornito uno stato condiviso, il grafo dei teoremi ha fornito il piano di lavoro e Lean è stato l’arbitro finale. Senza questi elementi, secondo Anthropic, i primi agenti perdevano ripetutamente il filo del progetto.
La formalizzazione completata da Claude è ora disponibile nel repository pubblico di Anthropic su GitHub, insieme ai sorgenti Lean, agli script di verifica e a una versione della dimostrazione consultabile tramite browser. Il repository contiene pagine per circa 29.511 teoremi e 1.450 moduli di definizioni, offrendo ai ricercatori un modo per seguire la catena formale delle dipendenze anziché considerare i 13 milioni di righe come un blocco opaco.
Il teorema di Fermat entra dunque nell’era delle macchine in una forma insolita: la matematica ha quasi 400 anni, la dimostrazione di Wiles ha più di 30 anni e il nuovo artefatto è una vasta ricostruzione verificata al computer. Il suo risultato più concreto non è una nuova risposta alla domanda di Fermat. È un progetto Lean pubblico che un computer può compilare, rieseguire e respingere se un qualsiasi passaggio formale non supera la verifica.