Jordan Curve Theorem 的再形式化

# 若尔当曲线定理的重新形式化
来源：https://arxiv.org/html/2607.01734
###### 摘要

我们提出了一个*重新形式化*的案例研究，这是自动形式化的一种变体，其中输入证明不是自然语言，而是来自不同证明助手的现有形式化开发。具体来说，我们报告了若尔当曲线定理的三个重新形式化：从 Mizar 到 Lean、从 HOL Light 到 Lean、以及从 HOL Light 到 Agda。我们分析了结果，并指出了对实际重新形式化任务重要的流程设计选择。最终的正式化成果可在 https://github.com/epfl-lara/jordan-curve-theorem 获取。

关键词

## 1 引言

自动形式化问题备受关注：给定自然语言（如论文或教科书）形式的数学文本，在证明助手中生成相应的形式化。而另一个更简单但同样非常有用的问题——不是从非形式化证明，而是从另一个证明助手的现有形式化开发来形式化一个数学理论——受到的关注则少得多。我们将此任务称为*重新形式化*。

跨证明系统的自动证明迁移一直是 ITP 社区的一个研究课题（Kohlhase 和 Rabe, 2021（https://arxiv.org/html/2607.01734#bib.bib297）; Anonymous, 1994（https://arxiv.org/html/2607.01734#bib.bib14））。在 LLM 在形式化数学领域取得最新进展之前，主要可行的方法是语句和证明的低级逻辑翻译。多年来，人们提出了许多方法，但它们面临两个基本障碍。首先，逻辑基础（例如，依赖类型理论、高阶逻辑或集合论）之间的不匹配难以克服。即使逻辑基础可证明是等价的，现有方法通常也仅限于基础非常相似的系统之间的迁移、从较简单系统到较复杂系统的迁移（例如，（Blanqui, 2024（https://arxiv.org/html/2607.01734#bib.bib65）; Keller 和 Werner, 2010（https://arxiv.org/html/2607.01734#bib.bib293））），或者像 Guilloud 等人 (2024)（https://arxiv.org/html/2607.01734#bib.bib241） 那样具有较大复杂度和证明规模开销的翻译。

第二个障碍是，即使技术上可行，生成的翻译也不自然。特别是，某个概念的翻译往往与目标助手中该概念的定义方式不匹配。这就是*库对齐*问题。例如，将 HOL Light 证明迁移到 Lean 时，HOL Light 中自然数N\\mathbb\{N\} 的定义在迁移到 Lean 后，其对 N\\mathbb\{N\} 的定义不仅与 Lean 的归纳类型 N\\mathbb\{N\} 不同，甚至可能无法在 Lean 中证明与之等价。通常的解决方法是手动对齐概念，但这会将每个被翻译概念的使用限制在特定的 API 上。

然而，在数学研究中，除少数特殊领域外，人们普遍认为逻辑基础的具体选择影响不大：原则上，只要背景足够，任何证明系统都可以“自然地”进行数学证明。就此而言，上述两个问题是那些必须确定性、完备且构造正确，但无法保留原始证明精神的翻译的产物。基于 LLM 的证明迁移则相反：它不是确定性、完备或构造正确的，但可以保留证明思路，从而在很大程度上避免上述两个障碍。这就是*重新形式化*背后的基本原理。

在本文中，我们通过一个案例研究表明，合适的智能体流程结合大型语言模型可以将大型数学形式化开发迁移到完全不同逻辑基础的证明助手中。具体来说，我们以若尔当曲线定理（JCT）为主要研究对象。JCT 指出，任何不自交的闭曲线将平面R2\\mathbb\{R\}^\{2\} 分成两个不相交的区域——一个有界内部和一个无界外部——并于 1887 年由 Camille Jordan 证明。这是一个著名的例子，证明看似显然，实际却冗长且技术性强，并且具有重要的应用。

JCT 的首次形式化于 2005 年由 Hales (hales2007jordan) 在 HOL Light 证明助手（Harrison, 2009（https://arxiv.org/html/2607.01734#bib.bib258））中完成，证明大约有 60,000 行。同年，一个国际团队在 Mizar 证明助手（kornilowicz2007proof）中完成了该定理的另一个形式化。Mizar 中对 JCT 的证明工作历时 14 年，由于该问题的吸引力和从事此工作的人倾向于消失，它被描述为一个黑洞，形式化数学家掉进去就再也看不到了。尽管 Hales 更快，但他仍然描述其形式化工作花费了“数月艰苦努力”。以现成的形式化证明为基线，手动将证明移植到不同的证明助手所需时间会更少，也许是“几个”月的艰苦工作。相比之下，本案例研究中的重新形式化在一周内产生了 JCT 的形式化，主动人工参与时间不超过两天，并且使用了商用 LLM。这表明，大规模实用的证明迁移现已可行。

在论文的其余部分，我们介绍了 JCT 的三个重新形式化：从 Mizar 到 Lean、从 HOL Light 到 Lean、以及从 HOL Light 到 Agda。选择 Lean（de Moura 等人, 2015（https://arxiv.org/html/2607.01734#bib.bib158））是因为其完善的工具生态系统和 Mathlib (mathlib2020) 库；选择 Agda (Norell2007) 是因为它是一个逻辑基础相似但工具相对不够完善的证明助手的例子，以测试证明助手的生态系统的影响。对于每个案例，我们介绍流程并报告影响智能体性能的设计选择。然后，我们比较这三个重新形式化，以评估源和目标证明助手的逻辑基础及工具对实际重新形式化的影响程度。

## 2 重新形式化任务与评估设置

我们使用术语*重新形式化*表示以下任务：给定一个建立命题TT 的现有形式化开发，在一个不同的目标证明助手中生成一个新的、可独立校验的形式化开发，以建立相应的命题T′T^\{\\prime\}。与构造正确的证明翻译不同，我们的目标不是保留源语法、证明项或定义相等性，而是在目标助手中恢复一个在数学上忠实于源、在目标助手中惯用的证明开发。因此，源形式化不被视为要编译的对象，而是作为定理的精确规范和高度详细、保证正确的证明。基于 LLM 的智能体使用此规范，结合目标助手的库、搜索工具和验证循环，为目标证明系统构建原生的开发。

#### 任务范围。

我们的案例研究侧重于若尔当曲线定理及其支撑基础设施。这是重新形式化的一个有用压力测试，原因有三。首先，该定理的表述只需要实数和连续函数，因此可以直接在我们考虑的所有助手中表述。其次，证明开发规模大且技术上异构，混合了拓扑、几何、图论论证和分析引理。第三，在多个助手中存在成熟的源形式化，允许我们比较不同源语言和库之间的重新形式化。

对于每个案例研究，设置包括：

- • 若尔当曲线定理的源形式化，
- • 目标助手及其标准库和现有生态系统工具，
- • 结合 LLM、工具使用和人工编写的提示与指令的智能体流程。

#### 人工角色。

没有手写任何证明代码，也未向智能体提供任何数学见解或证明指导。人工输入用于配置工作流程：修改提示、插入额外的验证步骤，并利用观察到的失败模式改进过程。这正是我们希望在论文中呈现的那种工程经验。

#### 评估目标。

我们的评估旨在回答三个问题。首先，当前基于 LLM 的流程能否在保持较低人工工作量的同时，跨证明助手迁移大型、非平凡的形式化？其次，哪些因素对实际成功影响最大：源和目标助手的工具质量、库的成熟度、逻辑基础的性质与不匹配、所使用的模型，还是智能体流程的设计？第三，对于重新形式化，什么是好的智能体流程和防护栏设计？

#### 衡量指标与报告观察结果。

如果生成的目标开发在目标助手中完全验证（没有sorry 占位符或额外公理）并建立了最终的若尔当曲线定理陈述，则重新形式化被视为验证成功。对于每个重新形式化，我们首先给出一个侧重于流程设计的定性经验报告。特别是，我们强调在实践中学习到的有用经验：如何构建工作流程、智能体在哪里失败，以及哪些设计选择和防护栏使重新形式化成功。

随后，我们用量化描述符补充此经验报告：估计的人工参与时间、生成开发的大小（定理数、行数、策略数）、编译时间、原始证明中已经存在于目标助手库中的比例与需要主动形式化的部分的比例、完成项目所需的活动天数，以及近似的 LLM 成本。这些指标当然不完美——证明规模是复杂性的一个平庸代理变量，而时间和成本在很大程度上依赖于供应商——因此不应被理解为最终基准，而是作为定性报告的支撑背景。

## 3 JCT：从 Mizar 到 Lean

从 Mizar 数学库（MML）重新形式化 JCT 分三个不同的步骤进行：(1) 提取依赖信息，(2) 构建证明草稿和库对齐，(3) 填充证明。我们同时使用了原始的 Mizar 工具（Naumowicz 和 Kornilowicz, 2009（https://arxiv.org/html/2607.01734#bib.bib354））和mizar-rs 证明检查器重实现（carneiro:LIPIcs.ITP.2023.10）。

#### 步骤 1：提取元数据。

Mizar 证明检查器不是一个单一工具，而是一组在不同阶段分别执行并通过标准中间文本格式交换数据的工具集合。与证明数据完全存储在内存中的封闭环境不同，文本格式支持对证明数据进行独立的处理和分析。

我们利用成功运行证明检查器生成的中间文件来提取源文件之间的依赖图，以及最终若尔当曲线定理陈述所在开发中的定理依赖信息。

#### 步骤 2：证明草稿和库对齐。

依赖图和 MML 源代码被提供给一个智能体，指令是每个 Mizar 源文件对应生成一个 Lean 文件，将 Mizar 定理翻译为 Lean 定理骨架，并插入包含原始 Mizar 源元素、位置以及当前定理证明中使用的定理和引理的注释。

在第二轮中，智能体被指示为从 Mizar 导入的每个组件补充元数据，即 Mathlib 中最接近的匹配定理。

然后手动验证生成的若尔当曲线定理陈述是否正确，并且仅依赖于 Mathlib 中的定义。

#### 步骤 3：填充证明。

最后，指示智能体利用元数据和 Mizar 源文件填充每个定理的证明。Mizar 源提供证明草稿，而元数据提供证明中可用的一个闭合引理集。当上一步找到的最接近匹配足以闭合目标时，智能体被指示委托给 Mathlib。

尽管有元数据和源链接，智能体有时会偏离，尝试从头编写证明草稿，特别是在上下文窗口总结之后。在这种情况下，手动引导智能体参考 Mizar 源文件。在整个形式化过程中，这种情况发生了大约 10 次，除此之外没有提供数学指导。

通过使用脚本自动生成的状态文件（过滤 Lean 构建输出）和包含人类可读形式化计划的 Markdown 文件来跟踪进度，智能体被指示在完成每个定理后更新该 Markdown 文件。

### 3.1 结果

最终的 Lean 开发包含 413 个引理和定理，大约 474,000 个字符（约 11,000 行）。相比之下，源 Mizar 开发（限制为JORDAN*、BROUWER* 和 BORSUK*）大约 775,000 个字符（约 23,500 行）。大小的差异很大程度上归因于引理被 Mathlib 中的接近匹配所消解。该项目在 Mathlib 缓存的情况下编译耗时 111 秒（lake build 的挂钟时间）。

整个形式化大约需要 10 天完成，使用了通过 GitHub Copilot 的 Claude Opus 4.6 和 GPT-5.4。我们估计人工参与（包括搭建项目、监控进度和引导智能体）约为 20 小时。

#### 与 Mizar 的差异。

由于流程优先使用现有的 Mathlib 引理（只要足够），生成的 Lean 开发并不总是重现 Mizar 的内部证明机制。若尔当曲线定理论证的整体结构仍然接近源文件，但几个中间构造被更惯用的基于 Mathlib 的推理所取代。特别是，Mizar 的 Go-board 证明工程中的大量部分已不再需要，因为等价的拓扑结果在 Mathlib 中已经可用。

## 4 JCT：从 HOL Light 到 Lean

与从 Mizar 到 Lean 的形式化不同，从 HOL Light 到 Lean 的形式化是线性的。HOL Light 对若尔当曲线定理的证明分为 30 个部分（标记为 A 到 DD）。智能体被指示逐部分、逐定理地工作，而不预先计算依赖图或阅读后续部分。智能体对每个部分的工作流程设置如下：

1. 1. 使用专用脚本填充 HOL Light 定理和定义的目录。
2. 2. 构建定理和定义的 Lean 骨架，使用sorry 占位符代替证明。
3. 3. 依次填充所有 sorry，每次填充后尝试构建。
4. 4. 一旦文件没有sorry 且干净编译，用相应的 Lean 定理更新目录并更新状态文档。
5. 5. 再次读取指令文件，继续下一个部分。

#### 填充目录。

在读取状态文件以确认项目状态和当前部分后，智能体执行一个专用 Python 脚本，该脚本从给定部分提取所有定理和定义