为什么都在内核中？

# 为什么一切都放进内核？ 来源：https://lawrencecpaulson.github.io/2026/07/30/Collatz.html 2026年7月30日 \[`general` (https://lawrencecpaulson.github.io/tag/general)`Lean` (https://lawrencecpaulson.github.io/tag/Lean)`Isabelle` (https://lawrencecpaulson.github.io/tag/Isabelle)`HOL system` (https://lawrencecpaulson.github.io/tag/HOL_system)`philosophy` (https://lawrencecpaulson.github.io/tag/philosophy)`memories` (https://lawrencecpaulson.github.io/tag/memories)\]爆炸性新闻！[Collatz猜想](https://en.wikipedia.org/wiki/Collatz_conjecture)刚刚被证伪了。Ramana Kumar 证明了它的否定形式。该证明已在 Lean 中通过检查，并使用独立的 Nanoda 类型检查器进行了双重检查。不幸的是，证明是错误的。它利用了 Lean 内核中的一个 bug。不知为何，Nanoda 也没有检测到这个错误。我现在写这篇文章不是为了幸灾乐祸。可靠性 bug 已经在 [Isabelle 中被发现](https://lawrencecpaulson.github.io/2026/01/15/Broken_proofs.html)，以及其他许多证明助手中；也许明天就会发现一个新的、可怕的 bug。尽管如此，这里有一些教训，让我们开始吧！ ### Collatz猜想 这个著名的猜想已经存在了近一个世纪，吸引了严肃数学家和平庸之辈的关注。它涉及以下过程：从一个数字 N 开始。然后重复这一步：如果 N 是偶数，就除以二；如果是奇数，则将 N 设为 3N+1。Collatz 猜想这个过程无论我们从哪个 N 开始，都保证最终达到 1。广泛的测试未能找到任何反例。最近的工作表明，语言模型非常擅长[寻找猜想的反例](https://theconversation.com/hello-there-the-jacobian-conjecture-is-false-thanx-why-a-tiny-social-media-post-has-mathematicians-rethinking-ai-283883)，那么为什么不用 Collatz 试试呢？解决它确实会引起轰动。 ### 证明对象的沉重负担 正如我们半个世纪以来所知道的，[证明对象是不必要的](https://lawrencecpaulson.github.io/2022/01/05/LCF.html)。Robin Milner 设计 ML 语言，就是为了支持证明助手的特定目的。通过*抽象类型*的概念，证明内核可以与程序的其余部分安全隔离。推理规则被限制在抽象类型内，成为创建定理的 API。 尽管如此，我们社区中的很多人还是加倍努力地存储证明对象。他们特别指出，证明对象是可以被独立检查的*证书*。但我不知道有任何一例独立的证明检查器检测到了通过证明助手内核的可靠性错误。对于 Collatz 来说，正如我们所见，Nanoda 也被愚弄了。当我们考虑到证明对象所带来的内存负担时，这就像开车去任何地方都在后面拖着一辆备用车，以防抛锚。而你的车确实抛锚了，但瞧，备用车也坏了。而且你的车抛锚的确切原因正是拖着备用车的负担。因为只有那些有证明对象的证明演算，才似乎需要把所有东西都放进内核。 ### 偷窃与诚实的劳作 在 20 世纪的大部分时间里，逻辑学家假设的公理尽可能少，然后从这些公理推导出其余的数学。也许他们担心罗素悖论和其他悖论；也许他们只是过于节俭。这种观点也许由罗素本人表达得最好： > “假设”我们想要的东西的方法有许多优点；它们与偷窃相比诚实劳作的优势相同。让我们把这种方法留给别人，继续我们的诚实劳作吧。（罗素，1919） 所以值得注意的是——据传闻——Lean 中的 bug 是由内核中的嵌套归纳类型引起的。Rocq 中的一些可靠性 bug 是由内核中涉及递归函数的模式匹配引起的。我不太确定为什么依赖类型理论不够表达力，无法从更基础的演算中表达诸如递归之类的东西。原因可能是技术性的。但让我们明确一点：在集合论和简单类型理论中，你几乎不需要假设什么。集合论给了你一些引入集合的原则：并集、分离、配对、替换。简单类型理论给了你一点点逻辑和一点 λ-演算，从而得到一个类型化集合论，其中的集合是布尔值函数。然后，通过诚实的劳作，你可以在相当一般的情况下获得归纳定义、记录、递归数据结构和递归函数，包括模式匹配和部分函数。你可以使用符号二进制算术进行数值计算。因为所有这些都是在原始公理的基础上定义的，而不是被假定出来的，所以它们位于内核之外，不会导致矛盾。 回到 1980 年代，当我研究 Martin-Löf 类型理论时，出现了一个关于表达递归函数的问题。该理论只承认基本递归的形式。但该理论也允许更高类型，从而有可能实现更强大的递归形式。由于我接受了诚实劳作传统的数学训练，我努力（而且确实很费力）在 Martin-Löf 类型理论中定义了一个[组合子系统](https://doi.org/10.1016/S0747-7171(86)80002-5)，可以表达巨大的终止递归函数空间。但我当时没有理解这个游戏的玩法。对这个问题的正确答案是*扩展* MLTT，加入递归的通用概念，而且我必须承认，这可以简单而优雅地完成。我不确定是否有人理解了我所做的工作。多年后，我看到这篇论文被引用时评论说：“Paulson 用递归扩展了 MLTT”：他们无法想象有人通过诚实的劳作*获得*递归。 ### 诚实的劳作是什么样的？ 我能理解证明助手的实现者为什么选择偷窃这个选项，因为诚实的劳作真的像砸石头一样。众多目标中最简单的是[递归数据结构](https://rdcu.be/fwTU2)。归纳定义可以转化为集合上的单调算子。最小不动点给出归纳定义，如果你更喜欢余归纳定义，就取最大不动点。在 Isabelle 中，我们很少把这些构造与类型联系起来，但[递归数据类型](https://rdcu.be/fwT1b)是一个重要的特例，现在通过*有界自然函子*以一般而复杂的方式处理。 从第一性原理构造*递归函数*尤其乏味。你从一个[良基关系](https://en.wikipedia.org/wiki/Well-founded_relation)开始，然后通过良基归纳证明所需递归函数的存在性。我在 MLTT 中关于递归的工作在这方面有些帮助，所以并非完全白费。Isabelle/HOL 现在支持[递归函数定义](https://rdcu.be/fwT25)的极大一般性，包括模式匹配和终止检查。而所有这些都安全地位于内核之外。 具有讽刺意味的是，证明对象有时被吹捧为能带来更强的可靠性保证。显然恰恰相反。如果你主要关心的是可靠性，你应该选择 HOL Light 或 HOL4.1 (https://lawrencecpaulson.github.io/2026/07/30/Collatz.html#fn:1)。Isabelle 的 bug 比这两个多，但很少，而且肯定比某些其他系统少得多。