Il fatto
Anthropic ha annunciato la prima dimostrazione completa dell'Ultimo Teorema di Fermat verificata da computer. Claude, orchestrato da un harness multi-agente basato su Claude Code, ha lavorato in gran parte in autonomia per 11 giorni scrivendo la prova nel linguaggio Lean: 30.300 teoremi dimostrati, di cui 29.500 usati nella dimostrazione finale. Il post di Anthropic è del 4 settembre 2026; i log citati segnano il completamento alle 02:00 UTC del 18 agosto. La discussione su Hacker News è già molto attiva.
Perché conta
Formalizzare la dimostrazione di Wiles era considerato un progetto pluriennale: l'impresa comunitaria partita nel 2024 da Kevin Buzzard all'Imperial College ha un solo blueprint iniziale di 86 pagine. Il risultato è arrivato invece in poco meno di due settimane, su iniziativa del ricercatore Tianyi Peng, che voleva solo testare se Claude potesse fare progressi.
La matematica non è nuova: la prova segue la versione semplificata di Wiles di Darmon, Diamond e Taylor. A cambiare è la verifica. Una dimostrazione per lettori umani si controlla per mesi: quella originale di Wiles (1995) è di 129 pagine e nel 1993 un revisore ne trovò una lacuna critica, colmata dopo un anno di lavoro con Richard Taylor. Qui il controllo è algoritmico, come una calcolatrice verifica un calcolo.
Buzzard, che ha ricevuto il risultato, scrive:
This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics.
Cosa cambia in concreto
- Prove2Me è la piattaforma che ha sbloccato il progetto. Collaborativa e aperta, progettata da Peng e collaboratori alla Columbia University: mantiene un DAG di enunciati che indica agli agenti cosa dimostrare dopo, separa enunciati e prove in file distinti per accelerare la compilazione Lean e conserva una descrizione in linguaggio naturale di ogni teorema per ricerca e riuso.
- I tentativi precedenti, senza questa struttura, fallivano: gli agenti perdevano lo stato del progetto e smettevano di collaborare in modo efficace. Quei fallimenti hanno comunque lasciato circa il 7% delle righe non-boilerplate della prova finale.
- L'input umano si è limitato a istruzioni ad alto livello: «Jacobian as a scheme sounds high priority», «push the Mazur to be done soon».
- Consumo dichiarato: circa sei miliardi di token di output. La frase della fonte si interrompe prima di precisare modello e costi.
- Per scala: 13 milioni di righe di Lean, oltre cinque volte la dimensione di Mathlib, la libreria comunitaria su cui la formalizzazione si appoggia.
Per chi usa proof assistant il punto operativo è quello che emerge dalla valutazione di Buzzard: gli artefatti di autoformalizzazione sono ormai abbastanza robusti da essere costruiti sopra, e la prova è multi-livello. Se confermato, abbassa il costo di verificare risultati nuovi, oggi valutato in mesi o anni di revisione tra pari.
Cosa non è ancora chiaro
- La verifica indipendente. Lo stesso Buzzard qualifica il momento come «historic moment (modulo re-check)»: la fonte non dice se la ricontrolla della community Lean sia in corso, completata o quanto tempo richiederà.
- Non è noto quale modello esatto abbia prodotto la prova: la frase sui token si tronca su «a general-purpose internal…».
- La fonte pubblica solo estratti del ragionamento degli agenti e non specifica se e quando l'intero repository Lean sarà reso pubblico.
- Anthropic è insieme autrice del risultato e parte interessata: nel materiale non risultano valutazioni esterne già documentate.
Lascia un commento