PaperFormalizer è stato presentato su arXiv il 26 ottobre 2026. È una pipeline agentica basata su Lean che aiuta gli autori a trovare e chiudere le lacune nascoste nei propri articoli scientifici. Trasforma gli articoli in versioni verificate formalmente. Lo strumento è descritto in un lavoro sull’autoformalizzazione degli articoli in Lean. Affronta un problema noto a chiunque scriva matematica. Anche un testo rilegato con cura può lasciare piccoli gap nelle dimostrazioni o nelle assunzioni dichiarate. L’obiettivo dichiarato è rendere praticabile la produzione di articoli verificati, per rendere più robusta la ricerca che si fonda su dimostrazioni matematiche.
Che cos’è PaperFormalizer e perché è rilevante
PaperFormalizer nasce per rispondere a un limite strutturale della pubblicazione scientifica tradizionale. Un articolo sottoposto a revisione tra pari e letto con attenzione può comunque contenere enunciati ambigui. Può contenere passaggi dimostrativi incompleti o ipotesi non esplicitate. Il linguaggio naturale infatti non forza la completezza logica.
La risposta proposta è una pipeline agentica costruita attorno a Lean. Lean è il linguaggio di dimostrazione interattiva. In esso ogni affermazione va provata passo per passo contro un nucleo formale. Il sistema parte dal sorgente LaTeX di un articolo e lo trascrive in una versione verificata in Lean. Se la trascrizione va a buon fine, ogni risultato dichiarato ha una dimostrazione controllata dalla macchina. La pipeline si interrompe ogni volta che un enunciato ammette più di una lettura, perché per dimostrarlo occorre prima dire esattamente cosa afferma.
Come funziona la pipeline di autoformalizzazione
Il flusso parte dal sorgente LaTeX dell’articolo. PaperFormalizer trascrive l’articolo in un grafico delle dipendenze tra enunciati. Ogni definizione, lemma e teorema diventa un nodo. Le relazioni di uso tra essi diventano archi. Questa struttura permette al sistema di lavorare sugli enunciati uno alla volta, rispettando l’ordine logico dell’articolo.
Ogni enunciato viene poi sottoposto a un audit in linguaggio naturale su tre dimensioni: fedeltà, ambiguità e correttezza. In pratica, il sistema controlla che la versione formale dica ciò che l’autore intendeva, che l’enunciato non ammetta letture multiple e che sia vero.
Segue la fase più pesante: la formalizzazione e la dimostrazione in Lean. I controlli avvengono contro Mathlib, la libreria standard della comunità Lean. Avvengono anche contro librerie di dominio opzionali e contro il toolkit personale dell’autore. Il toolkit è l’insieme di formalizzazioni già costruite nelle sessioni precedenti.
Il ruolo centrale dell’autore
L’elemento distintivo è la filosofia “author-in-the-loop”. Solo l’autore sa cosa un enunciato vuole davvero dire. Solo l’autore sa come una lacuna nella formalizzazione di un risultato va corretta al meglio. Per questo, quando la pipeline si ferma, la domanda va a lui.
Le correzioni non vengono applicate in autonomia. Ogni riparazione è presentata come una proposta, esplicitata sia in linguaggio naturale sia in simboli TeX, che l’autore può accettare, rifiutare o ridirigere. Le decisioni che potrebbero cambiare ciò che l’articolo afferma restano tutte in mano all’autore. Il sistema non riscrive i risultati, ma segnala dove il testo non regge e suggerisce come sistemarlo.
Output, strumenti e benefici per la comunità
Alla fine del processo l’autore riceve una versione annotata e rivista dell’articolo. Riceve anche un report delle modifiche effettuate e il codice Lean prodotto. In questo codice ogni dichiarazione è collegata all’enunciato dell’articolo che formalizza. Il collegamento esplicito tra testo e codice rende tracciabile la corrispondenza tra la matematica pubblicata e la sua versione verificata.
Due meccanismi di crescita accompagnano lo strumento. Il toolkit dell’autore si espande a ogni articolo formalizzato, così che le formalizzazioni già svolte diventano materiali riutilizzabili nei lavori successivi. In più, gli autori possono condividere i propri articoli verificati e mettere a disposizione il codice Lean. I ricercatori che costruiscono su quei risultati possono riutilizzarlo direttamente. Una piattaforma raccoglie i papers con codice Lean condiviso dagli utenti.
Sul piano pratico, PaperFormalizer gira dentro un agente di codifica esistente, Claude Code o Codex. Il sistema è disponibile attraverso il repository indicato nel lavoro. La proposta si rivolge a chi lavora nella scrittura scientifica o nella verifica formale.
Fonti:
Punti chiave
Da ricordare
- PaperFormalizer è una pipeline agentica basata su Lean che trasforma articoli scientifici in versioni verificate formalmente, partendo dal sorgente LaTeX.
- Ogni enunciato viene auditato in linguaggio naturale per fedeltà, ambiguità e correttezza prima della formalizzazione.
- Davanti a un enunciato ambiguo la pipeline si ferma e lascia all'autore ogni decisione che potrebbe cambiare ciò che l'articolo afferma.
- Le correzioni sono proposte in linguaggio naturale e simboli TeX, e l'autore può accettarle, rifiutarle o ridirigerle.
- L'output comprende una versione annotata e rivista dell'articolo, un report delle modifiche e codice Lean con dichiarazioni collegate agli enunciati.
- Il sistema gira dentro agenti di codifica come Claude Code o Codex e il toolkit dell'autore cresce a ogni articolo formalizzato.
