💻 computer science

ZFLean: a framework for set-level mathematics in Lean

本文介绍了 ZFLean，这是一个 Lean 4 库，它将核心 ZFC 集合论集成到 Mathlib 生态系统中，通过改进的易用性、规范构造以及与原生类型的桥梁，以促进混合集合层级和类型化证明。

原作者： Vincent Trélat

发布于 2026-04-28

📖 1 分钟阅读☕ 轻松阅读

原作者： Vincent Trélat

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

想象一下，你正在试图建造一座房子。你拥有两套不同的蓝图和工具：

“类型化”工具（Lean 的原生系统）： 它们就像高科技的激光引导机械臂。它们极其精确，但只有当每一块砖都完美地标记了其特定类型（例如“红砖”、“蓝砖”）时，它们才能工作。如果你试图在需要“蓝砖”的地方使用“红砖”，机械臂就会停止并拒绝工作。这对于安全性来说很棒，但有时数学感觉需要更加灵活。
“集合”工具（ZFC）： 它们就像一大堆杂乱无章的 raw 粘土。在这个世界里，一切都只是“东西”。你可以把一块粘土塑造成杯子、球体或正方形，而它们都只是“粘土”。这就是传统数学家通常思考集合的方式：一切都是一个集合的元素，你可以自由地混合和搭配。

问题所在：
很长一段时间以来，如果你想在“类型化”机械臂车间内使用“集合”工具进行数学运算，那简直是一场噩梦。你必须不断将你的粘土形状翻译成机械臂友好的标签，证明你的翻译是正确的，然后再将结果翻译回来。这既缓慢又枯燥，而且容易出错。大多数人干脆完全避开了那堆粘土，只使用机械臂。

解决方案：ZFLean
Vincent Trélat 创建了 ZFLean，这就像在机械臂车间内部建造了一个通用翻译器和一套定制工具。

以下是其工作原理，使用简单的类比：

1. “粘土”车间（ZFC 模型）

ZFLean 在机械臂车间内设立了一个特殊区域，在这里适用“粘土”规则。在这里，你可以像传统数学家那样定义集合、关系和函数，而无需担心机械臂通常要求的严格“类型”。这是一个安全空间，你可以说“这是一组数字”，而无需机械臂询问：“它是Nat还是Int？”

2. “智能翻译器”（关系演算）

过去最大的头痛问题是“样板代码”——即为了证明你的粘土形状实际上是有效的，所需的大量重复、枯燥的文件工作。

旧方法： 对于每一步，你都必须手动证明“是的，这个关系是一个函数”以及“是的，这个定义域是有效的”。
ZFLean 方法： 该框架自带智能小助手（称为 zrel、zpfun 和 zfun 等策略）。把这些助手想象成自动填充表单。当你编写证明时，这些助手会自动检查枯燥的细节并为你填写文件。你负责编写数学内容；助手负责处理行政负担。

3. “桥梁”（互操作性）

这是神奇的部分。通常，“粘土”世界和“机械臂”世界是相互隔离的。ZFLean 在它们之间建造了桥梁。

如果你在粘土世界中构建了一组自然数，ZFLean 可以立即指出：“嘿，这实际上与机械臂的 Nat 类型是相同的。”
这意味着你可以进行混乱但灵活的集合论数学运算，然后无缝跨越桥梁，使用机械臂强大且预先构建的工具（如代数求解器）来完成工作。你不必二选一；你可以在同一个证明中同时使用两者。

4. “乐高套件”（规范构造）

为了让生活更便捷，ZFLean 附带了一套预先构建的标准乐高积木套件。

需要一组真/假值吗？这里有一个布尔集合。
需要一组计数数字吗？这里有一个自然数集合。
需要一种处理“可能”值（如选项）的方法吗？这里有一个选项集合。
这些不仅仅是 raw 粘土；它们是预先塑形、经过测试的，并附带了使用说明（例如“如何相加两个数字”或“如何切换开关”）。

5. “试驾”（案例研究）

为了证明该系统有效，作者使用了一个经典的数学谜题——柯里化同构——对其进行了测试。

想象一下： 你有一台一次接受两个输入的机器（就像三明治机同时接受面包和肉）。“柯里化”是将这台机器转化为一次只接受一个输入（面包）的过程，然后给你一台新机器，这台新机器接受第二个输入（肉）。
作者使用 ZFLean 证明了这两种关于机器的思考方式实际上是同一回事。证明脚本看起来几乎和人类数学家在黑板上写的一模一样，而“智能助手”则在后台默默地处理所有的技术故障。

结论

ZFLean 是一个框架，它让数学家能够在传统集合论的灵活、直观风格（“粘土”）中工作，同时置身于现代、严谨的计算机证明系统（“机械臂”）之内。它消除了翻译的摩擦，自动化了枯燥的文件工作，并搭建了桥梁，使你可以使用来自两个世界的最佳工具，而不会卡在中间。

其结果是一个包含约 8,300 行代码的库，使得在 Lean 中进行“集合级”数学运算感觉就像在纸上书写一样自然流畅。

以下是 Vincent Trélat 所著论文《ZFLean：Lean 中的集合层级数学框架》的详细技术总结。

1. 问题陈述

现代在 Lean 等证明助手中的形式化主要基于类型论（特别是依赖类型论），其中数学对象被构建为类型。尽管这种方法功能强大，但对于集合层级数学（ZFC）而言却显得笨拙，而后者通常更受青睐，原因包括：

外延性推理：基于元素而非构造来推理相等性。
偏函数处理：通过关系自然地处理偏函数，而非使用 Option 类型或依赖类型对其进行编码。
范畴式推理：在“同构意义下”工作，而非严格的定义相等性。

挑战：在类型化助手（如 Lean 的 Mathlib ZFC 模型）中直接在集合论模型内工作会引入显著的摩擦：

样板代码：用户必须不断手动管理“侧条件”（例如，证明一个关系是良定义的，证明一个函数是全函数）。
脆弱性：跨越集合论对象（ZFSet）与原生 Lean 类型（Type）之间的边界是手动的且容易出错。
缺乏自动化：现有工具通常缺乏使集合论证明像类型证明一样流畅所需的特定重写提示和策略。

2. 方法论

作者提出了ZFLean，这是一个构建在 Mathlib 现有 ZFC 模型之上的 Lean 4 库。该方法论侧重于创建统一的关系演算和互操作桥梁，以使集合层级的开发更加符合人体工程学。

核心设计选择：

基础：利用 Mathlib 的 ZFC 实现，该实现将集合构建为归纳“预集”（PSet）的外延商。
关系演算：ZFLean 不将函数视为标准类型论中的首等全对象，而是将其视为函数关系。它引入了针对二元关系、偏函数和全函数的演算。
基于策略的自动化：该框架引入了三个轻量级策略（zrel、zpfun、zfun），旨在自动消除良构性侧条件（例如，证明一个复合是关系或函数）。
桥梁：该库在规范 ZFC 对象（如 ZFBool、ZFNat）与 Lean 的原生类型（Bool、Nat）之间构建了显式同构（桥梁），允许属性在两个世界之间传输。

3. 主要贡献

A. 关系演算与自动化

定义：形式化了关系的逆、恒等、复合、定义域、值域和像。
功能性：区分了偏函数（IsPFunc）和全函数（IsFunc）。
策略：
- zrel：消除证明某集合是关系（ $R \subseteq A \times B$ ）的目标。
- zpfun：消除证明某集合是偏函数的目标。
- zfun：消除证明某集合是全函数的目标。
- 这些策略使用属性标记的引理（例如 @[zfun]）递归地解决侧条件，从而对用户隐藏样板代码。
符号：引入了函数应用（@zf(x)）和 $\lambda$ -抽象的便捷语法，并提供了关于 $\beta$ -归约、 $\eta$ -展开和外延性的定理。

B. 规范构造

该库提供了一套在 ZFC 内定义的标准数学对象，并包含其通用性质：

布尔值：一个具有代数结构（合取、析取、否定）和案例消除器的双元素集合 $B$ 。
自然数（ $\mathbb{N}$ ）：定义为最小的归纳集（冯·诺依曼序数）。包含递归子、归纳原理和算术运算。关键在于，它配备了 CommSemiring 结构，以便利用 Lean 的 ring 策略。
整数（ $\mathbb{Z}$ ）和有理数（ $\mathbb{Q}$ ）：构造为自然数/整数对的商类型，运算从代表元提升而来。
余积和选项：和类型与选项类型的集合论定义。

C. 同构与传输

嵌入与同构：通过单射和双射函数定义了集合层级的嵌入（ $A \hookrightarrow_z B$ ）和同构（ $A \cong_z B$ ）。
康托尔 - 施罗德 - 伯恩斯坦定理：在框架内形式化。
传输：证明了 ZFC 构造与 Lean 的原生类型是同构的（例如 ZFBool $\simeq$ Bool）。这允许用户将定理从丰富的 Mathlib 类型论库无缝“传输”到集合论上下文中。

D. 案例研究：柯里化同构

该论文通过证明柯里化同构： $C^{A \times B} \cong (C^B)^A$ ，展示了该框架的实用性。

证明将 curryz 和 uncurryz 定义为集合层级函数。
它利用框架的自动化处理侧条件（复合和像的良定义性），证明它们是互逆的。
证明脚本紧密模仿标准数学论证，自动化层处理了“枯燥”的集合论验证。

4. 结果

工件规模：该库包含 8,324 行 Lean 代码和 706 个已证明定理。
组件细分：
- 关系演算：约 2,534 行代码（172 个定理）。
- 自然数：约 1,260 行代码（199 个定理）。
- 嵌入/同构：约 1,626 行代码（31 个定理）。
可用性：案例研究表明，该框架成功降低了集合层级形式化的摩擦。用户可以编写看起来像标准集合论论证的证明，而无需手动证明每个关系复合都是有效关系。
互操作性：在 ZFSet 和原生 Type 之间切换的能力，使得可以在集合论对象上重用 Mathlib 的代数策略（如 ring）。

5. 意义

弥合基础：ZFLean 有效地调和了单一证明助手中数学的“集合论”和“类型论”观点。它允许数学家为特定问题选择最自然的基础（外延集合 vs. 构造类型），而不会失去对生态系统自动化的访问。
人体工程学：通过自动化集合论中固有的繁琐侧条件（成员资格证明、关系良定义性），它使非专家也能在 Lean 中进行 ZFC 开发，并使大规模形式化变得切实可行。
可扩展性：模块化设计（关系演算 + 规范对象 + 桥梁）允许轻松扩展。未来的工作包括形式化实数（通过柯西序列或戴德金分割）和基本分析。
比较：与 Isabelle/ZF（其中集合论是单独的对象逻辑）或 Rocq 的集合论发展（通常缺乏与类型论自动化的深度集成）不同，ZFLean 提供了一种混合方法，在保持证明处于集合层级的同时，利用 Lean 原生的类型论基础设施。

总之，ZFLean 为在 Lean 4 中进行 ZFC 核心数学提供了一个稳健、符合人体工程学且可互操作的框架，成功降低了集合论形式化的入门门槛，同时保持了与更广泛的 Mathlib 生态系统的兼容性。