回顾百年前数学基础危机：从罗素悖论到哥德尔不完备定理

100年前，数学界经历了一场基础危机：若干悖论的发现，暴露出支撑数学各个领域的支柱上出现了裂缝。其中最著名的是罗素悖论，它指向那个自相矛盾的“所有不包含自身的集合所组成的集合”，从而表明朴素集合论是不一致的。这促使数学家们去寻找一个严谨而无矛盾的基础。特别是，David Hilbert 发起了一项纲领，要设计出一套完备且一致的公理系统：人们应当能够从公理中推出一切数学真理，同时避免悖论——“真理，全部真理，而且只有真理”。这样的目标对数学家来说是自然而然的，因为它会让他们的工作立于更坚实的地基之上。也正因如此，当 Gödel 用他的不完备性定理给 Hilbert 纲领以致命一击时，这是一场震撼性的事件：这样一个完备且一致的数学系统根本不可能存在！

尽管这样一项不可能性结果本应进一步加深那场存在性危机，数学家们却很快恢复过来，继续前行：对朴素集合论的改进，例如罗素的类型论，被提了出来；而尽管由于 Gödel 的结果，这类系统仍然无法被形式地证明为一致，人们却大多相信它们是一致的，事实也证明那些基础裂缝对人们所关心的那类数学几乎没有影响。事实上，类型论已经发展得如此成熟，以至于它构成了 Lean 这类交互式定理证明器的基础，使得越来越多的数学内容可以用计算机语言形式化，从而让证明能够由程序自底向上地自动检查。

除了公理系统之外，Hilbert 还在他的纲领中提出了一个相关目标：发展一种算法，自动判定任何数学命题的真假，从而把定理证明化约为对规则的机械应用。这一目标也被 Alan Turing 证明是不可能的，那是在他关于停机问题不可判定性的里程碑式证明中，而该证明催生了计算机科学这一丰饶领域。这是一个颇具诗意的矛盾：在确立 Hilbert 纲领之不可能的同时，Gödel 和 Turing 创造出了尽可能强大的计算机器。

自 Hilbert、Gödel 和 Turing 的时代起，一个世纪已经过去。出乎一切预料，我们如今正目睹 Hilbert 的“证明机器”化为现实，其化身是 AI agent，配备了在 Lean 这类证明助手中找到的机械化形式系统。这一发展，事实证明，对数学界的冲击远比 Hilbert 纲领的崩塌更为猛烈。我不确定 Hilbert 本人是否考虑过他的纲领若成功会带来什么后果，但 von Neumann 展现出了惊人的先见之明¹：

当不可判定性失效时，今天所理解的数学就不复存在；取而代之的将是一套绝对机械的规定，借助它，人们可以判定任何给定语句是否可证。

我不是数学家，而是计算机科学家。在计算领域，AI 的冲击没有那么剧烈，大多数人甚至为之欢呼，以越来越快的速度源源不断地生成代码。然而我所感受到的，是一种放任自流的气氛：如今，不再阅读 AI 生成的代码正逐渐成为标准做法。这对计算机科学而言是一场巨大的悲剧。我们是极少数有可能彻底弄清事物底层的学科之一——只要有源代码，我们就能确切理解一个程序在做什么，可我们现在却要放弃这一点！我们现在拥有了能够做到 Hilbert 所梦想的一切的机器，却抛弃了他视为科学之灵魂的东西：

我们绝不能相信那些人——他们今天带着哲学家的姿态和审慎的语气，预言文化的衰落，并接受 ignorabimus（我们不可知）。对我们而言，不存在 ignorabimus，在我看来，自然科学中根本不存在任何 ignorabimus。与愚蠢的 ignorabimus 相对，我们的口号应当是 Wir müssen wissen – wir werden wissen（“我们必须知道——我们将会知道”）。

作为计算机科学家，我们应当思考数学界正在发生的事：拒绝阅读一个通过了所有测试——甚至通过了形式验证——的程序的代码，无异于一旦 AI 在 Lean 中解出一个定理就无视其证明。事实上，从字面意义上说，二者是同一回事，因为根据 Church-Howard 对应，程序即证明，而 Lean 这类定理证明器正是这样运作的。当 AI 生成的证明长得读不完时，数学家不会放弃理解它，而是费尽心力去简化证明，直到它变得可消化。我们在计算领域也必须采取同样的态度：运用抽象、重构、收窄范围、发明并采用更高层的语言，直到我们能把代码装进脑子里。

我不知道 AI 最终是否会在所有活动中超越人类——我相信我们是用大脑思考的，而大脑不过是架构不同的生物计算机——但我知道，如果我们把思考拱手让给机器，结局会很糟。想想那些日益增多的案例：人们因依赖 AI 提供医疗建议而失去生命。我们越是把机器的话视为理所当然，就越无法掌控自己的命运。我们必须知道——我们将会知道。

Zur Hilbertschen Beweistheorie，译文见 Philip Welch 的 Turing Centenary Lecture。↩︎