“领先于他的时代”：AI 揭开改写数学的人笔记本里隐藏的发现

奥地利逻辑学家库尔特·哥德尔是 20 世纪最具原创性的思想家之一。他在 1931 年发表的两条不完备性定理改变了数学的面貌，也为数字时代铺平了道路。

在 1930 年代取得那些开创性成果之后，哥德尔只发表了几篇论文。但他未发表的手稿多达数万页，科学史学者对此极感兴趣。

2017 年起，芬兰逻辑学家扬·冯·普拉托在赫尔辛基大学主持一个项目，解读哥德尔在 1940 年代初写下的 16 本笔记。这批被称为“工作笔记”的材料共 1,009 页，内容密集，讨论数学与逻辑。其中很大一部分用的是德文速记法加贝尔斯贝格体，这种速记法在哥德尔使用它的时候就已经过时了。

对文本的数学解读进展极其缓慢，大约一周一页，直到 9 月冯·普拉托请 AI 模型 Claude 帮忙。两天之内，Claude 就给出了全部材料的完整摘要，显示哥德尔证明过数百条无人知晓的定理。

这位现代最著名的逻辑学家，实际发现的成果远比任何人以为的要多。

阿尔伯特·爱因斯坦在普林斯顿大学向库尔特·哥德尔（右二）颁奖，两人后来成为朋友。图片由 Bettmann/Bettmann Archive 提供

“我惊呆了，”冯·普拉托说。“这些笔记里不仅有几十处结果在 70 年代和 80 年代才被重新发现，还包含 14 个至今无人继续研究的逻辑主题。哥德尔远远走在了他的时代前面。”

哥德尔改变了逻辑学的走向，因为他揭示了数学知识的边界。他的不完备性定理表明，在一切数学系统中都存在既无法证明也无法证伪的真命题。此前几代逻辑学家曾希望一切真理都可验证，这一结果对他们是个打击；但哥德尔的工作把这一领域推向了新的方向，启发了艾伦·图灵写下 1936 年那篇开创现代计算理论的论文。

1940 年，哥德尔在纳粹统治下逃离了奥地利。他定居新泽西州普林斯顿，在高等研究院与阿尔伯特·爱因斯坦结为密友。晚年他愈发多疑，拒绝吃不是妻子亲手做的食物，1978 年死于饥饿。

冯·普拉托说，他 2017 年启动哥德尔项目，是因为即将从赫尔辛基大学强制退休。“我该做点什么让自己变得不可或缺？对了，我要开始读哥德尔那些神秘的速记页！”他拿到了欧洲研究理事会 250 万欧元（210 万英镑）的资助，自学了加贝尔斯贝格速记法。他说，“全世界能读懂这种速记的只有六个人，我是其中之一。”随后他组建了一个小团队。

8 月，在法国一场关于 AI 与定理证明的会议上，冯·普拉托遇到了几位计算机科学家，他们建议他借助 Claude 来解读这些笔记本。回到赫尔辛基后，他着手推进，把自己对笔记本的转录稿、此前写过的六本关于哥德尔的书，以及其他二手科学文献一并交给 Claude。

“几天之内，我就看到了一份 650 页的笔记本解读。每一页都必须逐一核对，但这基本上是人类无法完成的工作，”他说。“人一次只能读一页，而且容易忘。读完大约 50 页要花我们一年时间。我们根本没法把所有不同的部分同时记在脑子里。

“AI 能把上千页里的所有片段串联起来。它可以把哥德尔的所有文字看成一个整体。”

哥德尔某本笔记本中速记样本的缩微胶片图像。图片由高等研究院（Institute for Advanced Study）提供

哥德尔的不完备性定理揭示了这样一类命题的存在，它们的真值独立于所在的形式系统，也就是说，在该系统内既无法证明也无法证伪。1966 年，美国数学家保罗·科恩证明了连续统假设与选择公理这两个著名命题的独立性，并因此获得数学界最高荣誉菲尔兹奖。

哥德尔得知科恩获得菲尔兹奖后说，他早在 1940 年代就已经证明了这个结果。然而当同行要求他给出证明时，哥德尔却无法从自己的笔记中重建出来。

冯·普拉托交给 Claude 的第一项任务，是查明哥德尔的工作笔记中是否存在选择公理独立性的证明。若有，就能证实哥德尔 1966 年说的是真话。答案回来了，有，几乎有。“他只差一步，”冯·普拉托说。“有一个定义哥德尔弄错了，但两年前他手里还是正确的定义，所以大家认为，只要他再多做几个月，本来也会得到正确的定义。在我看来，他这套证明的结构实在漂亮，它让集合论的这些结果全都遵循同一个模式。

“尤其让我震动的是，他从想法出发。他不像那种摆弄公式、指望碰巧走到某处的人。他的想法非常非常清晰，然后有条不紊。一步一步往前走，最终实现了他在这一形式化工作中设定的目标。”

冯·普拉托说，Claude 把重建出的选择公理独立性证明交给他时，他把它交给证明助手 Coq 验证，Coq 是一个检查数学证明是否有效的程序，结果通过了。冯·普拉托认为，如果哥德尔当年把关于选择公理的工作发表出来，他本会拿下 1940 年的菲尔兹奖。“也许他觉得，科恩拿到奖的时候，那多少是他错过的东西。”

在后来的讨论中，冯·普拉托让 Claude 提取笔记中所有哥德尔给出过证明、勾画过证明或有过证明思路的定理。Claude 找到了 663 条。把这些结果放进 Coq 之后：“大约 400 条按原陈述通过验证，大约 200 条经过修补，也就是说，定理的陈述可能需要写得更精确，或者需要补充某些假设。大约 50 条是错的，这并不奇怪。哥德尔自己重读笔记时，偶尔也会在页边添一句“falsch!”（错误）或“schlecht!”（糟糕）。”

冯·普拉托补充道：“我相信，继续研究哥德尔的手稿还会发现更多宝藏。Claude 说，这些笔记本里包含十几个逻辑和数学基础方面的主题，而这些主题自被写下以来的 80 多年里从未有人发现过。所以这是一个值得探索的方向。但还有很多其他内容。他的物理学和宇宙学笔记本是一片未知领域，我打算完成目前的逻辑项目后就开始探索。”

印第安纳州圣母大学逻辑学教授乔尔·戴维·哈姆金斯尚未看过 Claude 对哥德尔关于选择公理独立性证明的重构，但他表示，如果这一重构站得住脚，“那将非同寻常，在历史上也很有意义。不过，其中有多少是 Claude 的功劳、多少是哥德尔的功劳，则是历史学家的工作。”

哈姆金斯说：“笔记本里存在与[科恩的证明]相似的内容，并不意味着他已经完成了它。这表明他当时正走在这条路上。你没有告诉任何人的工作，不会为你赢得功劳。但哥德尔有如此多开创性的想法，所以他的笔记本里充满令人兴奋的内容，也许并不令人意外。”