Anthropic ha pubblicato il 4 settembre una formalizzazione verificata a macchina dell'Ultimo teorema di Fermat in Lean 4; la GitHub API colloca la creazione del repository alle 14:21:04 UTC. La tesi circolata era che Claude avesse dimostrato l'Ultimo teorema di Fermat in 11 giorni. I file del repository raccontano qualcosa di più circoscritto e, per certi versi, più interessante.
Che cosa dice il file di attribuzione
Il repo include un ATTRIBUTION.md che registra 106 file contenenti materiale del progetto FLT dell'Imperial College London guidato da Kevin Buzzard e del progetto flt-regular — "54 sotto Definitions/, 52 sotto P2M/Sol/; e i 23 file che riproducono il testo di Mathlib". Decine di righe recano la dicitura "whole file (100%)". Il file NOTICE data il prelievo: "Material was taken from the project's main branch as of 2026-05-21". Nel porting della toolchain a Lean 4.33, il file di attribuzione registra che ha "left the other 41 byte-identical".
La verifica è reale
Nulla di tutto ciò smentisce la verifica. Il README riporta che tutti i 60.475 moduli sono stati compilati, che #print axioms fermat_last_theorem è vincolato ai tre assiomi standard e che nessun modulo contiene axiom, sorry, native_decide, unsafe o partial def. La compilazione ha richiesto 5 ore e 32 minuti con 96 job, con un picco di 153 GB di memoria. I numeri di Anthropic: 13 milioni di righe di Lean, 29.500 teoremi intermedi usati nella dimostrazione finale, circa sei miliardi di token in output.
Che cosa non torna nella cornice ricevuta
Tre cose. Claude non ha dimostrato nulla di nuovo — si tratta di autoformalizzazione dell'esposizione Darmon–Diamond–Taylor del 1995 dell'argomento di Wiles–Taylor–Wiles, una dimostrazione conclusa dagli esseri umani trentuno anni fa. Non è un lavoro senza aiuto: secondo il conteggio di Anthropic, un nono del repository contiene testo Lean umano, in parte verbatim. E Buzzard, il matematico la cui recensione Anthropic cita, ha scritto lo stesso giorno sul proprio blog che "mathematically this work of anthropic tells us essentially nothing" e che la formalizzazione "just faithfully follows the early literature on the proof and adds nothing." Anche diverse testate lo hanno definito il file più grande del suo genere; invece si tratta di 60.475 moduli, non di un file.
La tesi onesta resta comunque grande
Le macchine possono ora tradurre migliaia di pagine di letteratura matematica esistente in forma verificabile dal kernel in meno di due settimane, partendo da diversi anni di lavoro volontario in Lean. È un risultato reale sulla velocità di traduzione. Non è un risultato sulla scoperta matematica, e il README ammette esso stesso il divario residuo: "What no tool can check is that each intermediate theorem means what its name suggests."