最近，我花了一点时间翻看那份据称由 OpenAI 公布、收录了 722 个问题的数学成果清单。几何、数论、组合、代数、逻辑，各种熟悉又陌生的名字排在一起。对于一个做数学科普的人来说，这有点像小时候拿到一本厚厚的习题集：先翻目录，看看有没有自己认识的题。我本来也是这样随手翻着。编号 244 的标题停在眼前：The Partition Principle does not imply Choice。它的中文意思是：分划原理并不推出选择公理。

这句话看上去只是在两个抽象原理之间加了一个“不”，背后却牵涉集合论中最敏感的一条分界线：我们究竟需要多少“选择”，才能继续进行通常的数学？截至 2026 年 10 月 8 日，OpenAI 已公开一份日期为 2026 年 9 月 24 日的预印本，声称构造出了满足这一结论的模型。如果构造最终经独立检查成立，它将为一个长期开放的问题给出否定答案。(但现在更准确的说法仍然是“提出了一个候选模型”，而不是“数学界已经确认了定理”。)

先看懂两个原理

设有一个满射 g:B→A。满射的意思是，对每个 a∈A，单点集 {a} 在 g 下的原像集合都非空。分划原理（Partition Principle，简称 PP）断言：只要这样的满射存在，就一定存在一个单射 f:A→B。单射的意思是，A 中不同的元素不会被 f 映射到 B 中的同一个元素。

先介绍选择函数：给定一族以集合 I 为指标的非空集合Sᵢ，其中i遍历I。如果函数 c 的定义域是 I，并且对每个 i∈I 都有 c(i)∈Sᵢ，那么 c 就是这族集合的选择函数。选择公理（Axiom of Choice，简称 AC）断言：每一族非空集合都有选择函数。直观的讲，就是对于任何一堆非空集合，我们都能在每个集合里抓一个元素出来形成新的集合。而抓的方式就是选择函数。

对于满射 g:B→A，对每个 x∈A，单点集 {x} 在 g 下的原像集合都非空。选择公理在每个这样的原像集合下抓取元素，这样就有了选择函数f，于是 f(x) 是 {x} 在g 下的原像集合中的元素。而显然有 g(f(x))=x。因此，g∘f 等于 A 上的恒等映射，这样的 f 自动是单射：若 f(x)=f(y)，两边应用 g，就得到 x=y。

两个原理的差别就在这里：通过选择公理得到的 f 不仅是单射，还满足 g∘f 等于 A 上的恒等映射，也就是 f 是 g 的右逆。分划原理只保证存在某个单射 f:A→B，不要求 f(x) 属于单点集 {x} 在 g 下的原像集合。因此，这个单射未必是原像集合族的选择函数。事实上，“每个满射都有右逆”与选择公理等价。

和哆嗒数学网有关的两段往事

看到这个问题，我想起了两段和哆嗒数学网有关的往事。第一段与陶哲轩所著的《陶哲轩实分析》有关。早期版本的习题 8.4.3 曾要求读者证明：只要满射 g: B → A 存在，就有单射 f: A → B；随后再由这个性质推出选择公理。这个“反过来”其实触及了分划原理是否蕴含选择公理的长期问题。

后来，哆嗒数学网的小编在陶哲轩博客的《Analysis I》(中文译名《陶哲轩实分析》)勘误讨论页留言，指出题目需要补充条件。陶哲轩在讨论中确认，单射 f 还应满足：对每个属于 A 的元素 a，都有 g(f(a)) = a，也就是 f 是 g 的右逆。博客上的交流记录至今仍然可以查到。补上这一条件后，f(a) 才一定属于单点集 {a} 在 g 下的原像集合，题目也回到了与选择函数等价的正确表述。

第二段往事与一位群友有关。当时，哆嗒数学网的群里有位非常热心的朋友，经常回答大家的数学问题。硕士即将毕业时，他告诉我们，已经拿到了中科院数学所的录取机会，准备攻读数理逻辑方向。他还说，博士期间想研究的问题，就是分划原理与选择公理是否等价，并希望证明它们等价。

多年过去，我们已经失去了直接联系。后来我看到的公开资料显示，他已在国内一所高校任副教授，主要研究选择公理不成立时的集合论。至少从研究方向看，他仍沿着当年选择的道路走到了今天。看到这次的消息，我也想起了他：不知道他是否已经读到这份材料，又会怎样看待其中的构造。无论这个候选结果最终如何，愿他在自己长期投入的领域里继续有所收获。

为什么问题会悬而未决这么久

选择公理是一个全局原则：它同时处理任意规模、任意形状的非空集合族。分划原理的表面形式却只谈一对集合之间的满射和单射，它要求的是单射的存在，而非指定原像集合族的选择函数的存在。这两种叙述在有限情形中很接近，到了无限集合上却可能分开。

集合论里存在许多强弱不同的选择原则，它们分别保证不同类型的非空集合族有选择函数。例如，AC(WO) 断言：凡是以可良序集合为指标的非空集合族，都有选择函数；等价地，可以只考虑以序数为指标的集合族。一个模型可以满足 AC(WO)，同时存在其他非空集合族没有选择函数，从而使完整的选择公理失效。分划原理也是在这些原则的相互关系中被研究的。

要构造满足 PP 而不满足 AC 的模型，必须同时完成两件事：一方面，让某个非空集合族没有选择函数；另一方面，保证模型中的任意满射仍对应一个从值域到定义域的单射。前一个条件使 AC 失败，后一个条件使 PP 成立。难点就在于让这两个条件在同一个模型中共存。

新预印本声称构造了什么

OpenAI 的预印本给出的目标，可以概括成一个模型满足：

• ZF：不预设完整的选择公理；
• PP：每个满射都对应一个从值域到定义域的单射；
• AC(WO)：以可良序集合为指标的非空集合族都有选择函数；
• ¬AC：完整的选择公理失败。

这是一项相对一致性构造：从满足相应假设的起始模型出发，构造一个满足 ZF+PP+AC(WO)+¬AC 的模型。在目标模型中，以可良序集合为指标的非空集合族都有选择函数，但至少有一个非空集合族没有选择函数。与此同时，分划原理对模型中的所有集合都成立。

这类构造采用力迫法与对称子模型的方法。力迫法先得到原模型的一个扩张，其中的集合由称为“名字”的对象描述。随后，依据预先设定的对称性条件，从这些名字所描述的集合中构造出一个中间模型。在适当条件下，这个对称子模型仍满足 ZF。

构造的关键在于：某个非空集合族属于这个子模型，但它在扩张模型中的选择函数都不属于这个子模型，于是子模型中的 AC 失败。为了同时得到 PP，还必须证明：子模型中的任意满射，都有一个同样属于子模型的、从值域到定义域的单射。集合论中的函数本身也是集合，因此，函数是否属于目标模型，是整个证明不可缺少的一环。

从候选构造到独立验证

集合论的独立性结果尤其依赖模型构造的每一个细节。一个函数是否真的属于目标模型，一个对称性条件是否在所有阶段保持，所采用的对称性条件是否排除了目标集合族的所有选择函数，都可能改变最终结论。即使论文同时提供了代码、形式化材料或证明助理接口，也必须先确认：形式化的命题与论文中的模型构造完全一致，所有关键引理都被覆盖，而且没有把额外假设藏进定义里。

Lean 验证的意义取决于形式化所覆盖的内容：验证若干引理，与验证包含全部假设和关键步骤的最终定理，是不同层次的工作。论文中的数学陈述、代码中的命题及其依赖条件，需要一一对应。截至 2026 年 10 月 8 日，这份日期为 2026 年 9 月 24 日的候选构造及其形式化状态，仍有待独立核实与专家检查。

这种谨慎并不是对 AI 结果的特殊苛刻，而是集合论的正常标准。过去也曾有论文或预印本声称找到了类似模型，相关结论后来仍需要补充、修订或继续争论。一个新结果真正改变教科书，需要的不只是漂亮的摘要，而是模型存在性、ZF 公理保持、PP 成立以及 AC 失败这几件事同时经得住检查。

这件事真正能改变什么

如果预印本最终成立，那么“分划原理是否蕴含选择公理”这个问题的答案将是：不蕴含。更准确地说，PP 会被确认成一个严格弱于 AC 的选择原则。对于日常数学，这意味着很多依赖良序集合或可数结构的论证仍可能照常进行；但对于需要任意非空集合族都有选择函数的证明，PP 本身将不足以提供所需条件。

这件事也提醒我们，数学中的公理不是只有“接受”与“拒绝”两档。选择公理可以被拆成许多强弱不同的原则；一个理论可以保证某些类型的非空集合族有选择函数，同时允许其他非空集合族没有选择函数。看似只差一个函数存在性条件，背后却是整个数学宇宙结构的差异。

所以，编号 244 的真正看点并不只是“AI 解出了一道难题”。它把一个常被简化成口号的问题重新摆到我们面前：当我们断言一个非空集合族有选择函数时，究竟使用了哪一条公理？当我们只知道存在一个单射时，又能推出哪些集合族有选择函数？这两个问题之间的缝隙，正是集合论研究了一个多世纪的地方。

参考资料

1. OpenAI Math 项目目录，编号 244： The Partition Principle does not imply Choice。
2. OpenAI 预印本： The Partition Principle does not imply Choice，发布日期为 2026 年 9 月 24 日。
3. OpenAI Math 项目说明： OpenAI Math，包含成果目录与形式化状态说明。
4. 陶哲轩著《陶哲轩实分析》；陶哲轩博客《Analysis I》勘误讨论页，其中保留了关于习题 8.4.3 的交流记录。
5. Frank Gilson 的相关预印本： A model of ZF in which the Partition Principle holds but the Axiom of Choice fails；The Partition Principle implies the Axiom of Dependent Choices。相关预印本的结论与修订状态尚待独立核实。