用证明助手逐条核对统计论文

统计学论文靠长证明撑结论，真正逐行读过的人寥寥无几。10 月 26 日发布的一套开源工具，让机器来干这件事，而且已经在真实论文里抓出了后来被官方勘误确认的错误。

一、发生了什么

两位作者发布的这套工具，名字缩写里带着「用证明助手核对论文」的意思，组织一组由命令行编程助手驱动的模型智能体，把一篇论文的证明逐条翻译进 Lean 4 证明助手及其数学库，再在那里逐个验证。

设计上有几处很克制。每个编号结论只给四种判定之一：无条件成立、附带命名的假设条件成立、记录问题（写明位置和责任在哪一侧）、或者未完成及原因。四种里最有价值的是第二种：把用到的未证明前提逐条列成命名假设，等于直接告诉作者「你的结论靠这些没检验过的东西撑着」。智能体必须顺着论文自己的证明走，不许另起炉灶找新证明；写和审由不同智能体分任；每条陈述先与原文比对再证，证完留指纹；每个判定背后是可以脱离模型重跑的证据。整套流程能无人值守跑几小时，撞上用量上限会等待，修订后只重查改动部分，成本按角色、模型、结论分项上报。

补一点背景，这是背景，不是论文结论：Lean 证明助手及其数学库这几年成了形式化数学的主阵地，社区已经把大量经典定理搬了进去。但此前的工作多为逐个定理攻坚，把散落在论文里的完整证明批量搬进去核对，这套工具做到了前所未有的完成度。

实战结果最有说服力：先在四篇带标准答案的示例论文上验证流程，再盲测三篇已发表的统计学论文——用它们公开勘误之前的版本。三篇里，工具都在勘误声明所指的那一步找到了已发表的错误，还额外揪出一些经人工确认的新问题。对照组里，同一个模型直接面对论文加证明助手，最长的一篇判定正确率更低，还把几条比原文更窄的陈述误报为已证；而这套工具的每个判定都没有超出其证明证据的范围。

二、跟你有什么关系

审稿人和期刊编辑：机器核不了论文的意义，但能核证明的每一步，把它当一道新增工序，比多找一个审稿人可靠。

写论文的：先让工具过一遍你的证明，勘误级错误在投稿前被逮住，代价小得多。

做学术诚信工具的：判定必须落在可重跑的证据上，这条设计原则比堆模型更值钱。

三、怎么用

1. 把论文源码交给工具，让它先出四类判定清单，人工只审「条件成立」和「记录问题」两类。
2. 对照勘误历史测一回工具，确认它能在正确步骤报警，再信它的安静。
3. 记住边界：它核的是证明对不对，不是假设合不合理、数据真不真。

四、三个别信的说法

模型直接配证明助手就够了。 对照实验显示，缺了流程约束，模型会漏判、会把窄陈述报成全称，组织方式本身就是能力。

通过编译就等于正确。 编译器只保证逻辑闭合，陈述是否忠实于论文原意，仍需比对环节把关。

这种工具离实用还远。 三篇真实论文的盲测已经对上了勘误结论，至少在统计学领域它已可用。

五、一句话结论

证明没人读的时代，让机器先读一遍。

信息来源

• 用证明助手与智能体核对统计论文证明的开源工具（arXiv 摘要），2026 年 10 月 26 日提交

功能与价格以官方公告为准。本文写于 2026 年 10 月 28 日。