我们必须知道——我们必将知道

# 我们必须知道——我们终将知道 来源：https://remy.wang/blog/hilbert.html 100 年前，数学界经历了一场基础危机：若干悖论的发现，揭示了支撑数学各个领域的支柱中存在的裂缝。其中最著名的是罗素悖论，它指出“所有不包含自身的集合所构成的集合”存在矛盾，从而表明朴素集合论是不一致的。这促使数学家为数学寻找一个严谨且无矛盾的基础。特别是，大卫·希尔伯特发起了一项计划，旨在设计一个完备且一致的公理系统，也就是说，人们应当能够从这些公理推导出所有数学真理，同时避免悖论——“真理、全部真理，而且只有真理”。这样的目标对数学家而言十分自然，因为它能让他们的工作建立在更加坚实的基础之上。因此，当哥德尔以不完备定理给予希尔伯特计划致命一击时，同样引发了一场巨震：这样一个完备且一致的数学系统不可能存在！ 尽管这样的不可能性结果本应进一步加深这场生存危机，数学家们却很快恢复过来，继续前行：人们提出了对朴素集合论的改进，例如罗素的类型论；虽然由于哥德尔的结果，这些系统的一致性仍然无法得到形式化证明，但人们普遍相信它们是一致的，而且事实表明，这些基础上的裂缝对人们所关心的数学几乎没有影响。事实上，类型论如今已经相当成熟，成为 Lean 等交互式定理证明器的基础，使得越来越多的数学内容可以用计算机语言进行形式化，从而让程序能够从最基础的层面开始自动检验证明。 除了公理系统，希尔伯特还在他的计划中提出了一个相关目标：开发一种算法，自动判定任意数学命题的真假，从而将定理证明归结为机械地应用规则。艾伦·图灵也证明了这一目标不可能实现，他关于停机问题不可判定性的里程碑式证明，催生了计算机科学这一硕果累累的领域。颇具诗意的矛盾在于，哥德尔和图灵在确立希尔伯特计划的*不可能性*时，却创造了最强大的、*能够*做到这一切的计算机器。 自希尔伯特、哥德尔和图灵的时代以来，一个世纪已经过去。出乎所有人的意料，我们如今正在见证希尔伯特的“证明机器”成为现实，其化身便是配备了 Lean 等证明助手中的机械化形式系统的 AI 智能体。事实证明，与希尔伯特计划的破灭相比，这一发展对数学界造成了更具毁灭性的影响。我不确定希尔伯特本人是否考虑过他的计划若是成功会带来什么后果，但冯·诺依曼展现出了惊人的先见之明1 (https://remy.wang/blog/hilbert.html#fn1)： > 当不可判定性不再成立时，今天人们所理解的数学也就不复存在；取而代之的将是一套完全机械化的规程，借助它，人们可以判定任意给定的语句是否可证。 我不是数学家，而是一名计算机科学家。在计算领域，AI 带来的冲击没有那么剧烈，大多数人甚至在为它欢呼，以越来越快的速度产出代码。然而，我感受到的却是一种放弃的氛围：不再阅读 AI 生成的代码，如今正逐渐成为一种惯例。这对计算机科学而言是一个巨大的悲剧。我们是极少数能够彻底刨根究底的学科之一——只要拥有源代码，我们就能准确理解一个程序在做什么，然而我们如今却在放弃这一点！我们现在拥有了能够实现希尔伯特所有梦想的机器，却抛弃了他视为科学灵魂的东西： > 我们不能相信那些如今摆出哲学姿态、用深思熟虑的语调预言文化衰落，并接受*我们将永远无法知道*的人。对我们而言，不存在*我们将永远无法知道*，而且在我看来，自然科学中也根本不存在这样的事。为了反对这种愚蠢的不可知论，我们的口号应当是*我们必须知道——我们终将知道*（“我们必须知道——我们终将知道”）。 作为计算机科学家，我们应当思考数学界正在发生的事情：一个程序通过了所有测试——甚至通过了形式化验证——就拒绝阅读它的代码，这无异于 AI 在 Lean 中证明了一个定理后，便对证明本身不闻不问。事实上，从字面意义上说，两者就是一回事，因为根据丘奇–霍华德对应，程序就是证明，而这正是 Lean 等定理证明器的运作方式。当 AI 生成的证明长到难以阅读时，数学家不会放弃理解它，而是煞费苦心地简化证明，直到它变得易于理解。我们在计算领域也必须采取同样的态度：使用抽象、重构、细化范围、发明并采用更高层次的语言，直到我们能够把代码装进脑海里。 我不知道 AI 最终是否会在所有活动中超越人类——我相信我们用大脑思考，而大脑只是采用了不同架构的生物计算机——但我知道，如果我们放弃思考，把它交给机器，结局一定会很糟。想想那些因依赖 AI 的医疗建议而丧命的案例，它们正在不断增多：我们越是不加思索地相信机器的话，就越无法掌控自己的命运。*我们必须知道——我们终将知道*。 --- 1. *论希尔伯特证明论* (https://eudml.org/doc/167910)，译文见 Philip Welch 的图灵百年纪念讲座 (https://people.maths.bris.ac.uk/~mapdw/ecms2.pdf)。↩︎ (https://remy.wang/blog/hilbert.html#fnref1)