即便经过仔细校对的论文，也难免在证明或所设假设上留下细微缺口。PaperFormalizer 试图用 Lean 生态中的智能体流水线帮助作者发现并闭合这些缺口，最终把论文转化为经过 Lean 验证的版本。该工作由 Jiyuan Tan 等作者提交，论文摘要于 2026 年 10 月 22 日发布在 arXiv 上。
它的起点是论文的 LaTeX 源文件。系统先把论文转写为一个由陈述组成的依赖图，使各条定义、引理、定理与推论之间的依赖关系显式化。随后，它在自然语言层面对每条陈述进行审计，检查其是否忠实于原文、是否存在歧义、以及是否正确。这一阶段并不急于形式化，而是先确保自然语言表述本身经得起推敲。
在审计之后，流水线会把陈述在 Lean 中形式化，并尝试完成证明。证明所依赖的背景包括 Mathlib、可选的领域库，以及作者个人的工具包。随着更多论文被形式化，作者的工具有望不断积累和扩展。
论文强调，只有作者才真正知道一条陈述想要表达什么，以及某个结果中的形式化缺口应当如何最好地修补。因此，流水线在设计上把涉及语义判断的决定留给作者。当一条陈述可以被多种方式解读时，系统会停下来询问作者；对于每一处修复，它都会以自然语言和 TeX 符号呈现为提案，作者可以接受、拒绝或重新引导；任何可能改变论文主张的决定，也都交由作者拍板。
最终产出包括三个部分：带注释并经过修订的论文版本、一份变更报告，以及 Lean 代码。在 Lean 代码中，每个声明都与它所形式化的那条陈述建立链接，便于追溯。作者可以共享自己已验证的论文，使后续研究者能够直接复用其中的 Lean 代码。
PaperFormalizer 运行在编程智能体环境中，例如 Claude Code 或 Codex。项目代码已在 GitHub 上公开，用户共享 Lean 代码的论文则发布在 paperformalizer.org。通过降低产出经过验证的论文的门槛，作者希望让依赖数学证明的研究更加稳健。