arXiv cs.AI· Jiyuan Tan, Vasilis Syrgkanis, Jose Blanchet·· 11 小时前AI 评分38
PaperFormalizer：作者参与式的 Lean 论文自动形式化工具
PaperFormalizer: Author-in-the-Loop Autoformalization of Research Papers in Lean
AI 导读
PaperFormalizer 是一个基于 Lean 的智能体流水线，可将论文从 LaTeX 源码转成依赖图并逐条审计、形式化与证明，最终产出经 Lean 验证的论文版本。它运行在 Claude Code 或 Codex 等编码智能体中，遇到歧义或可能改变论文主张的决策时会停下来交由作者确认，并输出修改报告及与声明对应的 Lean 代码。作者可共享已验证论文，供后续研究者复用其 Lean 代码。
正文 · AI 翻译
摘要：即使是经过仔细校对的论文，其证明或所述假设中也可能留下细小的缺口。我们推出 PaperFormalizer，一个基于 Lean 的智能体流水线，帮助作者发现并弥补自己论文中的此类缺口，并将每篇论文转化为经 Lean 验证的版本。PaperFormalizer 从 LaTeX 源文件出发，将论文转写为陈述之间的依赖图，用自然语言审查每条陈述的忠实性、歧义与正确性，然后在 Lean 中针对 Mathlib、可选的领域库以及作者的个人工具包对陈述进行形式化并证明。只有作者才知道一条陈述究竟想表达什么，以及某个结果中的形式化缺口最好如何修复。因此，只要某条陈述存在不止一种解读，该流水线就会停下来询问作者；它会以自然语言和 TeX 符号呈现每一种修复方案，作为作者可以接受、拒绝或改向的提议，并把所有可能改变论文主张的决定都留给作者。输出包括：论文的批注修订版、变更报告，以及 Lean 代码——其中每个声明都链接到它所形式化的陈述。随着更多论文被形式化，作者的工具包会不断扩充；作者还可以分享自己已验证的论文，使在其基础上开展研究的研究者能够复用其 Lean 代码。通过让已验证论文的产出变得切实可行，PaperFormalizer 旨在让依赖数学证明的研究更加稳健。PaperFormalizer 运行于编码智能体（Claude Code 或 Codex）之中，可在 此 https URL 获取。用户分享的带 Lean 代码的论文可在 此 https URL 获取。
| 主题： | 人工智能（cs.AI）；计算机科学中的逻辑（cs.LO） |
| 引用为： | arXiv:2610.31810 [cs.AI] |
| （或本版本的 arXiv:2610.31810v1 [cs.AI]） | |
| https://doi.org/10.48550/arXiv.2610.31810 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Jiyuan Tan [查看邮箱]
[v1]
2026年10月22日 星期四 18:46:53 UTC（1,452 KB）
来源：arXiv cs.AI · arxiv.org