文章借 Hilbert 计划与 Lean 形式化证明，主张用抽象与重构理解 AI 生成代码

100年前，数学世界经历了一场基础性危机：人们发现了好几个悖论，这暴露出支撑所有数学领域的支柱上的裂缝。其中最著名的是罗素悖论，它指向矛盾的“所有不包含自身的集合之集”，从而揭示了朴素集合论的不一致性。这促使数学家去寻找一个没有矛盾的数学严格基础。特别地，大卫·希尔伯特启动了一项计划，旨在设计一套完备且一致的公理系统，也就是说，人们应该能够从这些公理推导出所有数学真理，同时避免悖论——“真相、全部真相，而且只有真相”。对数学家来说，这样的目标很自然，因为它能使他们的工作建立在更坚实的基础之上。因此，当哥德尔以其不完备定理给希尔伯特计划致命一击时，也同样是一件轰动数学界的大事：这样的完备、一致的数学系统不可能存在！

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

除了公理系统之外，希尔伯特还在他的计划中提出了一个相关目标：开发一种算法，自动判定任何数学陈述的真假，从而将定理证明化为规则的机械应用。艾伦·图灵也证明了这个目标不可能实现——他提出了停机问题不可判定性的里程碑式证明，并由此催生了富有成果的计算机科学领域。颇具诗意的一处矛盾在于，在确立希尔伯特计划不可能实现的同时，哥德尔和图灵还创造了世界上最强大的计算机。

自希尔伯特、哥德尔和图灵的时代以来，一个世纪已经过去。尽管困难重重，我们如今正见证希尔伯特“证明机器”的实现——它化身为由 Lean 等证明助手中的机械化形式系统武装起来的 AI 智能体。结果表明，与希尔伯特计划的崩溃相比，这一发展对数学界造成的影响要更具毁灭性。我不确定希尔伯特本人是否考虑过如果他的计划成功会带来什么后果，但冯·诺依曼展现出了非凡的远见¹：

一旦不可判定性不再成立，那么今天人们所理解的数学便不复存在；取而代之的将是一种完全机械化的规则，借助它，人们便可以判定任何给定的句子是否可证明。

我不是数学家，而是计算机科学家。在计算机领域，AI 带来的冲击没那么剧烈，甚至大多数人都为它欢呼，看着它以越来越快的速度批量生成代码。然而，我感受到的是一种弃守的氛围：不再阅读 AI 生成的代码，如今正成为标准做法。这是计算机科学的一大悲剧。我们是极少数能够将事情追究到底的学科之一——只要拥有源代码，我们就能确切理解程序做了什么，然而现在却正在放弃这一点！我们如今拥有了能够实现希尔伯特一切梦想的机器，却抛弃了他所认为的科学灵魂：

我们绝不能相信那些今天摆出哲学家的姿态、以深思熟虑的语调预言文化衰落并接受 ignorabimus 的人。对我们来说不存在 ignorabimus，在我看来，自然科学中更是完全不存在。与愚蠢的 ignorabimus 相对立，我们的口号应当是 我们必须知道——我们终将知道（“我们必须知道——我们终将知道”）。

作为计算机科学家，我们应该审视数学领域正在发生的事：拒绝阅读一个通过所有测试——甚至通过形式化验证——的程序的代码，就如同 AI 在 Lean 中解出一个定理后，我们立刻无视证明一样。事实上，从字面意义上说，两者是一样的，因为根据丘奇—霍华德对应，程序就是证明，而定理证明器（如 Lean）正是这样运作的。当 AI 生成的证明长到无法阅读时，数学家不会放弃理解它，而会费尽心思简化证明，直到它易于理解。我们在计算领域也必须采取同样的态度：使用抽象、重构、细化范围、发明并采用更高层的语言，直到我们能够在脑中完整容纳这些代码。

我不知道 AI 最终是否会在所有活动上超越人类——我认为，我们是用大脑思考的，而大脑不过只是采用不同架构的生物计算机——但我知道，如果我们放弃思考，把思考交给机器，最终一定会落得很惨。想想越来越多人因依赖 AI 提供医疗建议而丧生的案例：我们越是把机器的话当真，对自己命运的掌控就越少。我们必须知道——我们终将知道。

论希尔伯特的证明理论，译文见 Philip Welch 的图灵百年纪念讲座。↩︎