PaperFormalizer：作者参与式的研究论文 Lean 自动形式化

事件

PaperFormalizer 是一个基于 Lean 的智能体流水线，目标是帮助作者在自己论文中找出并修补证明或假设陈述上的细小缺口，最终把论文转成经 Lean 验证的版本。它从 LaTeX 源码出发，把论文转写为陈述之间的依赖图，先用自然语言逐条审查陈述的忠实性、歧义与正确性，再针对 Mathlib、可选领域库和作者个人工具库完成形式化与证明。

该流水线强调作者始终在环：只有作者清楚某条陈述真正想表达什么、某个结果的形式化缺口该如何修补。因此当一条陈述存在多种读法时，流程会停下来询问作者；每一处修复都以自然语言和 TeX 符号的形式作为提案呈现，作者可以接受、拒绝或改向；任何可能改变论文主张的决策都留给作者。最终产出包括带注释和修订的论文版本、变更报告，以及每条声明都链接到其所形式化陈述的 Lean 代码。

随着更多论文被形式化，作者的个人工具库会不断扩充，作者也可共享已验证论文，让后续研究者复用其 Lean 代码。该工具运行在 Claude Code 或 Codex 等编码智能体内，代码已在 GitHub 开源，用户共享 Lean 代码的论文可在 paperformalizer.org 查看。其意义在于让经过验证的论文变得可实际生产，从而增强依赖数学证明的研究的稳健性。

来源

本条目由采集管线自动抓取并发布，完整内容见下方来源链接。

*采集源：arXiv cs.AI*