arxiv.org·2026/10/26
为什么重要 提供作者在环的 Lean 形式化管线，逐条审计论文陈述并形式化证明，支持共享 Lean 代码，可提升数学证明类研究的稳健性。
即使经过仔细校对，论文的证明或陈述假设中仍可能留下小漏洞。我们介绍 PaperFormalizer，一个基于 Lean 的智能体管线，帮助作者发现并弥合自己论文中的此类漏洞，并将每篇论文转化为经过 Lean 验证的版本。PaperFormalizer 从 LaTeX 源码开始，将论文转录为陈述的依赖图，用自然语言审计每条陈述的忠实性、歧义性和正确性，然后在 Lean 中针对 Mathlib、可选的领域库和作者的个人工具集对陈述进行形式化并证明。
只有作者知道陈述的本意，以及结果中的形式化漏洞最好如何修复。因此，当某条陈述有不止一种解读时，管线会停下来询问作者；它以自然语言和 TeX 符号呈现每一项修复，作为作者可以接受、拒绝或重定向的提案，并且把可能改变论文主张内容的每一项决定都留给作者。输出包括论文的注释和修订版本、变更报告，以及 Lean 代码，其中每个声明都链接到它所形式化的陈述。随着更多论文被形式化，作者的工具集不断增长，作者可以分享他们验证过的论文，使后续研究者能够复用他们的 Lean 代码。通过使验证过的论文可实际产出，PaperFormalizer 旨在让依赖数学证明的研究更加稳健。PaperFormalizer 在编码智能体（Claude Code 或 Codex）内运行，可在 https://github.com/Jiyuan-Tan/PaperFormalizer 获取。用户分享的带 Lean 代码的论文可在 https://paperformalizer.org 获取。
Even a carefully proofread paper can leave small gaps in its proofs or its stated assumptions.
We introduce PaperFormalizer, a Lean-based agentic pipeline that helps authors find and close such gaps in their own papers and turn each paper into a Lean-verified version.
Starting from the LaTeX source, PaperFormalizer transcribes the paper into a dependency graph of statements, audits each statement in natural language for faithfulness, ambiguity and correctness, and then formalizes and proves the statements in Lean against Mathlib, optional domain libraries and the author's personal toolkit.
Only the author knows what a statement is meant to say and how a formalization gap in a result is best fixed.
The pipeline therefore stops and asks the author whenever a statement admits more than one reading, presents every repair, in natural language and TeX symbols, as a proposal that the author can accept, decline or redirect, and leaves to the author every decision that could potentially change what the paper claims.
The output is an annotated and revised version of the paper, a report of the changes, and Lean code in which each declaration is linked to the statement it formalizes.
The author's toolkit grows as more papers are formalized, and authors can share their verified papers so that researchers who build on them can reuse their Lean code.
By making verified papers practical to produce, PaperFormalizer aims to make research that rests on mathematical proofs more robust.
PaperFormalizer runs inside a coding agent (Claude Code or Codex) and is available at https://github.com/Jiyuan-Tan/PaperFormalizer.
Papers with Lean code shared by users are available at https://paperformalizer.org.
原版排版与图表 · 手机无法内嵌时可在浏览器打开。PDF 插件内选文不能传给网页助手。