Nel 1995 il matematico britannico Andrew Wiles rese pubblica la dimostrazione in 129 pagine dell’Ultimo Teorema di Fermat. Dopo decenni in cui la verifica riga per riga da parte di un calcolatore sembrava richiedere anni di lavoro umano, una rete di agenti basata sull’intelligenza artificiale di Anthropic ha formalizzato l’intero testo in appena 11 giorni.
L’esperimento non ha introdotto una nuova dimostrazione teorica, ma ha tradotto i passaggi logici originali in Lean 4, un software strutturato per controllare la validità matematica di ogni passaggio formale.
Nel 2024 la comunità accademica aveva impostato un percorso guidato da Kevin Buzzard dell’Imperial College di Londra, organizzato su una roadmap di 86 pagine concepita per svilupparsi lungo diversi anni. Il modello automatizzato ha superato quella pianificazione lavorando in autonomia quasi totale.
La struttura logica da 13 milioni di righe
Per completare la trasposizione formale, gli agenti intelligenti hanno generato 13 milioni di righe di codice Lean. Si tratta di un volume che supera di oltre cinque volte l’intero archivio matematico Mathlib.
Il sistema ha analizzato e risolto 30.300 teoremi e lemmi intermedi. Di questi, circa 29.500 sono confluiti nella catena deduttiva finale, con un consumo di 6 miliardi di token attraverso un modello di ricerca interno ad Anthropic affine a Fable 5.1.
L’organizzazione modulare del calcolo
La gestione di una simile mole di istruzioni è stata resa possibile dall’uso di un grafo aciclico diretto, che ha assegnato a ogni agente una porzione logica autonoma senza generare dipendenze circolari.
Separare la definizione iniziale degli enunciati dalla loro effettiva dimostrazione ha permesso la compilazione parallela dei moduli, velocizzando i riscontri della macchina senza attendere il completamento della catena complessiva.
Matematica
Verifica indipendente e requisiti hardware
La validità dell’intero impianto matematico poggia esclusivamente sui tre assiomi fondamentali di Lean, escludendo scorciatoie o presupposti privi di dimostrazione. L’enunciato definitivo combacia perfettamente con quello archiviato in Mathlib.
Un controllo esterno è stato eseguito tramite nanoda, un verificatore indipendente sviluppato in Rust che ha riesaminato oltre un milione di dichiarazioni analizzando l’impatto e la latenza della memoria.
Il file risultante presenta una verbosità superiore a quella di un testo redatto a mano e richiede un picco di 153 GB di RAM durante la compilazione. Il flusso operativo dimostra la fattibilità di una digitalizzazione rapida della letteratura scientifica passata, aprendo alla revisione automatica di errori rimasti inosservati nelle pubblicazioni storiche.
