不弃选择公理，化解巴拿赫–塔斯基：一份尘封证明的复活

luyuanhong

不弃选择公理，化解巴拿赫–塔斯基：一份尘封证明的复活

原创  围城里的猫  MathSpark  2025 年 08 月 22 日 12:06  江苏

一篇被遗忘的研究工作为数学界最大争议之一扫清了障碍。两名学生如今已用计算机核验了该证明。

这是数学中最离奇的结论之一：把一个球分解成无数个微小的部分，再重新组装，居然可以得到两个新球，而且它们都与原球一样大。这一“巴拿赫–塔斯基定理”（Banach–Tarski）仿佛让球体能被“魔法般”地复制，因此一直令一些专业人士颇为不适。可事实表明，这个悖论有办法回避——上世纪 1990 年代几乎被遗忘的一条思路就能做到。如今，一名女学生和一名男学生对该思路进行了细致研究，并借助计算机完成了验证。

自 1924 年斯特凡·巴拿赫（Stefan Banach）与阿尔弗雷德·塔斯基（Alfred Tarski）发表相关结果以来，这种怪异的“倍增”就在数学界引发不安。一些学者据此怀疑：支撑整个学科的某条基本假设可能是错的。因为该悖论之所以成立，依赖于所谓的选择公理——允许从一族集合中各取出一个元素。20 世纪初，曾有批评者主张把选择公理从数学基本假设中移除。然而事实显示，缺少选择公理会产生更离奇的后果——因此，对大多数学家而言，“删去它”并不是选项。


巴拿赫–塔斯基悖论｜一个体积为 V 的球体可以分解为两个球体，每个的体积仍为 V ，也就是实现了“倍增”。

随后，法国研究者 Olivier Leroy 在 20 世纪 90 年代完成了看似不可能的壮举：他在不放弃选择公理的前提下，设法消解了巴拿赫–塔斯基悖论。他将相关想法记入笔记，但尚未来得及整理发表，便于 1996 年意外去世。17 年后，两位昔日同事将其资料汇编成一篇 40 页的法文论文并在网上公开。

据此，Leroy 扩展了拓扑学——这一比几何更为抽象的领域。通过去掉“拓扑必须以点为基本对象”这一前提，他得以推广该领域的许多既有概念。由此可以证明，巴拿赫–塔斯基悖论在这种新拓扑下不再出现：一个球体已无法被“倍增”，尽管选择公理仍然成立。

用于一项鲜为人知研究的证明检验器

这个深入到数学最抽象深处的证明，让两位高中毕业生 Chiara Cimino 和 Christian Krause 深深着迷。Krause 多年来一直学习多种编程语言，并曾参加德国“青年研究（Jugend forscht）”竞赛。在那里，他结识了以数学为主攻方向的 Cimino 。自 2020 年起，Cimino 在就读中学的同时于康斯坦茨大学修读数学，至今已完成七个学期。

2023 年，两位学生决定启动一个共同项目。他们希望将一个数学证明“形式化”：把它翻译为计算机可理解的编程语言，并交由计算机检验。后者由“证明检验器”完成——这是一类计算机程序，逐一核查陈述的逻辑顺序并检出矛盾。

这是一项相当繁琐的工作：专业数学家往往需要花费数天、数周甚至数月，先把证明整理为合适的形式，再将其译成 Lean 编程语言，以便计算机处理。Cimino 说：“按计划，我负责数学部分，Christian 负责信息学部分。但事实证明，这两部分根本无法彼此分割。”

Cimino 和 Krause 首先把 Leroy 的法文论文中的证明拆解成一个“蓝图”（Blueprint），分为数十个子步骤：他们需要定义若干量，完成一系列辅助性的小证明，并最终把所有部分汇总成完整结论。其间还得对证明若干处做“补全”——例如原文把某些步骤称为“显然”，却未给出细节。Krause 说：“有的地方最终写了几百行代码。”经过将近两年的努力——两人几乎每个周末都会在学生研究中心见面推进——他们终于完成了这项工作：Cimino 与 Krause 已将 Leroy 的证明形式化并通过计算机检验，并凭此在 2025 年的“青年研究（Jugend forscht）”大赛中获得第二名。

这也为数学共同体贡献了重要一环。当前，许多研究者正致力于用基本定义与定理扩充证明检验器的数据库，目标是未来任何数学证明都能由计算机核验。为此需要大量前期铺垫：原则上，几乎全部数学知识都要被翻译成程序语言。Cimino 与 Krause 现已提供了若干关键积木——他们形式化的众多拓扑学定义、命题与证明，如今已可供全球研究者调取使用。

两位获奖者如今都已高中毕业并即将入学。Cimino 将在波恩继续攻读数学，Krause 则计划在海德堡主修物理。但两人都已下定决心：今后仍将持续投入证明检验器相关工作。



MathSpark