A formalization of Borel determinacy in Lean

Each language version is independently generated for its own context, not a direct translation.

这篇论文讲述了一个非常酷的故事：一位名叫 Sven Manthe 的数学家，使用一种名为 Lean 的“超级数学计算器”（计算机证明助手），成功地将一个困扰数学界几十年的深奥定理——博雷尔确定性（Borel Determinacy）——完全用代码“算”了出来。

为了让你轻松理解，我们可以把这个过程想象成建造一座通往“无限游戏”王国的桥梁。

1. 什么是“无限游戏”？（背景故事）

想象一下，有两个玩家（0 号和 1 号）在玩一个永远玩不完的游戏。

他们轮流从一堆数字或符号中挑选。
每选一个，就形成一个越来越长的序列。
游戏永远不会结束，最终会形成一个无限长的序列。
规则是：如果这个无限序列符合某种特定的“图案”（比如它是某种复杂的数学集合），0 号赢；否则，1 号赢。

核心问题：在这个无限长的游戏中，是否总有一方拥有“必胜策略”？也就是说，无论对方怎么出招，只要我按我的策略走，我就一定能赢？

在数学上，这被称为“确定性”。对于简单的游戏，答案很明显；但对于那些图案极其复杂（属于“博雷尔集”）的游戏，这个问题非常难解。

2. 马丁的“魔法地图”（原始证明）

1975 年，一位叫马丁（Martin）的数学家证明了：只要游戏的规则（那个图案）是“博雷尔集”级别的，那么这个游戏一定是确定的（有人必胜）。

马丁的证明非常精妙，但他用了一种叫做**“解包”（Unraveling）**的魔法。

比喻：想象原来的游戏是一个复杂的、打结的毛线球（很难直接看出谁赢）。马丁说：“别直接解这个毛线球！我们把它‘解包’到一个新的、更简单的游戏世界里去。”
在这个新世界里，游戏的规则变得像“开/关”灯一样简单（要么赢，要么输，没有中间地带）。
一旦在新世界里证明了有人必胜，就能把胜利“映射”回原来的复杂游戏。

马丁的证明依赖于一种层层递进的数学归纳法，就像爬楼梯一样，从最简单的规则开始，一步步构建出复杂的规则。

3. 用 Lean 重写证明（本文的成就）

Sven Manthe 做的，就是把马丁的这篇论文，从“人类语言”翻译成"Lean 编程语言”，让计算机一步步验证，确保没有任何逻辑漏洞。

这就像把一本充满直觉和省略号的“魔法书”，变成了一本每一步都严格符合物理定律的“工程图纸”。

遇到的挑战与创意解决方案：

挑战一：处理“无限”的楼梯
马丁的证明中，处理“无限多个游戏组合”时，需要用到一种叫“逆极限”的高级数学工具。这就像要把无数个不同大小的盒子套在一起，还要保证它们完美契合。

Sven 的解法：他引入了**“范畴论”**（一种研究数学结构之间关系的工具）。他把这些游戏看作是一个个“乐高积木块”，利用范畴论的通用规则，自动把这些积木完美地拼在一起，而不是手动去数每一块积木。这就像是用一个自动化的 3D 打印机，而不是手工去粘。

挑战二：策略的“定义域”问题（最有趣的部分）
在数学里，有些策略只在“特定情况”下才有意义。比如，0 号玩家的策略只在“轮到 0 号走”时存在，轮到 1 号时这个策略就“不存在”了。

传统做法（Lean 库的惯例）：为了编程方便，通常会给这些“不存在”的情况编造一个**“垃圾值”**（比如强行规定：如果轮到 1 号，0 号的策略就是“0"）。这就像为了填表，把“不适用”的格子强行填上"0"。
Sven 的做法：他坚持**“不填垃圾值”**。如果策略不存在，他就直接说“这里没有定义”。
- 比喻：想象你在写一个食谱。
  - 填垃圾值法：如果你没有鸡蛋，食谱就写“放 0 个鸡蛋”。虽然能算，但如果你后面要计算“鸡蛋的总重量”，0 个鸡蛋可能会干扰逻辑。
  - Sven 的方法：食谱直接写“如果没有鸡蛋，这一步跳过”。
- 为什么这很难？ 在计算机里，这会让代码变得非常复杂（因为类型会随条件变化）。Sven 为此发明了一些特殊的“魔法咒语”（自动化脚本），让计算机能自动处理这些复杂的逻辑跳转，就像给计算机装了一个智能导航，能自动绕过“死胡同”。

4. 为什么这很重要？

数学的“零误差”验证：人类看论文可能会漏掉一个微小的假设，但计算机不会。Sven 证明了马丁的定理在计算机眼里是绝对真理。
打破常规：Sven 挑战了数学软件界（Mathlib）的惯例。大家习惯用“垃圾值”来偷懒，但他证明了坚持严谨的数学定义（不填垃圾值）虽然难，但更清晰、更强大。这就像是为了追求完美的建筑，拒绝使用任何填充物，虽然施工难度大，但大楼更坚固。
未来的基石：这是第一次有人用计算机证明这么高级的“博雷尔”级别的游戏理论。以前计算机只能证明简单的游戏。这为未来证明更复杂的数学定理（甚至涉及“大基数”这种宇宙级别的数学概念）铺平了道路。

总结

这篇论文就像是一次**“数学探险”：
Sven Manthe 带着计算机（Lean），拿着马丁留下的古老地图（原始证明），穿越了复杂的逻辑丛林。他不仅成功到达了终点（证明了定理），还修了一条更坚固、更规范的新路（改进了编程方法），告诉后来的探险者：“看，我们不需要用‘垃圾值’来凑合，我们可以用更优雅、更严谨的方式构建数学大厦。”**

这不仅是一个数学证明，更是一次关于**“如何用最严谨的方式思考”**的演示。

Each language version is independently generated for its own context, not a direct translation.

这是一份关于 Sven Manthe 在 Lean 4 定理证明器中形式化**博雷尔确定性（Borel Determinacy）**的论文《A formalization of Borel determinacy in Lean》的详细技术总结。

1. 研究问题 (Problem)

核心目标：在 Lean 4 定理证明器及其数学库 mathlib 中，形式化证明博雷尔确定性定理。该定理由 Martin (1975) 证明，指出所有博雷尔集（Borel sets）上的无限两人博弈（Gale-Stewart 博弈）都是确定的（即至少有一方拥有必胜策略）。
背景与挑战：
- 证明复杂度：博雷尔确定性是集合论中著名的定理，其证明需要 ZFC 公理系统中比大多数常见定理大得多的片段（涉及不可达基数等概念，尽管在 ZFC 内可证）。
- 形式化难度：此前，没有任何证明助手（Proof Assistant）形式化过闭集（Closed sets）以外的确定性结果。
- 类型论差异：Lean 基于构造演算（Calculus of Inductive Constructions），其理论强度略强于 ZFC（等价于 ZFC 加上任意有限个不可达基数），因此博雷尔确定性在 Lean 中成立。但更强的确定性形式（如解析集确定性）在没有额外公理的情况下无法在 Lean 中证明。
- 技术障碍：Martin 的原证明涉及复杂的逆极限构造、策略的层级定义以及处理部分函数（Partial Functions）的方式，这些在类型论中直接形式化极具挑战性。

2. 方法论 (Methodology)

论文遵循 Martin 在 [Mar85] 中的证明思路，但针对 Lean 的类型论特性进行了关键性的调整和适配：

2.1 核心证明策略：普遍可解性 (Universal Unravelability)

不直接证明确定性：证明不直接针对博雷尔集进行归纳，而是证明一个更强的性质——普遍可解性（Universal Unravelability）。
定义：
- 可解性 (Unravelability)：对于任意 $k$ ，存在一个 $k$ -覆盖（ $k$ -covering），使得原博弈的支付集在该覆盖下的原像是闭开集（Clopen）。
- 普遍可解性：对于任意覆盖，该博弈在覆盖后的版本都是可解的。
优势：普遍可解性集合构成一个 $\sigma$ -代数。这使得可以通过对博雷尔集的构造进行归纳（补集、可数并集），从而避免 Martin 原证明中使用的超限归纳法（Transfinite Induction），简化了形式化过程。

2.2 关键构造与形式化技术

博弈定义：
- 使用 List 表示有限序列，树（Tree）定义为有限序列的集合。
- 策略表示：形式化中定义了三种策略概念：策略（Strategy）、拟策略（Quasistrategy）和预策略（Prestrategy）。预策略被定义为从位置到移动集合的函数（允许空集），这使得定义必胜预策略变得平凡（空预策略即必胜），简化了引理证明。
- 函数式策略 vs. 策略树：虽然数学上常用“策略树”（兼容策略的位置树），但在 Lean 中，函数式策略（Functional Strategies，即从位置映射到移动）更容易定义和递归，因此主要采用此定义，并通过满射映射到策略树。
逆极限构造 (Inverse Limit)：
- 处理可数并集时，需要构造博弈的逆极限。
- 范畴论应用：利用 mathlib 的范畴论库，定义树范畴 $\mathcal{C}$ 。证明了该范畴具有所有极限，并利用伴随函子定理（Adjoint Functor Theorem）证明层级限制函子保持极限。
- $k$ -覆盖的修正：Martin 原证明要求覆盖在前 $k$ 层是恒等映射，这在类型论中难以处理。作者将其放宽为“双射”，并通过范畴论引理证明投影映射在相应层级上是 $k$ -固定的（ $k$ -fixing）。
闭集的可解性：
- 构造了一个“解构博弈”（Unraveling game），其中玩家不仅移动，还同时提交策略（或拟策略）。
- 通过引入额外的数据结构（策略树），将原本复杂的策略交互转化为博弈树中的节点，使得解构后的博弈成为闭开博弈（Clopen game）。

2.3 部分函数的形式化设计 (Partial Functions)

设计选择：Lean mathlib 通常使用“垃圾值”（Junk values，如将部分函数扩展为全函数，未定义处返回 0）来处理部分函数。
本文做法：作者坚持使用命题假设（Propositional Hypotheses），即定义域受限的函数类型 {x // P x} → Y。
理由：这更符合数学直觉，且在重写（Rewriting）时能自动保持定义域属性，避免了手动维护大量关于“该点有定义”的假设。

3. 关键贡献 (Key Contributions)

首个高阶确定性形式化：这是首次在证明助手（Proof Assistant）中形式化超越闭集（Closed sets）的博弈确定性结果。项目包含约 5000 行代码，大部分用于形式化 Martin 的证明本身。
证明方法的改进：
- 用直接归纳替代了 Martin 证明中的超限归纳，通过引入“普遍可解性”概念，使得证明过程更适应构造性类型论。
- 利用范畴论处理逆极限，解决了层级稳定化（Levelwise stabilization）在形式化中的识别难题。
Lean 开发实践与工具改进：
- 策略定义：引入“预策略”概念简化了存在性证明。
- 自动化战术（Tactics）：开发了自定义战术来处理列表长度奇偶性（Presburger 算术）和 $k$ -固定属性的自动推断。
- 性能优化：针对依赖类型（Dependent Types）嵌套导致的证明项（Proof Terms）爆炸问题，开发了元程序 abstract（后被核心语言采纳为 as_aux_lemma），通过 eagerly abstracting proof terms 将运行时间从指数级降低到线性级。
方法论辩论：详细论证了在形式化数学中，使用“定义域受限”而非“垃圾值”处理部分函数的优劣，指出虽然 mathlib 倾向于后者，但在处理复杂依赖关系时前者更具优势，尽管对工具支持要求更高。

4. 结果 (Results)

定理证明：成功在 Lean 4 中证明了所有博雷尔博弈都是确定的。
代码库：建立了一个包含博弈定义、策略理论、覆盖理论及 Martin 证明完整形式化的代码库（约 5000 行）。
工具链增强：
- 解决了 Lean 中处理依赖类型部分函数时的重写（Rewriting）和性能瓶颈问题。
- 证明了范畴论工具在处理博弈论逆极限构造中的有效性。

5. 意义 (Significance)

理论验证：证明了即使在强类型论（Lean）中，涉及复杂集合论构造（如博雷尔集、不可达基数强度）的定理也是可形式化的，且不需要额外的非构造性公理（除了 ZFC 本身隐含的强度）。
描述性集合论库建设：为在 Lean 中构建更完整的描述性集合论（Descriptive Set Theory）库奠定了基础。博雷尔确定性是连接大基数公理与描述性集合论的关键桥梁，其形式化有助于后续研究（如解析集确定性）。
形式化方法论的启示：
- 展示了在类型论中处理“部分函数”的另一种可行路径（依赖类型 vs 垃圾值），为未来的形式化项目提供了设计参考。
- 揭示了当前 Lean 工具链在处理深层依赖类型时的性能瓶颈，并提出了有效的工程解决方案（元程序抽象），推动了工具本身的改进。
未来方向：为形式化更大类集合的确定性（需大基数假设）以及从确定性构造大基数内模型（Inner Models）铺平了道路。

总结：该论文不仅是一个具体的数学定理形式化成果，更是一次在类型论框架下处理复杂数学结构（博弈、策略、逆极限）和形式化工程挑战（依赖类型性能、部分函数设计）的典范，显著推进了计算数学和描述性集合论在计算机辅助证明领域的发展。