PaperFormalizer：在精益流程中实现研究论文的作者参与式自动形式化

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