La rivendicazione sulla percolazione compila. La domanda resta.

Scientific American, a fine settembre, ha raccontato la vicenda come la soluzione di un sacro graal della probabilità da parte di un modello Anthropic. Tre giorni prima che la rivendicazione circolasse, Hugo Duminil-Copin aveva scritto che era solo questione di tempo prima che la congettura più famosa del suo campo «cadesse sotto i bulldozer». Il tono dominante è stato: ce l’ha fatta un’intelligenza artificiale. Il dettaglio più interessante sta un passo più in là.

La domanda classica riguarda una griglia di collegamenti che si aprono o si chiudono a caso. Sotto una soglia critica i gruppi restano finiti; sopra, possono aprirsi percorsi infiniti. Proprio sulla soglia, esiste già un ammasso infinito? Per le griglie piane e per dimensioni molto alte la risposta era no. Tra la dimensione tre e la dieci il problema restava aperto da decenni.

A fine agosto 2026, senza annuncio di lancio, nel repository pubblico formal-math di Anthropic è comparso uno sviluppo Lean attribuito a Claude. Afferma di dimostrare la Congettura 3 di Kozma e Nitzan del 2024, da cui seguirebbe θ(p_c) = 0 su reticoli interi in ogni dimensione almeno pari a due. Gil Kalai lo ha segnalato il 3 settembre chiamandolo una rivendicazione, non ancora un risultato. Il 6 settembre ha precisato che resta da verificare se la formalizzazione dice davvero ciò che i matematici intendevano, e che agli esperti servono ancora dettagli per digerire l’argomento.

Qui sta la cucitura. Un kernel Lean può certificare che ogni passo discende dalle definizioni scritte nel file. Non può certificare che quelle definizioni coincidano con la congettura umana. Il README del progetto lo ammette: il lavoro non è stato referato da nessuno indipendente dall’autore; la correttezza poggia sui controlli meccanici; chi legge dovrebbe controllare che Challenge.lean enunci il teorema voluto. La guida di quindici pagine è presentata come aiuto alla lettura, non come garanzia. Note di registro indicano Justin Leder come direttore del lavoro e attribuiscono il codice Lean all’AI. Un audit strutturale riassunto su whataifound ha trovato reticolo, misura di Bernoulli, θ e p_c allineati ai sensi da manuale, senza sorry fuori dai segnaposto previsti — e senza che un matematico avesse ancora letto l’intera argomentazione.

Il 3 ottobre 2026, sul branch main di anthropics/formal-math la directory percolation non c’era più: restava visibile solo la formalizzazione zeta23. I file esistono ancora al commit fissato 795efb86 del 28 agosto. Non è una prova di ritiro né di errore. È solo il fatto che l’artefatto non sta più dove un link a main si aspetterebbe di trovarlo.

La notizia utile non è «un modello ha dimostrato un teorema». È che, finito il controllo della macchina, resta aperta la distanza tra un enunciato che compila e un risultato che la comunità può dare per chiuso.