当 Lean 验证你的论文：PaperFormalizer 如何让数学证明不再有"小漏洞"
一个被忽略的边界条件
想象你刚写完一篇统计学习理论的论文。证明里有 29 个引理、定理、推论。你反复校对，合作者也查了三遍。你提交了。几个月后，一个博士生在复现你的 Lemma A.2 时发现：你的采样项速率 \(t^{\beta/2} n^{-1/2}\) 需要有界方差，而你的假设里根本没给这个条件。在对称稳定噪声指数 3/2 的情形下，你的误差界是 \(n^{-2/15}\)，而你论文里写的是 \(n^{-1/5}\)——你声称的界，成立的概率趋于零。
这不是假设性场景。这是 Jiyuan Tan、Vasilis Syrgkanis 和 Jose Blanchet 在斯坦福用 PaperFormalizer 验证自己论文时真实发现的问题。
PaperFormalizer 想做的事情听起来简单：把你的 LaTeX 论文变成 Lean 验证过的版本。但它的设计哲学比这复杂得多——它不打算替你做决定，它打算帮你发现你没想到要检查的地方。
论文不是文本，是依赖图
PaperFormalizer 的第一步，是把论文从"一串文字"变成"一张图"。
传统校对是线性的：从头读到尾，找笔误。但论文的逻辑结构不是线性的——定义 2.1 被引理 3.1 用，引理 3.1 被定理 3.3 用，定理 3.3 被推论 3.4 用。一个早期定义的歧义，会沿着依赖链传播到所有下游结果。
所以 Stage 1 做的是转录：一个 agent 把 LaTeX 源码拆成节点（每个定义、假设、引理、定理、推论、引用结果各一个节点），然后画边——每当一个陈述的证明用到另一个陈述，就加一条有向边。结果是一张依赖图，论文的骨架架。
这个设计的关键洞察是：论文的错误不是均匀分布的，它们沿着依赖链聚集。Proposition 3.3 错了，所有依赖它的定理、推论都继承了这个错误。PaperFormalizer 的案例研究里，7 个结果中 5 个需要修改，全部追溯到两个根源：Proposition 3.3 和 Lemma A.1。
三轴审计：忠实性、歧义性、正确性
Stage 2 是自然语言审查。一个 reviewer agent 沿依赖图的拓扑序逐个检查每个节点，沿三个轴：
忠实性：这个节点真的匹配论文里写的吗？转录 agent 有没有把 \(\alpha\) 和 \(\beta\) 搞混？
歧义性：这个陈述只有一种合理读法吗？"homogeneity inequality holds for both treatments"——是同时成立还是分别成立？
正确性：这个陈述成立吗？它的证明真的建立了这个陈述吗？
第三个轴最关键。reviewer 只在能在论文的设定内找到反例时，才报告一个结果"错误"。如果反例都是退化的边界情况（零方差、空类），reviewer 不说"错了"，而是加一个侧条件。
这个设计很精妙：大部分论文的"错误"不是逻辑断裂，而是缺少正则性条件。作者心里默认排除了退化情形，但没写出来。Lean 不会让你含糊——要么陈述包含这个条件，要么证明过不了。
作者在环：不替你做决定
这是 PaperFormalizer 和其他自动形式化系统最大的区别。
当一条陈述有多种读法时，agent 不会猜。它停下来，在本地网页上用自然语言和 TeX 符号呈现每种读法，等作者选。当一条修复会实质性改变主要结果时，agent 不会自动应用——它把提案给作者，作者可以接受、拒绝、或者让 fixer 换个方向试。
被保留给作者的决定有四类： 1. 会实质性改变主要结果的修复 2. 任何会让主要结果与印刷版实质不同的裁决 3. 把结果提升到个人工具包 4. 是否分享论文
这四类决定的共同点是：它们改变论文声称了什么。agent 可以帮你发现漏洞、提议修复、写 Lean 代码，但它不替你决定你的论文说了什么。
这个边界很重要。一个自动修复系统如果替你改了主要定理的陈述，你可能会在不知情的情况下"发表"了一个你没打算声称的结果。PaperFormalizer 的设计原则是：agent 做苦力活，作者做语义决定。
修复提案：最小改动保住核心贡献
当 reviewer 发现 Proposition 3.3 的证明第一步就有问题时——它需要给定 \((X, U)\) 的外生性，但假设只给了给定 \(X\) 的外生性——fixer agent 不会建议重写整个定理。它提议加条件：\(\alpha < \beta\)、\(0 < p(X) < 1\)、条件均值外生性、有限条件尾均值。
这些条件都是证明里实际用到的。作者接受了，因为它们不改变论文的核心结论——极端处理效应的识别公式不变，只是加上了证明需要的正则性条件。
案例研究的数字很说明问题：
- 第一篇论文（极端事件处理效应）：7 个结果中 5 个需要修改
- 第二篇论文（最优传输）：12 个结果全部如印刷版成立
- 第三篇论文（神经因果模型）：29 个结果中 20 个证明成立，2 个被反驳且无法修复
六阶段流水线
完整的流水线是：
Stage 1（转录）：LaTeX → 依赖图。每个陈述一个节点，使用关系画边。
Stage 2（自然语言审查）：沿依赖序检查忠实性、歧义性、正确性。有歧义就问作者。有错误就提议修复。
Stage 3（规划）：对每个陈述决定——从 Mathlib/领域库/个人工具包复用，还是新形式化，还是保持引用。引用结果通常不形式化（太贵），作为显式假设进入 Lean 代码。
Stage 4（脚手架）：把所有计划形式化的陈述写成 Lean 语句，证明留空。编译。检查每个 Lean 陈述对应正确的自然语言陈述。
Stage 5（证明填充）：循环——worker 填证明，reviewer 检查忠实性，确认没有 sorry 和非标准公理。如果 Lean 工作显示论文陈述有误，回到 Stage 2 修复。
Stage 6（链接与报告）：每个 Lean 声明链接到论文中它形式化的陈述。输出：带注记的论文（原文红色、修改蓝色）、修订版论文、Lean 代码、变更报告。
个人工具包：每篇论文让下一篇更便宜
一个研究者通常在同一领域工作多年，跨论文复用相同的技术。PaperFormalizer 的个人工具包设计利用了这一点。
工具包分三层：
- 底层：只读基础库（Mathlib + 选定的领域库）
- 中层：可复用结果，分为 Foundations（基础库缺失的标准结果）和 Tricks（作者自己的可复用引理）
- 顶层：每篇形式化论文一个模块树
案例研究的 Lean 代码有 136 个文件、约 26,000 行，其中 13 个模块（约 2,500 行）来自作者工具包的 Foundations 层——Chernoff 界、事件条件化、Rényi 的指数序统计表示。这些是作者之前论文形式化时积累的，这次直接复用。
每篇论文让下一篇更便宜——这是 PaperFormalizer 的飞轮效应。作者还分享了验证过的论文，所以后来者可以从已验证的 Lean 代码起步，而不是从零开始。
两个模型家族的分工
PaperFormalizer 大部分角色跑在 OpenAI 的 gpt-6.1-sol 上（通过 Codex CLI），包括转录、fixer、reviewer、脚手架、证明填充。但 Lean 规划、最终 Lean 审查的第二独立 reviewer、以及工具包策展跑在 Claude Opus 上（通过 Claude Code CLI）。
用两个模型家族的关键原因是：规划和最终审查来自写 Lean 代码之外的模型。这是对抗模型同源偏差的设计——如果同一个模型写代码又审代码，它可能系统性地忽略自己的盲点。
当 Claude Code 不可用时，这些角色 fallback 到 gpt-6.1-sol 高推理强度。但论文明确说 pipeline 是在双模型配置下调优的，单模型路径还没在真实论文上跑过。
和其他系统的区别
已有工作分两类：
自然语言审查类（OSVerify、Rethlas-OSV）：审查论文数学的自然语言正确性，把审计过的发现交给人类专家。不做形式化。
自动形式化类（Rethlas、Archon、LeanMarathon、LeanFlow）：把非形式化论证或整篇论文形式化到 Lean 4。没有作者在环。
PaperFormalizer 在两者之间。它先做自然语言审查并提议修复，再形式化每个陈述，在陈述有多种读法或修复会改变主要结果时问作者。这个"中间位置"是它的核心贡献——纯自动形式化无法处理语义歧义，纯自然语言审查无法提供机器可验证的保证。
局限与诚实
论文很诚实地说明了局限：
- macOS 和全新 Windows 前置安装还没测过
- codex-only 路径（没有 Claude）还没在真实论文上跑过
- 运行时间长、token 消耗大，建议从短论文开始或用
--targets限制 - 领域库安装成本不低：Mathlib-only 约 8GB，加 Causalean 约 15GB，加 StatLean 约 19GB
这意味着什么
PaperFormalizer 不是一个"一键验证"工具。它是一个需要作者参与的协作系统——你需要在关键决策点做决定，你需要读 agent 的提案并判断是否符合你的意图。
但它的价值恰恰在这里：它把"形式化验证"从需要数周 Lean 专家工作的奢侈品，变成作者写论文时可以跑的常规步骤。不是一键完成，而是一下午的交互——agent 做苦力，你做决定。
更大的愿景是论文共享生态：作者分享验证过的论文和 Lean 代码，后来者复用这些代码作为起点。每篇被验证的论文都让同领域的下一篇更便宜。这不是单点工具，是一个累积性的基础设施。
当 Lean 验证变得和 LaTeX 排版一样常规时，数学证明的"小漏洞"就不再是不可避免的学术代价了。PaperFormalizer 不是终点，但它指向了一个方向：论文的数学正确性可以像代码的正确性一样被机器检查，而作者保持对内容的完全控制。
---
*论文：arXiv:2610.31810 · 代码：github.com/Jiyuan-Tan/PaperFormalizer · 共享论文：paperformalizer.org*