L’ANALISI
Claude formalizza il teorema di Fermat in Lean: la verifica conta più della scoperta
Claude ha prodotto una formalizzazione completa del teorema di Fermat in Lean. Cosa verifica davvero il kernel, come hanno lavorato gli agenti e quali limiti restano.
In breve: il risultato rende controllabile da software una prova matematica già nota. Il punto non è che Claude abbia scoperto un nuovo teorema, ma che un sistema multi-agente abbia trasformato una dimostrazione molto estesa in un artefatto accettato da kernel formali indipendenti.
Che cosa è stato pubblicato
Il repository contiene la chiusura di import della prova finale, 1.450 moduli di definizioni e 29.511 moduli con enunciati e prove. Il progetto usa Lean 4.33.1 e Mathlib 4.33.0, espone il percorso della dimostrazione e documenta i comandi per ripetere build e verifiche.
Come hanno collaborato gli agenti
Decine di agenti hanno definito concetti e risolto teoremi intermedi. I primi tentativi hanno perso lo stato del progetto. Il passaggio a Prove2Me ha introdotto un grafo aciclico delle dipendenze, descrizioni ricercabili e separazione tra enunciati e prove, così gli agenti potevano lavorare in parallelo senza ricostruire ogni volta il contesto.
Che cosa controllano Lean e i kernel
Lean verifica che ogni passaggio segua dalle regole e dagli assiomi ammessi. Il comparator controlla che l’enunciato coincida con quello di Mathlib e riproduce l’ambiente nel kernel; il repository dichiara anche l’accettazione da parte di nanoda, un’implementazione indipendente. Questo riduce la fiducia richiesta nella prosa generata, non elimina la necessità di capire la matematica.
Perché non è una nuova scoperta matematica
La formalizzazione segue una versione semplificata della dimostrazione di Wiles esposta da Darmon, Diamond e Taylor e riusa lavoro open source precedente. La novità è la scala e la velocità dell’autoformalizzazione, non un metodo matematico alternativo per dimostrare il teorema.
Condizioni e limiti
Non è una nuova dimostrazione matematica: formalizza una variante semplificata della prova nota di Wiles. Tempi, token e grado di autonomia sono dichiarati da Anthropic; il repository rende il risultato ispezionabile, ma in questo controllo non è stato ricompilato integralmente per i requisiti dichiarati di centinaia di gigabyte e molte ore.
Checklist per valutare risultati simili
- Controlla che codice, toolchain e dipendenze siano versionati.
- Distingui l’enunciato verificato dalla narrazione del vendor.
- Verifica assiomi ammessi e corrispondenza con l’enunciato canonico.
- Cerca un secondo checker o kernel indipendente.
- Se serve una verifica propria, pianifica prima RAM, spazio disco e durata.