Anthropic ha pubblicato il 4 settembre la prima dimostrazione completa dell’ultimo teorema di Fermat verificata da un computer. Il lavoro è stato svolto da decine di agenti Claude che, in gran parte da soli, hanno scritto in undici giorni tredici milioni di righe di codice nel linguaggio Lean.
Che cosa vuol dire “formalizzare”
Una dimostrazione matematica scritta per esseri umani salta i passaggi ovvi e si appoggia a secoli di risultati già pubblicati. Un assistente di prova come Lean non concede nulla: ogni passaggio va scritto per esteso, e si può usare solo quello che è già stato formalizzato prima. In cambio, il computer controlla la logica in modo automatico e dice se regge oppure no.
Serve perché verificare a mano una dimostrazione lunga è un mestiere lento e fallibile. Andrew Wiles presentò la sua prova dell’ultimo teorema di Fermat nel giugno 1993; due mesi dopo un revisore trovò una falla che gli costò un anno di lavoro, chiuso solo con l’aiuto di Richard Taylor. La versione corretta, pubblicata nel 1995, occupa 129 pagine.
Undici giorni, trentamila teoremi
Il progetto è nato da Tianyi Peng, ricercatore di Anthropic il cui gruppo alla Columbia University costruisce strumenti per la formalizzazione automatica. Gli agenti hanno prodotto 30.300 teoremi intermedi verificati, di cui 29.500 finiti nella dimostrazione finale. L’intervento umano si è limitato a indicazioni sulle priorità, del tipo “questa parte sembra urgente”.
Il conto delle risorse è alto: circa sei miliardi di token in uscita, generati da un modello di ricerca interno che Anthropic descrive come grosso modo paragonabile a Claude Fable 5.1. Il risultato è cinque volte più lungo di Mathlib, la libreria comunitaria di dimostrazioni formalizzate su cui il lavoro si appoggia — segno, ammette l’azienda, che la prova è molto più prolissa del necessario. Usa comunque soltanto i tre assiomi standard di Lean, senza scorciatoie né passaggi lasciati in sospeso.
Quello che gli agenti non hanno fatto da soli
I primi tentativi sono falliti: gli agenti perdevano il filo del progetto e smettevano di collaborare. La svolta è arrivata con Prove2Me, una piattaforma aperta ideata da Peng e dai suoi collaboratori alla Columbia, che tiene un grafo dei teoremi da dimostrare e permette a più agenti di lavorare in parallelo senza pestarsi i piedi. Non è un prodotto Anthropic.
Anche la matematica di partenza non era terra vergine. La dimostrazione segue l’esposizione di Darmon, Diamond e Taylor della prova di Wiles, e riutilizza pezzi del progetto di formalizzazione guidato da Kevin Buzzard all’Imperial College di Londra e del progetto flt-regular. Buzzard, che ha esaminato il risultato su richiesta di Anthropic, lo ha definito un traguardo straordinario e ha aggiunto che gli oggetti prodotti dalla formalizzazione automatica sono ormai abbastanza solidi da poterci costruire sopra. Sul suo blog ha però intitolato il commento “Anthropic mi ha battuto sul tempo”: il lavoro umano su cui gli agenti hanno poggiato i piedi è di anni, ed è pubblico.
A che cosa serve davvero
La parte interessante non è il teorema, dimostrato trent’anni fa. È che formalizzare risultati complessi smette di essere un progetto pluriennale. In un esperimento minore, gli stessi ricercatori hanno formalizzato il teorema dei tre primi di Vinogradov in tre giorni usando tre abbonamenti Claude Max ordinari.
Se regge, cambia il modo in cui la comunità matematica controlla il proprio lavoro — compreso quello prodotto dalle macchine, che cresce più in fretta di quanto i revisori umani riescano a leggere. Anthropic ha già pubblicato risultati su altri fronti scientifici, dalle proteine progettate e verificate in laboratorio in poi, ma qui il punto è diverso: non è la macchina che scopre, è la macchina che controlla. E il controllo, a differenza della scoperta, si può verificare riga per riga.
Fonte: Anthropic; commento di Kevin Buzzard sul blog Xena Project.
Immagine: Pexels, licenza libera.
