PaperFormalizer：在精益框架下实现研究论文的作者参与式自动形式化

arXiv:2610.31810v1 发布类型：新 基本摘要：即使经过仔细校对的论文，其证明或所作假设中也可能存在细微漏洞。我们提出了 PaperFormalizer，一个基于 Lean 的智能体驱动流水线，帮助作者发现并弥补自身论文中的此类漏洞，并将每篇论文转化为经 Lean 验证的版本。PaperFormalizer 从 LaTeX 源文件入手，将其转换为陈述的依赖关系图，逐条审核自然语言表述的忠实性、歧义性和正确性，随后在 Lean 中对这些陈述进行形式化并加以证明，同时参考 Mathlib、可选的领域库以及作者个人的工具包。只有作者最清楚某条陈述的真实意图，以及如何最佳地填补某一结论中的形式化缺口。因此，该流水线会在必要时暂停，并向作者提出相关问题。