Immaginate una biblioteca in cui, ogni poche settimane, qualcuno cambia la misura degli scaffali. I libri restano gli stessi, ma metà non entra più al proprio posto: bisogna rifilare una copertina, spostare un volume, riscrivere un’etichetta. Se nessuno lo fa, il libro non sparisce, però nessuno riesce più a tirarlo giù. Dopo un anno la biblioteca è piena di opere intatte e inservibili.
È la condizione quotidiana della matematica formalizzata in Lean, e il problema a cui prova a rispondere Lean Pool: An AI-Maintained Archive of Formalized Mathematics, depositato su arXiv il 21 settembre 2026 (2609.25199) e in questi giorni fra i paper in tendenza su Papers with Code. Lo firma da solo Vasily Ilin, della University of Washington; nei ringraziamenti Justin Asher compare come co-creatore dell’archivio. E c’è una dichiarazione dell’autore da mettere subito in chiaro: la parte scritta da un essere umano è una pagina. Il resto è «prodotto quasi interamente dall’AI», e i numeri, assicura la dichiarazione finale, vengono da registri conservati e ricalcolati, non da misure sintetiche.
Il collo di bottiglia si è spostato
Generare argomenti matematici con un modello è diventato facile; leggerli e controllarli no. Lean è un linguaggio in cui una dimostrazione si scrive in modo che un piccolo programma, il kernel, possa verificarla passo per passo: se compila, è corretta rispetto all’enunciato scritto. Per questo accompagna sempre più spesso i risultati ottenuti con l’AI. Il paper cita due rilasci recenti di OpenAI, fra cui quello sull’esplosione in tempo finito per Navier–Stokes, usciti insieme alle loro formalizzazioni.
Ma una formalizzazione non vive da sola. Poggia su Mathlib, la grande libreria comune di Lean, e Mathlib cambia di continuo: nomi cambiati, lemmi spostati, interfacce riscritte. Un progetto chiuso e lasciato lì prima o poi smette di compilare. E Mathlib stessa, osserva Ilin, cresce a ritmo lineare perché ogni contributo passa per una revisione umana severa: garanzia di qualità, e motivo per cui le mancano ancora molte definizioni e teoremi della matematica di ricerca.
Lean Pool è la risposta: non una libreria integrata come Mathlib, ma un archivio di progetti indipendenti, ciascuno con la propria paternità, tenuti insieme nello stesso ambiente e aggiornati in blocco. La visione dichiarata è un analogo formale di arXiv, ma mantenuto: un posto dove depositare in fretta un lavoro nuovo, con attrito minimo.
Nel paper «agente» vuol dire quello che vuol dire altrove: un modello che legge un errore di compilazione, chiama gli strumenti, prova una correzione, osserva il risultato e riprova. Il ciclo è costruito da capo nel libro.
Come funziona il cantiere
Un progetto entra in due modi. Lo propone un contributore, che non deve per forza esserne l’autore, oppure lo trova un agente: ogni giorno alcuni job automatici cercano formalizzazioni recenti e meno recenti con licenza Apache-2.0 o MIT, ne controllano attribuzione, licenza, dipendenze e costo, e preparano la richiesta di importazione. Sono ammessi solo lavori completi su risultati noti e con un nome: niente sorry o admit, i buchi che Lean lascia passare con un avviso; nessun assioma oltre ai tre standard (Classical.choice, propext, Quot.sound); niente set_option, dichiarazioni non verificate o meccanismi che aggirino i limiti di risorse e i linter. Ogni progetto ha una scheda con autori, fonte, risultati principali accompagnati dall’enunciato informale e un’etichetta di provenienza: dimostrazione scritta da persone, da un’AI o a quattro mani.
Le porte sono tre, e controllano cose diverse. Il kernel di Lean garantisce che le dimostrazioni siano corrette. I linter, quelli di Mathlib più alcuni controlli propri dell’archivio, controllano forma e igiene. Resta la domanda che nessun compilatore può fare: l’enunciato formale dice davvero ciò che il progetto dichiara di aver dimostrato? Per quella c’è una revisione affidata a un modello linguistico, che legge il contributo e ne giudica fedeltà, novità, rilevanza, fonti e qualità del codice.
Poi c’è la manutenzione, che è il cuore della proposta. Quando esce una nuova versione di Lean e Mathlib, un workflow separato ricompila tutto l’archivio senza toccarlo, assegna ogni progetto rotto a un agente di riparazione, raccoglie le patch e apre una richiesta di merge in bozza. Altri agenti, a giro, accorciano le dimostrazioni e riducono tempi di compilazione e memoria. Sopra, la decisione su che cosa entra resta ai maintainer umani.
I numeri del registro
Il paper non ha un esperimento centrale, ha registri. Alla data di osservazione, il 21 settembre, l’archivio contava 211 progetti completi, 7.043 file, 3.228.485 righe fisiche (commenti e righe vuote compresi) e 837 risultati principali registrati. Per provenienza, 70 progetti hanno dimostrazioni scritte da persone, 102 da un’AI, 39 miste. I contributori con commit sono 18, le richieste di merge arrivate dalla comunità e accolte 63. Dentro ci sono lo sviluppo sui teoremi di incompletezza di Gödel, la classificazione delle superfici compatte, la congettura polinomiale di Freiman–Ruzsa, e il progetto più grosso di tutti, sull’esplosione in tempo finito per Navier–Stokes ed Euler: 641.073 righe, dimostrazioni etichettate come scritte da un’AI, circa un quinto dell’intero archivio da solo.
La prova più interessante riguarda gli aggiornamenti, cioè la biblioteca con gli scaffali che cambiano. In sei salti di versione, da Lean 4.30 a 4.34, la quota di progetti che non compilavano più è andata da un minimo di 3 su 148 a un massimo di 100 su 143 (le prime cinque misure sono ricostruite a posteriori, l’ultima viene dal registro di produzione).
Il salto verso la versione stabile 4.34.0 è documentato nei dettagli. Dei 191 progetti sondati, 97 davano errori di compilazione; sono partiti 97 job di riparazione, 95 hanno chiuso con successo, 2 no (i progetti sul gruppo fondamentale dei grafi e sull’incompletezza). Il tasso di rottura, $97/191 \approx 0{,}51$, è di circa un progetto su due. Ma i job riusciti non bastavano, e il paper non lo nasconde. È servita un’ulteriore integrazione, sempre assistita da agenti, per sistemare gli errori residui, gli avvisi e le interfacce cambiate. Alla fine sono entrati 198 progetti (nel frattempo ne erano arrivati altri), con 639 file toccati e 5.951 righe aggiunte o tolte. Ore di lavoro umano e spesa in denaro non sono state registrate.
Le ottimizzazioni danno numeri modesti. Una compressione estesa a tutta la libreria ha tolto 45.217 righe e accorciato la build completa del 3,3%; un’altra passata ha rimosso 54.965 righe e guadagnato il 5,8%. Un giro di proof golfing, l’arte di accorciare le dimostrazioni, ha invece allungato la build del 5,4%, pur usando meno memoria.
Un revisore difficile da misurare
La parte più delicata è la revisione affidata al modello, perché è l’unica porta che controlla il significato. Il servizio ha lasciato 296 rapporti strutturati: 188 approvazioni, 71 richieste di modifica, 37 verdetti di discussione. I problemi trovati riguardano enunciati non conformi al risultato dichiarato, attribuzioni, risultati incompleti, definizioni duplicate, codice superfluo. Il paper riporta anche un dato difficile da leggere: quando la stessa richiesta di merge è stata rivista più volte, i verdetti coincidono in 37 coppie su 69, poco più della metà. Ma fra una revisione e l’altra potevano cambiare il codice e il modello revisore, e una richiesta di modifiche seguita da un’approvazione è proprio ciò che si spera. Il confronto che misurerebbe la coerenza del revisore, a parità esatta di codice, è impossibile: di coppie così non ce n’è nessuna. E nessuno ha verificato in modo indipendente l’accuratezza dei verdetti. Il servizio, infine, è stato spento a mano prima della data di osservazione: i rapporti conservati si fermano al 13 settembre e non coprono gli import più recenti.
I costi registrati raccontano due regimi. Con le chiamate API della prima versione, 285 rapporti hanno un costo stimato di circa 309 dollari in tutto, con una mediana di venti centesimi. Con la versione successiva, che spezza le modifiche grandi in porzioni, 6 rapporti hanno un costo equivalente stimato di 752 dollari, con una mediana di 89. Sono stime, avverte il testo, non fatture, e non contano le esecuzioni andate perse.
Che cosa costa tenerlo insieme
Accogliere tutto ha un prezzo in risorse. Sulla stessa macchina, con una build per libreria, Lean Pool conta 3,23 milioni di righe contro i 2,33 di Mathlib; la build completa richiede 60 minuti contro 37 e un picco di 20 GiB di memoria contro poco più di 7. Il profiling delle prestazioni, nell’archivio, è solo consultivo: segnala, non blocca. In Tau Ceti, un progetto vicino in cui l’AI scrive matematica secondo tabelle di marcia umane, il confronto delle prestazioni è invece una condizione per il merge.
Quanto al riuso, la prova sta in un audit separato chiamato LeanEval, in cui Lean Pool è il repository pubblico con codice corrispondente nel maggior numero di soluzioni: 20, contro 8 del progetto sulla classificazione delle superfici, che viene subito dopo (una soluzione può combaciare sia con l’archivio sia con il repository d’origine di un suo progetto). È un segnale incoraggiante, con una riserva: nella bibliografia quell’audit risulta un manoscritto di autori anonimi, quindi oggi il lettore non può verificarlo.
I limiti
Il primo è di genere: il paper analizza il registro operativo dei mesi fra giugno e settembre, non una prova controllata; non c’è un gruppo di confronto, e ogni misura di ottimizzazione sull’intera libreria viene da una sola build prima e dopo. Il secondo è di sostanza: durante la migrazione alla versione stabile alcune ipotesi ausiliarie sono state rafforzate (su misurabilità, sigma-finitezza, massimalità), e il paper precisa che la build riuscita garantisce la compatibilità degli enunciati accolti, non l’equivalenza di ogni dichiarazione prima e dopo. Se a riparare è un agente, è il punto da sorvegliare: una dimostrazione che torna a compilare perché l’enunciato è diventato un po’ più debole è corretta, ma non è più la stessa cosa. Il terzo non lo solleva il paper, ma salta all’occhio: le decisioni di merge spettano ai maintainer, e due dei cinque casi di riuso registrati sono sviluppi controllati dal maintainer dell’archivio.
Perché conta adesso
Se la matematica prodotta con i modelli continuerà a uscire a questo ritmo, il problema non sarà generarla ma tenerla usabile: trovare un teorema, capirne le ipotesi, importarlo senza ricostruirlo. Lean Pool scommette che quel lavoro di manutenzione, noioso e continuo, sia il mestiere giusto per gli agenti, lasciando alle persone la decisione su che cosa entra. I registri dicono che il meccanismo regge: sei aggiornamenti attraversati, con quote di progetti rotti fra il 2 e il 75 per cento, l’ultimo chiuso solo dopo un secondo giro di integrazione. Dicono anche dove non basta ancora: un revisore di cui nessuno ha misurato l’affidabilità, e che nel frattempo è stato spento. La domanda aperta non è se un agente sappia far ricompilare una dimostrazione. È chi si accorge quando, per farla ricompilare, ha cambiato che cosa dimostra.
I commenti sono riservati agli iscritti.
Accedi per commentare