PaperFormalizer: autoformalizzazione degli articoli scientifici in Lean con la partecipazione dell’autore

Abstract degli autori

Anche un articolo revisionato con cura può lasciare piccole lacune nelle dimostrazioni o nelle ipotesi dichiarate. Presentiamo PaperFormalizer, una pipeline basata su agenti e su Lean che aiuta gli autori a individuare e colmare queste lacune nei propri articoli e a ottenere per ciascuno una versione verificata in Lean. Partendo dal sorgente LaTeX, PaperFormalizer trascrive l’articolo in un grafo delle dipendenze tra enunciati, verifica in linguaggio naturale la fedeltà, l’ambiguità e la correttezza di ciascun enunciato, quindi formalizza e dimostra gli enunciati in Lean usando Mathlib, eventuali librerie specialistiche e gli strumenti personali dell’autore. Solo l’autore sa che cosa intende esprimere con un enunciato e quale sia il modo migliore per colmare una lacuna nella formalizzazione di un risultato. Per questo la pipeline si ferma e consulta l’autore ogni volta che un enunciato ammette più di un’interpretazione, presenta ogni modifica proposta in linguaggio naturale e con simboli TeX, affinché l’autore possa accettarla, rifiutarla o indicare un’altra direzione, e lascia all’autore ogni decisione che potrebbe cambiare le affermazioni dell’articolo. Il risultato è una versione annotata e rivista dell’articolo, un resoconto delle modifiche e codice Lean in cui ogni dichiarazione è collegata all’enunciato che formalizza. Gli strumenti personali dell’autore si arricchiscono man mano che vengono formalizzati altri articoli, e gli autori possono condividere i propri articoli verificati affinché i ricercatori che vi si basano possano riutilizzarne il codice Lean. Rendendo praticabile la produzione di articoli verificati, PaperFormalizer mira a rendere più solida la ricerca fondata su dimostrazioni matematiche. PaperFormalizer funziona all’interno di un agente di programmazione (Claude Code o Codex) ed è disponibile all’indirizzo https://github.com/Jiyuan-Tan/PaperFormalizer. Gli articoli con codice Lean condivisi dagli utenti sono disponibili all’indirizzo https://paperformalizer.org.