即便經過仔細校對的論文，也難免在證明或所設假設上留下細微缺口。PaperFormalizer 試圖用 Lean 生態中的智能體流水線幫助作者發現並閉合這些缺口，最終把論文轉化為經過 Lean 驗證的版本。該工作由 Jiyuan Tan 等作者提交，論文摘要於 2026 年 10 月 22 日發佈在 arXiv 上。
它的起點是論文的 LaTeX 源文件。系統先把論文轉寫為一個由陳述組成的依賴圖，使各條定義、引理、定理與推論之間的依賴關係顯式化。隨後，它在自然語言層面對每條陳述進行審計，檢查其是否忠實於原文、是否存在歧義、以及是否正確。這一階段並不急於形式化，而是先確保自然語言表述本身經得起推敲。
在審計之後，流水線會把陳述在 Lean 中形式化，並嘗試完成證明。證明所依賴的背景包括 Mathlib、可選的領域庫，以及作者個人的工具包。隨着更多論文被形式化，作者的工具有望不斷積累和擴展。
論文強調，只有作者才真正知道一條陳述想要表達什麼，以及某個結果中的形式化缺口應當如何最好地修補。因此，流水線在設計上把涉及語義判斷的決定留給作者。當一條陳述可以被多種方式解讀時，系統會停下來詢問作者；對於每一處修復，它都會以自然語言和 TeX 符號呈現為提案，作者可以接受、拒絕或重新引導；任何可能改變論文主張的決定，也都交由作者拍板。
最終產出包括三個部分：帶註釋並經過修訂的論文版本、一份變更報告，以及 Lean 代碼。在 Lean 代碼中，每個聲明都與它所形式化的那條陳述建立鏈接，便於追溯。作者可以共享自己已驗證的論文，使後續研究者能夠直接複用其中的 Lean 代碼。
PaperFormalizer 運行在編程智能體環境中，例如 Claude Code 或 Codex。項目代碼已在 GitHub 上公開，用户共享 Lean 代碼的論文則發佈在 paperformalizer.org。通過降低產出經過驗證的論文的門檻，作者希望讓依賴數學證明的研究更加穩健。