超越正确性：迈向使用Lean 4的自动新颖性验证

# 使用 Lean 4 走向自动化新颖性验证
来源：https://arxiv.org/html/2608.14669

## 超越正确性：使用 Lean 4 走向自动化新颖性验证
Ayrton Porto  
布宜诺斯艾利斯省国立中域大学 (UNICEN)  
本研究独立完成。 [email protected]（2026年7月）

###### 摘要
应用于数学的人工智能系统验证正确性，但不验证新颖性：一个自动生成的定理可以在 Lean 中编译无误，却可能是一个已知的结果。本文介绍了 AViD Journal，这是一个流水线，它接收 LaTeX 文章，将其陈述在 Lean 4 中形式化，并通过一个三维决策树做出新颖性判定：维度包括形式化语料库（Mathlib）和非形式化语料库（TheoremSearch 和 Matlas，带时间过滤器和 LLM 判断器）中的先前存在性、通过自动策略判断的非平凡性，以及以前提集上的 Jaccard 距离衡量的证明间结构距离。在因声明重复而从 arXiv 撤回的论文上进行的评估，产生了一个比任何性能指标都更具启发性的结果：识别出了三个限制该方法的障碍，这些障碍与具体实现无关。首先，Lean 文件的成功编译并不能保证语义保真性。其次，召回率的上限是由定理索引的覆盖率决定的，而非相似度度量。第三，arXiv 在论文撤回时会移除源代码，这损害了任何基于这些论文构建的基准测试的可重复性。

*关键词：* 自动化定理证明、新颖性验证、Lean 4、Mathlib、语义搜索、证明距离、Jaccard 相似度、形式化数学

## 1 引言
First Proof 项目 [1 (https://arxiv.org/html/2608.14669#bib.bib1)]（其中十一位数学家贡献了未发表的研究问题）旨在将真正的推理与纯粹的文献搜索区分开来。其第二批由人类评审员评估 [2 (https://arxiv.org/html/2608.14669#bib.bib2)]，记录了应用于数学的语言模型的一种具体失败模式：当问题在结构上与已发表的结果相似时，系统表现更好，并且在多种情况下，它通过翻译文献中先前的证明来解决，甚至逐行复用其术语和符号，而不引用来源，以至于人类审稿人会将其标记为抄袭。那么，所缺乏的不是生成正确证明的能力，而是一种系统性的方法来评估一个证明是否真正是新的。模型可以生成能够编译、正确但并非新的陈述。这个问题是双重的。一方面，当前的数学AI系统（Axiom、Harmonic、DeepSeek-Prover）验证正确性但不验证新颖性。另一方面，将新颖性等同于不在 Mathlib [5 (https://arxiv.org/html/2608.14669#bib.bib5)] 中的天真标准在两个方向上都失败了：它将任何2026年的自动策略无需真正的数学思想就能证明的平凡定理标记为新，同时它会遗漏那些未形式化但在非形式文献中已发表的结果。陶哲轩 [4 (https://arxiv.org/html/2608.14669#bib.bib4)] 在其关于机器辅助证明的笔记中，从规模角度阐述了这个问题：形式化验证是劳动密集型的，以至于目前无法实时形式化相当比例的研究论文，而自动化辅助则有望实现当前无法达到的数学探索规模。陶哲轩将这一论点应用于*正确性*控制以及愿意逐行验证长证明的评审员稀缺性。我们认为，同样的论点也适用于*新颖性*控制：如果定理生成加速，手动评估每个结果是否真正新颖将变得像逐行验证一样不可行，而提出定理的一方本身就是一个模型。这个问题的紧迫性在本文写作过程中得到了说明。2026年7月，Anthropic 的数学家 Levent Alpöge 宣布了对雅可比猜想（自1939年Keller提出以来悬而未决）的一个明确反例，该反例在语言模型的协助下发现，且非常简短，其验证是基本的：几秒钟的符号计算，在几小时内独立地在 Lean 和 Isabelle 中针对预先注册的猜想陈述进行了形式化 [3 (https://arxiv.org/html/2608.14669#bib.bib3)]。该反例立即推广到所有维度 ≥3，并且在几天内，高维反例家族就在流传；这一事件也是更广泛的AI辅助反驳其他公开猜想浪潮的一部分。这样的事件以集中的形式产生了激发本工作的素材：源于同一发现的结果，由不同作者并行获得，其中某个陈述是否已被他人建立的问题是真实的，且手动回答成本高昂。此外，这正是我们在第 5.6 节 [https://arxiv.org/html/2608.14669#S5.SS6] 记录的覆盖限制不适用的情况：潜在重复的作品是同时代的，并且立即公开可用。

本文介绍了 AViD Journal（Automated Verification in Demonstrations），一个在操作层面上解决该问题的系统：它接收 LaTeX 文章，将其陈述在 Lean 4 中形式化，并通过一个三维决策树做出新颖性判定。

### 1.1 贡献
1.  一个完整的新颖性验证流水线。该系统遍历了从 LaTeX 源到判定的整个路径：数学环境的解析、使用多模型抽象在 Lean 4 中形式化，以及一个基于三个维度的八判定决策树：形式化语料库（Mathlib，通过 Leandex）和非形式化语料库（TheoremSearch 和 Matlas，带时间过滤器和 LLM 判断器）中的先前存在性、通过 Lean 自动策略判断的非平凡性，以及基于前提集 Jaccard 距离的证明间结构距离。
2.  一个因重复而被撤回论文的基准测试集。一个从 arXiv 撤回的论文数据集，其撤回说明声明了先前结果的重复，并带有按类别和年份匹配的对照组，以及对其重复者的可检索性分析。
3.  该方法失败模式的映射。评估的核心贡献不是性能指标，而是对三个障碍的刻画：(a) Lean 文件编译成功并不保证形式化忠于原始陈述；(b) 重复发现的结果往往早于预印本时代，因此对现有语料库不可见；(c) arXiv 在撤回论文时移除了 LaTeX 源，这限制了任何基于其构建的基准测试的可重复性。

### 1.2 文章结构
第 2 节 [https://arxiv.org/html/2608.14669#S2] 将本工作置于与新颖性验证相交的研究前沿中：陈述搜索基础设施、猜想生成中的新颖性过滤器、证明同一性，以及正确性与新颖性之间的区别。
第 3 节 [https://arxiv.org/html/2608.14669#S3] 描述流水线：解析器、形式化、参考语料库、三个维度和判定树。
第 4 节 [https://arxiv.org/html/2608.14669#S4] 单独验证每个工具。
第 5 节 [https://arxiv.org/html/2608.14669#S5] 报告在撤回论文上的评估，并刻画发现的失败模式。
第 6 节 [https://arxiv.org/html/2608.14669#S6] 以已构建的内容、剩余限制和未来工作作为结束。

## 2 相关工作
### 2.1 定理搜索引擎和基础设施
TheoremSearch [6 (https://arxiv.org/html/2608.14669#bib.bib6)] 索引了从 arXiv 和另外七个来源提取的 920 万条陈述，用简短的自然语言描述表示每个定理以进行嵌入，并公开无需认证的 API。其文档记录的动机（因重复而撤回的 arXiv 论文）与我们使用撤回论文进行实验的动机相同。TheoremSearch 找到相似陈述；AViD 添加了判定层。
Matlas [10 (https://arxiv.org/html/2608.14669#bib.bib10)] 从 1826 年至 2025 年的 435,000 篇同行评审文章中提取了 807 万条陈述，来源包括根据 ICM 引用标准选择的 180 种期刊，以及 1,900 本教科书。这两个来源在时间覆盖上是互补的：TheoremSearch 涵盖 1991 年以来的 arXiv，Matlas 涵盖 1826 年以来的同行评审期刊。AViD 将它们作为其非形式化语料库的两个分支消费，第 5 节 [https://arxiv.org/html/2608.14669#S5] 报告了这种组合覆盖的范围。
Mathlib 搜索引擎领域已经饱和。Leandex [21 (https://arxiv.org/html/2608.14669#bib.bib21)]，Project Numina 的语义搜索引擎，提供对 Lean 4 声明的搜索；Lean Finder [22 (https://arxiv.org/html/2608.14669#bib.bib22)] 将用户意图纳入对 Mathlib 的语义搜索。AViD 并非在该领域竞争：它消费其中之一作为基础设施（Leandex 是 D1 CF 的后端），并添加了这些工具均未提供的判定层。
一篇关于数学 AI 的最新综述 [17 (https://arxiv.org/html/2608.14669#bib.bib17)] 将陈述搜索引擎列为定位已建立定理的基础设施，这将 AViD 所解决的问题定位为该领域认可的问题。
两项近期工作作为基础设施相关，而非竞争对手。TheoremGraph [7 (https://arxiv.org/html/2608.14669#bib.bib7)] 构建了一个陈述级依赖图，统一了非形式化（来自 arXiv 的 1170 万个定理类环境）和形式化（LeanGraph，388,105 个 Lean 4 节点）；我们评估了使用其图依赖关系来衡量 D3 中证明间的距离，但最终还是采用了每个证明的直接前提集。在一个互补的方向上，COMPOSE [8 (https://arxiv.org/html/2608.14669#bib.bib8)] 通过结合文章的引用图和 Mathlib 的形式化依赖关系来预测合理的未来陈述，生成猜想而非裁决其新颖性。

### 2.2 猜想生成中的新颖性过滤器
LeanConjecturer [9 (https://arxiv.org/html/2608.14669#bib.bib9)] 使用 `exact?` 针对 Mathlib 过滤新颖性，并使用 `aesop` 过滤非平凡性：它从 40 个种子文件生成了 12,289 个猜想，其中 3,776 个被证明是语法有效且非平凡的。这些正是 AViD 作为 D1（`exact?` 作为 CF 的回退）和 D2（在 `T_AUTO` 中的 `aesop`）所实现的机制。AViD 的贡献并非发明这些过滤器，而是将它们组合成一个发布判定的决策树，添加 D3 和带时间过滤器的非形式化分支，并基于外部基准事实对其进行评估。
关于修剪冗余猜想 [15 (https://arxiv.org/html/2608.14669#bib.bib15)] 和通过前向推理进行合成生成 [16 (https://arxiv.org/html/2608.14669#bib.bib16)] 的工作，从生成角度说明了同样的需求。

### 2.3 证明同一性与相似性
AViD 在 D3 中使用的基于前提集的 Jaccard 距离，其表示方式借鉴了前提选择文献，其中定理由其证明的前提来表征：MaSh [23 (https://arxiv.org/html/2608.14669#bib.bib23)]、Kaliszyk 和 Urban [24 (https://arxiv.org/html/2608.14669#bib.bib24)] 使用 IDF 加权 k-NN，以及 Magnushammer [12 (https://arxiv.org/html/2608.14669#bib.bib12)] 使用变换器。但任务是相反的：那些系统是*选择*前提来从陈述构建证明，而 D3 使用*已使用*的前提集作为指纹来比较已完成的证明。唯一直接继承的组件是过滤：Piotrowski 等人 [13 (https://arxiv.org/html/2608.14669#bib.bib13)] 的 `math_filter`，它使用 Mathlib 名称作为白名单来丢弃技术引理，这与 D3 的 Jaccard 之前应用的过滤器是相同的配方。
Li 等人 [20 (https://arxiv.org/html/2608.14669#bib.bib20)] 对 Mathlib 网络的分析（基于 308,129 个声明和 840 万条边的图）表明，该库中被引用最多的引理是技术性基础而非深层数学：等式自反性（`Eq.refl`）是入度第二高的节点，有 69,580 次引用，而中国剩余定理甚至没有出现在前一百名中。也就是说，图中的中心度衡量的是一个引理的普遍程度，而非其数学内容的贡献。这证明了 D3 的过滤器 1 是合理的：在计算两个证明之间的 Jaccard 之前，AViD 丢弃来自 `Init.` 和 `Lean.` 命名空间的前提，这些恰恰是那些无处不在的技术引理。如果没有过滤器，两个证明仅因共享语言的基本机制而显得相似；有了过滤器，Jaccard 反映了真正区分数学内容的前提。
Yoo [11 (https://arxiv.org/html/2608.14669#bib.bib11)] 将定理表示为基于公理系统的证明向量，并使用余弦、欧氏或 Jaccard 相似度进行比较。这是在概念工具上最接近的工作，但目的相反：Atlas 根据结构相似性组织定理；AViD 使用这种相似性来决定一个证明是否冗余。Huch [14 (https://arxiv.org/html/2608.14669#bib.bib14)] 记录了 AFP 中无标度的入度分布，这对于未来使用 IDF 加权前提的工作很重要。

### 2.4 正确性与新颖性
现有的论文转 Lean 流水线验证证明是正确的，而非新的；新颖性验证委托给人工评审员。AViD 明确是那个被委托的层。一个完整的自动审查系统需要这两个维度，第 5 节 [https://arxiv.org/html/2608.14669#S5] 表明第一个不是第二个的充分条件：一个 Lean 文件可以无误编译，却并非原始陈述的忠实形式化。

### 2.5 定位
表 1：AViD 相对于先前工作的定位。先前工作构建基础设施模块；AViD 将它们组合成一个从 LaTeX 源到判定的流水线。  
*注：D3 已独立实现并验证（第 4 节 [https://arxiv.org/html/2608.14669#S4]），但在报告的实验中未在决策树中执行。差异不在于任何单个单元格，而在于组合：先前工作构建基础设施模块——搜索、形式化、相似性——；AViD 将它们组装成一个接收 LaTeX 论文并返回判定的流水线。

## 3 AViD 流水线
该系统接收一个 `.tex` 文件，提取其数学块，在 Lean 4 中形式化它们，并应用一个三维决策树来做出新颖性判定。本节详细描述每个阶段，以提供概念复制所需的细节。

### 3.1 LaTeX 摄取与解析
解析器从 LaTeX 源中提取数学环境：`theorem`、`lemma`、`proposition`、`corollary`、`definition` 及其西班牙语变体（`teorema`、`lema`、`proposición`、`definición`、`corolario`）。它也识别通过 `\newtheorem` 和 `\theoremstyle` 定义的缩写变体（`thm`、`lem`、`prop`、`cor`、`defn`）和用户定义环境。块之间的依赖关系从交叉引用 `\ref{}` 和 `\cite{}` 中提取。解析器用它们构建一个有向无环图并应用拓扑排序（Kahn 算法）来确定形式化顺序：没有依赖的块先处理；依赖于其他块的，随后处理。
并非所有检测到的环境都进入下一阶段。编排器只形式化被认为是可形式化的类型：`theorem`、`lemma`、`proposition`、`corollary` 及其变体。诸如 `remark`、`example`、`proof` 和 `definition`（当不作为依赖所需时）等环境虽被提取但