Una dimostrazione che ha richiesto a un matematico sette anni per essere costruita, e a un altro ricercatore una proiezione di cinque anni per essere formalizzata, è stata ora completata da un team di agenti di IA in undici giorni. Il modello Claude di Anthropic ha prodotto una versione formale dell’Ultimo Teorema di Fermat, uno dei problemi più celebri nella storia della matematica. Questa non è una nuova dimostrazione. È qualcosa che probabilmente è ancora più utile: una conferma leggibile e verificata dalla macchina che la dimostrazione umana è corretta, costruita da zero in un linguaggio di programmazione chiamato Lean.
Un Problema di 350 Anni, e Cosa Significa Veramente “Formalizzare”
L’Ultimo Teorema di Fermat afferma che nessun numero intero a, b e c può soddisfare l’equazione aⁿ + bⁿ = cⁿ quando n è un numero intero maggiore di 2. Pierre de Fermat ha proposto l’enigma nel diciassettesimo secolo, annotando famosamente nel margine di un libro di testo di aver trovato una dimostrazione ma di non avere abbastanza spazio per scriverla. Quella nota ha perseguitato la matematica per circa tre secoli e mezzo.
Andrew Wiles ha finalmente dimostrato il teorema nel 1995, dopo aver lavorato al problema in segreto per sette anni. La sua dimostrazione non è stata priva di difficoltà: è stata scoperta una falla, e ci è voluto circa un anno affinché Wiles e il suo collaboratore Richard Taylor la sistemassero. L’episodio illustra una vulnerabilità strutturale nelle dimostrazioni matematiche tradizionali. Sono scritte in linguaggio naturale e notazione logica, controllate da esperti umani e vulnerabili a errori che possono nascondersi all’interno di lunghe catene di ragionamento.
La formalizzazione affronta questa vulnerabilità direttamente. Significa tradurre una dimostrazione in codice informatico, nello specifico in un linguaggio formale che una macchina può verificare passo dopo passo. Non c’è ambiguità nel codice. O la logica regge oppure no. Un archivio centrale chiamato Mathlib memorizza già circa 2 milioni di linee di matematica formalizzata. La nuova dimostrazione di Anthropic aggiunge 13 milioni di linee a quel panorama, coprendo circa 29.500 teoremi intermedi che erano necessari per raggiungere il risultato finale. Questo la rende più di cinque volte più grande di tutti i precedenti contenuti di Mathlib combinati, e la più grande dimostrazione in Lean mai scritta.
Come Hanno Lavorato Davvero gli Agenti (e Dove Hanno Avuto Difficoltà)
Il sistema di Anthropic non ha usato un singolo modello di IA che lavorava in isolamento. Più agenti separati sono stati impiegati, ciascuno assegnato a diverse porzioni del problema, affrontando parti più piccole del teorema in parallelo. Il processo è girato ininterrottamente e autonomamente per undici giorni.
Gli esperti umani non sono stati assenti. Hanno fornito quelle che Anthropic descrive come “istruzioni di alto livello” per mantenere il lavoro sulla buona strada. Vale la pena notare questo: gli agenti periodicamente perdevano di vista lo stato generale del progetto e smettevano di collaborare efficacemente. Il sistema ha richiesto una guida esterna per riprendersi da quei blocchi. Ciò che alla fine ha aiutato è stato uno strumento originariamente progettato per la collaborazione matematica umana, chiamato Prove2Me. Una volta che gli agenti hanno iniziato a usarlo per tracciare il loro lavoro e coordinarsi sui prossimi passi, il progetto è andato avanti in modo più affidabile.
Kevin Buzzard, un matematico dell’Imperial College di Londra che aveva guidato un progetto quinquennale per formalizzare la stessa dimostrazione di Wiles e Taylor, ha commentato il risultato. Ha fatto notar che la dimostrazione poggia su “nessun’altra assunzione se non gli assiomi della matematica”, e ha descritto il lavoro come multi-strato, toccando l’algebra, l’analisi armonica, la geometria e la teoria dei numeri. La sua valutazione è significativa: Buzzard non era uno spettatore. Aveva organizzato una conferenza a Londra all’inizio di quest’anno riunendo esperti di IA, informatici e matematici per lavorare esattamente su questo problema. L’annuncio di Anthropic ha superato del tutto quell’sforzo.
Perché Questo È Importante al Di Là del Teorema Stesso
Ecco cosa la maggior parte della copertura di questa storia si perde. Il teorema in sé non è il punto. L’Ultimo Teorema di Fermat era già stato dimostrato. Ciò che Anthropic ha dimostrato riguarda qualcosa sulla natura della conoscenza matematica e su come può essere verificata, estesa e ampliata.
Buzzard lo ha detto direttamente: se l’IA può ora auto-formalizzare una dimostrazione di questa complessità, allora la formalizzazione automatica della più ampia letteratura matematica moderna diventa un obiettivo realistico a breve termine. Questo è un cambiamento significativo. La matematica è il fondamento della fisica, della crittografia, dell’informatica e dell’ingegneria. Un corpus formalizzato e verificabile da una macchina di conoscenza matematica permetterebbe ai ricercatori di costruire su risultati precedenti con molta più fiducia, catturando errori che la revisione umana potrebbe mancare e accelerando il ritmo con cui nuovi risultati possono essere stabiliti.
L’episodio illustra anche qualcosa di importante su come i sistemi di IA operano attualmente nel lavoro intellettuale ad alto rischio. Non sono autonomi nel modo in cui la parola viene talvolta usata liberamente. Richiedevano supervisione umana, si bloccavano durante il coordinamento e avevano bisogno di strumenti progettati per la collaborazione umana per funzionare efficacemente. La tempistica di undici giorni è notevole. Il bisogno di guida umana per tutto il tempo è altrettanto istruttivo.
L’IA qui non sta sostituendo i matematici. Sta gestendo un volume e una granularità di verifica logica che nessun team umano potrebbe sostenere a questa scala, liberando i ricercatori per concentrarsi sulle domande di livello superiore su cosa dimostrare e perché è importante.
In Breve
Gli agenti di IA di Anthropic hanno prodotto la più grande dimostrazione formale mai scritta, verificando l’Ultimo Teorema di Fermat in codice Lean leggibile dalla macchina attraverso 13 milioni di linee e 29.500 passaggi intermedi. Il risultato conta meno come scoperta matematica e più come dimostrazione che l’IA può ora formalizzare dimostrazioni complesse e stratificate a una scala e a una velocità precedentemente fuori portata. Il processo ha richiesto una guida umana e si è bloccato più di una volta. Quel contesto appartiene alla storia anch’esso.
Basato su un articolo di New Scientist.