🤖 AI

Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge

本文提出了一种关系桥接数据库和论文级形式化评分，旨在将文献元数据与形式化证明制品相连接，目标是将数学文献与机器可验证证明统一为一种可扩展的、机器可操作的知识图谱。

原作者： A. Mayeux

发布于 2026-06-11

📖 1 分钟阅读☕ 轻松阅读

原作者： A. Mayeux

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下数学的世界是一个巨大的图书馆，但它被分成了两个完全独立的侧翼，彼此互不往来。

图书馆的两个侧翼

“人类”侧翼（文献数据库）： 这里存放着所有已发表的数学论文。可以把这些地方想象成 MathSciNet 或 zbMATH。它们就像是图书馆的卡片索引。它们会告诉你谁写了哪篇论文、何时发表、主题是什么以及谁引用了它。这是人类研究的记录，但其中的数学内容是用“人类语言”（文本和符号）编写的，只有人类才能阅读和理解。
“机器人”侧翼（形式化库）： 这里存放着“机器可验证”的数学。想想像 Lean's mathlib 这样的系统。在这里，数学家将他们的想法转化为严格的计算机代码。这就像是将一部小说翻译成一种编程语言，以便计算机可以检查每一个逻辑步骤是否 100% 正确。问题在于，这个侧翼是根据代码的构建方式进行组织的，而不是根据原始论文来进行组织的。

问题所在：缺失的桥梁

目前，这两个侧翼是脱节的。如果你在“人类”侧翼找到了一篇著名的定理，文献目录并不会告诉你该定理是否已被翻译到“机器人”侧翼。反之，如果你在“机器人”侧翼看到一段代码，它也不会告诉你这段代码源自哪篇著名的论文。它们是同一片领土的两张不同的地图，但无法对齐。

解决方案：“桥梁层”

作者 Arnaud Mayeux 提议建立一座数字桥梁来连接这两个侧翼。这不是一个新的图书馆，而是一个连接器。

它的作用： 它将一篇来自“人类”侧翼的论文与其对应的“机器人”侧翼中的代码联系起来。
“形式化得分”（Formalization Score）： 为了使该系统发挥作用，系统会为每篇论文分配一个得分（从 0% 到 100%）。
- 100% 意味着计算机已经翻译并检查了该论文中的每一个定义、定理和证明。
- 50% 意味着其中一半的内容已被翻译。
- 0% 意味着这篇论文存在于人类世界，但机器人世界尚未触及它。

他们是如何测试的（“AI 翻译员”实验）

为了观察这座桥梁是否真的可以建成，作者使用人工智能（具体来说是一个名为 Google Gemini 的大语言模型）进行了一项小型实验。

他们给 AI 提供关于几篇不同数学论文的两份文档：

原始的人类论文（PDF 1）。
对应的计算机代码或文档（PDF 2）。

AI 被要求扮演一名严谨的图书管理员：

第一步： 计算人类论文中的每一个数学主张（例如“定理 A”、“定义 B”、“猜想 C”）。
第二步： 检查计算机代码，看是否存在该特定主张。
- 如果只是一个定义，代码需要包含该定义。
- 如果是一个定理，代码则既需要该定义，也需要其证明。
第三步： 计算百分比。

实验结果

AI 成功地为几个真实的案例计算出了这些得分：

球堆积（8 维）： AI 发现计算机代码覆盖了人类论文的 100%。（完美匹配）。
ζ(3) 的无理性： AI 发现匹配度为 50%。（一半的工作已完成）。
代数磁性（Algebraic Magnetism）： AI 发现为 0%。人类论文确实存在，但计算机代码与之完全无关。

为什么这很重要（根据论文所述）

论文认为这种系统是可行的。它并不试图取代人类审稿人或计算机检查器。相反，它充当了一个索引或目录，它会说：“嘿，如果你正在阅读这篇论文，这里是它与已被计算机检查的部分之间的链接，以及检查完成度的得分。”

局限性

作者诚实地指出了其缺陷：

阅读 PDF 很困难： 计算机很难从 PDF 中读取数学内容，因为 PDF 只是文本的图像，而不是结构化的事实列表。
AI 并非完美： AI 有时可能会在判断一段代码是否匹配某段文本时产生误判。
这是一个“尽力而为”的系统： 它不是一个完美的、神奇的地图。它是一个工具，旨在帮助研究人员根据当前可用的最佳数据，了解哪些部分已经形式化，哪些部分尚未形式化。

简而言之，该论文提出了一个评分系统，通过将人类数学论文与其计算机检查版本相连，并利用 AI 来协助统计已完成的工作量。

技术摘要：构建文献计量学与形式化数学知识之间的桥接层

问题陈述
现代数学知识目前分散在两个结构独立的基础设施中。一方面是文献数据库，如 MathSciNet 和 zbMATH Open，它们索引了人类可读的研究记录，捕捉了出版元数据、引用网络和专家评审。另一方面是形式化证明库（例如 Lean 的 mathlib）和交互式定理证明器（ITP），它们将机器可验证的数学编码为形式化检查的对象。虽然这些生态系统具有互补性，但它们仍然是脱节的：文献系统并不指示研究结果是否已被形式化，而形式化库则是围绕内部依赖图而非出版元数据进行组织的。尽管存在“对齐人工制品”（如综述论文或文档）来将经典结果映射到机械化进展，但这些映射是碎片化的、非标准化的，并且没有系统地集成到可查询的层级中。

方法论
本文提出了一种关系型桥接数据库，旨在集成这些现有的基础设施，而非取代它们。其核心方法论包含三个组成部分：

架构集成： 该系统作为一个对齐基础设施，将文献记录（来自 MathSciNet 和 zbMATH Open）与形式化人工制品（来自 Lean、Reservoir 等）联系起来。它不进行新的同行评审或形式化验证，而是作为一个存档平台，记录出版物与形式化代码之间的对应关系。
形式化评分 ( $S(P_i)$ )： 作者定义了一个定量指标，用于衡量特定论文 $P_i$ $P_{i}$ 的形式化程度。
- 将论文视为数学陈述 $S_i$ （定义、引理、定理、猜想等）的集合。
- 为每个陈述 $s$ 分配一个二元指示函数 $\phi(s)$ ：若 $s$ 在 Lean 中已完全形式化，则为 1；否则为 0。
- 要求区分：
  - 纯陈述（定义、构造、猜想）仅要求形式化对象的存在。
  - 已证陈述（定理、引理）则要求同时具备形式化陈述和完整的形式化证明。
- 评分计算公式为： $S(P_i) = 100 \cdot \frac{\sum_{s \in S_i} \phi(s)}{|S_i|}$ 。
通过跨文档对齐进行的可行性研究： 为了证明这些评分可以在大规模范围内进行估算，作者利用大语言模型（LLM）在零样本（zero-shot）设置下进行了实验。模型被要求对比非形式化数学论文（PDF 1）与形式化文档或 Lean 实现（PDF 2）。模型被指令执行以下操作：
- 从非形式化文本中提取细粒度的数学陈述。
- 将其分类为“纯陈述（Pure）”或“已证陈述（Proved）”。
- 识别形式化文本中的语义对应关系。
- 基于匹配陈述的比例计算形式化评分。

主要贡献

互操作层： 提出了一种数据库方案，旨在统一文献注册表与形式化验证环境，将出版元数据链接至形式化代码库。
形式化评分定义： 一种严谨的论文级指标 ( $S(P_i)$ )，用于量化出版物在形式化系统中的覆盖范围，并区分了定义的存在与证明的存在。
可行性演示： 通过概念验证研究表明，LLM 可以成功估算这些评分，通过将非形式化文本与形式化人工制品进行对齐，从而实现对形式化覆盖范围的大规模分析。

实验结果
作者使用 Google Gemini 在未经微调的情况下对六篇数学论文进行了实验。结果展示了系统区分不同形式化程度的能力：

高覆盖率： 8 维球堆积问题获得了 100 分，表明已完全形式化。
部分覆盖： 关于 $\zeta(3)$ 无理性的论文和关于多分次 Proj 方案的论文分别获得了 50 和 67.74（以及在第二次实验中的 96.30）的分数，反映了实质性但未完成的形式化。
低/无覆盖： 一篇关于“范畴的扩张（Dilatations of categories）”的论文获得了 41.67，而一篇关于“代数磁性（Algebraic magnetism）”的综述（其没有对应的 Lean 实现）在与无关文档匹配时获得了 0 分。
实验证实，模型能够正确识别不存在相关形式化的情况，并能区分完全形式化与部分形式化的著作。

意义与主张
本文将这项工作定位为将文献计量学与形式化数学生态系统整合为可扩展、机器可操作知识图谱的第一步。作者明确指出，所提出的系统并非现有出版或验证基础设施的替代品。相反，它作为一个“连接层”，将现有的、非结构化的对齐知识系统化为一种结构化的、可查询的资源。

其意义在于能够：

提供对已发表结果及其形式化对应物的统一访问。
实现对数学文献中有多少内容已被形式化进行大规模分析。
为将出版物链接到形式化证明对象奠定基础，从而可能支持未来的 AI 生成数学及人机协作工作流。

作者承认了局限性，指出 PDF 解析会引入歧义，检索质量会影响评分准确性，且 LLM 可能会产生伪造的对应关系。因此，他们将该系统框架化为一个用于关系对齐的“尽力而为（best-effort）的框架”，而非完美的映射，并预期超链接和映射最终将通过人工策展或类似于当前文献计量实践的有监督过程来进行处理。

技术摘要：构建文献计量学与形式化数学知识之间的桥接层

类似论文