Claude ha chiuso Fermat in 11 giorni: 13,4 milioni di righe di Lean e nemmeno un “ovviamente”

Il 4 settembre, Anthropic ha mostrato il primo test completo su macchina dell'Ultimo Teorema di Fermat. Claude in 11 giorni, quasi senza l'aiuto di persone, ha tradotto nella lingua la dimostrazione di Andrew Wiles Lean: 13,4 milioni di righe di codice, circa 30mila teoremi intermedi, zero “ovvi da quanto detto”. Il progetto, che i matematici pianificavano da anni - solo il disegno della prima fase di Kevin Buzzard dell'Imperial College di Londra era lungo 86 pagine - è stato completato in una settimana e mezza.

Chiariamo subito cosa qui non c'è: non ci sono nuove prove. Il modello non ha trovato un proprio percorso verso il teorema. Ha fatto qualcosa di diverso e, francamente, non meno complesso: ha preso una prova umana, dove su ogni pagina ci sono disclaimer come "questo segue banalmente", e l'ha riscritta in modo che il compilatore controlli ogni passaggio. I matematici dopo il 1995 avevano una fiducia nel teorema pari al 99,9%. Ora puoi andare al cento per cento: Lean ha percorso l'intera derivazione dai tre assiomi standard e non c'è più nulla di cui dubitare.

Cosa ha controllato esattamente il computer?

Qui i numeri sono più appropriati degli epiteti.

• I 13,4 milioni di righe di Lean sono più di cinque volte più grandi dell'intera Mathlib, la principale libreria matematica formale del sistema.
• Sono stati dimostrati circa 30mila teoremi intermedi; la produzione finale ne ha coinvolti circa 29.500.
• La compilazione di un repository su una macchina a 96 core richiede circa 20 volte più tempo rispetto alla compilazione di Mathlib. Buzzard ha ricevuto per tutta la durata del test un server con 500 GB di RAM.
• La dipendenza è solo su tre assiomi standard Lean. Nessuna “ipotesi di semplicità”.

Kevin Buzzard, lo stesso matematico che dal 2024 guida il progetto di formalizzazione di Fermat per la comunità, ha scaricato il repository, lo ha assemblato ed ha eseguito il comparatore: la formulazione di output del teorema coincide con quella di riferimento di Mathlib, tutte le spunte sono verdi. La sua recensione: “uno straordinario risultato di auto-formalizzazione”.

Una riga a margine, tre secoli e mezzo di lavoro

Intorno al 1637, Pierre de Fermat attribuì l'affermazione a margine dell'Aritmetica di Diofanto: per n maggiore di due, l'equazione aⁿ + bⁿ = cⁿ non ha soluzioni in numeri naturali. Di seguito una frase diventata leggenda: “Ho trovato una dimostrazione davvero meravigliosa, ma i margini sono troppo stretti”. Generazioni di matematici, da Eulero a Kummer, si sono orientate verso il risultato in blocchi. Nel 1908 fu assegnato un premio di 100mila marchi d'oro per la prova e nel primo anno furono ricevute 621 soluzioni errate.

Nel giugno 1993, Andrew Wiles presentò la sua dimostrazione in una serie di conferenze a Cambridge. Due mesi dopo, un recensore pose una domanda che rivelò un buco in uno dei progetti. Per un anno, Wiles mise insieme tutto - prima da solo, poi insieme all'ex studente Richard Taylor - fu sul punto di mollare tutto, e nel 1995 pubblicò un testo di 129 pagine. Rimaneva l’ultima domanda “ingegneristica”: è possibile forzare il computer a confermare tutto questo nella sua interezza?

Non una nuova prova, ma una nuova opportunità

Si basa sull'analisi del 1995 di Darmon, Diamond e Taylor dell'argomentazione di Wiles-Taylor attraverso il teorema di Langlands-Tunnell e la discesa del livello di Ribet. L'idea di formalizzare Wiles è stata espressa negli anni 2000 dallo scienziato informatico olandese Jan Bergstra, ma fino a poco tempo fa questo era considerato il lavoro di un'intera direzione scientifica. I casi individuali - quarto grado, quelli semplici regolari - sono stati spostati a Lean prima. Con il nuovo repository si chiude l'intero elenco dei 100 compiti di formalizzazione di Weidik: il punto di riferimento con cui è stata confrontata quest'area ha vent'anni.

Buzzard, a proposito, scrive onestamente: matematicamente il lavoro non rivela nulla di nuovo - credeva già in Wiles. Il valore è altrove. La revisione di un nuovo articolo di matematica richiede mesi o addirittura anni; Se si può chiedere a una macchina di formalizzare una dimostrazione al volo, la revisione tra pari si ridurrà e le ipotesi nascoste a livello di esperti inizieranno ad emergere. Per la scienza, dove tutto si basa sull’onestà delle conclusioni, questo è un cambiamento serio.

Come apparivano quegli 11 giorni dall'interno

Il lavoro è stato guidato da Tianyi Peng, un ricercatore antropico che aveva precedentemente riunito un gruppo di strumenti di formalizzazione dell’intelligenza artificiale presso la Columbia University. Secondo lui inizialmente non aveva intenzione di arrivare alla fine: voleva solo vedere quanto Claude avrebbe fatto avanzare il progetto di Buzzard. Promosso in finale.

Molti agenti lavoravano in parallelo: alcuni completavano le definizioni matematiche, altri prendevano d'assalto i lemmi intermedi, altri risalivano l'albero dei teoremi e altri ancora riassemblavano le parti in un'unica conclusione. I primi giorni sono andati male: gli agenti hanno perso il quadro generale del progetto e circa il 7% dei primi tentativi è rimasto nel codice finale. La svolta è avvenuta quando il team è stato trasferito sulla piattaforma Prove2Me: la dimostrazione in essa contenuta è un grafico dei nodi del teorema, dove è possibile vedere cosa è già stato dimostrato, cosa attende i prerequisiti e cosa prendere dopo. Le affermazioni sono separate dalle dimostrazioni, la compilazione è accelerata e ogni teorema ha una descrizione testuale ricercabile. La portata del lavoro è di circa sei miliardi di gettoni di output e gli stimoli umani sono stati ridotti ad alto livello: “questa direzione è una priorità”.

Dove guardare

Il repository è pubblicato su GitHub: se lo desideri, puoi eseguire tu stesso il controllo se hai una macchina con 96 core e nervi saldi. Fonti primarie: analisi da Anthropic E Il post di Poiana sul blog del Progetto Xena.

E se, dopo una storia da 13 milioni di righe, vuoi vedere come i modelli moderni affrontano compiti più piccoli - algoritmi, codice, calcoli - dai un'occhiata alle sezioni "Codice" E "Chiacchierata" su NeuralSpace: lì puoi sperimentare i modelli e collegarli ai tuoi progetti tramite l'API.