一百年前数学基础危机：罗素悖论与希尔伯特计划的兴衰

100年前，数学界经历了一场基础危机：若干悖论的发现揭示了支撑数学各个领域的支柱上存在的裂缝。其中最著名的是罗素悖论，它指向那个自相矛盾的“所有不包含自身的集合的集合”，从而表明朴素集合论的不一致性。这促使数学家们为数学寻找一个严格且无矛盾的基础。特别是，大卫·希尔伯特发起了一项纲领，旨在设计一套完备且一致的公理系统，意思是人们应当能够从公理中推导出所有数学真理，同时避免悖论——“真理，全部真理，除了真理别无他物”。这样的目标对数学家来说是自然的，因为它将把他们的工作置于更坚实的基础上。因此，当哥德尔用他的不完备性定理对希尔伯特的纲领给予致命一击时，这也是一场地震般的事件：这样一个完备且一致的数学系统不可能存在！

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

除了公理系统，希尔伯特还在他的纲领中提出了一个相关目标：发展一种算法来自动判定任何数学陈述的真假，从而将定理证明归结为规则的机械应用。这个目标也被艾伦·图灵证明为不可能，他在停机问题不可判定性的里程碑式证明中催生了计算机科学这一丰饶领域。这是一个颇具诗意的矛盾：在确立希尔伯特纲领之不可能性的过程中，哥德尔和图灵创造了最强大的计算机器，而它们恰恰能够做到。

自希尔伯特、哥德尔和图灵的时代起，一个世纪已经过去。排除万难，我们现在正目睹希尔伯特“证明机器”的实现，它以 AI agent 的形式化身，配备着 Lean 等证明助手中的机械化形式系统。这一发展，事实证明，对数学界的影响远比希尔伯特纲领的崩塌更具毁灭性。我不确定希尔伯特本人是否考虑过他的纲领若成功会带来什么后果，但冯·诺伊曼展现了惊人的先见之明¹：

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

我不是数学家，而是计算机科学家。在计算领域，AI 的冲击没有那么猛烈，大多数人甚至为之欢呼，以越来越快的速度生成代码。然而我所感受到的，是一种放任的气氛：不读 AI 生成的代码正在成为标准做法。这对计算机科学来说是一场巨大的悲剧。我们是极少数能够探究事物最底层的学科之一——只要有源代码，我们就能确切理解一个程序在做什么，然而我们现在正在放弃这一点！我们现在拥有了能够实现希尔伯特所梦想的一切的机器，但我们却放弃了他视为科学灵魂的东西：

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

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

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

Zur Hilbertschen Beweistheorie，译文见于 Philip Welch 的图灵百年纪念讲座。↩︎