AI 解析戈德尔未发表手稿：发现数百个已证实定理及超前逻辑成果
奥地利逻辑学家库尔特·戈德尔（Kurt Gödel）留下的 1,009 页密集文字，长期以来是科学史学家研究的难点。自 2017 年起，芬兰赫尔辛基大学逻辑学家 Jan von Plato 主持了一项旨在解读戈德尔 20 世纪 40 年代初撰写的 16 本“工作手册”的项目。
这些材料包含大量关于数学和逻辑的复杂论述，其中许多内容使用了一种名为 Gabelsberger 的德语速记法书写。这种速记法在戈德尔使用它时便已显得过时，导致文本的数学理解进展极为缓慢——团队此前每周仅能处理大约一页内容。
转折点出现在今年 9 月。Jan von Plato 引入了 AI 模型 Claude 协助研究。在几天之内，Claude 提供了对整个材料的综合摘要。这一突破揭示出，现代最著名的逻辑学家之一所发现的成果远超以往想象。
Plato 表示，工作簿中不仅包含了几十个直到 20 世纪 70 年代和 80 年代才被学界知晓的预期结果，还涵盖了 14 个未被后续研究者深入追求的逻辑主题。这表明戈德尔的思想远远超出了他的时代。
从人工转录到 AI 全景式阅读
为了推进研究，Plato 利用欧洲研究委员会提供的 250 万欧元资助，自学了 Gabelsberger 缩写，并组建了一个小团队。他是世界上仅有的六名能阅读该速记法的人之一。然而，面对浩如烟海的资料，人类记忆和处理能力存在局限。“我们花了一年时间阅读大约 50 页。我们只是无法记住所有不同的部分。”Plato 说道。
8 月，在法国一场关于人工智能和定理证明的会议上，Plato 遇到了计算机科学家。返回赫尔辛基后，他开始向 Claude 展示自己以前关于戈德尔及其他二级科学文献所写的六本书，以及工作簿的转录内容。
Claude 在几天内生成了一本 650 页工作簿的解释。Plato 指出，这基本上是人类不可能完成的工作量。人工智能能够连接成千上万页的部分，将戈德尔的所有著作视为一幅完整的画面进行整体把握。
验证选择公理独立性与定理提取
戈德尔的不完整性定理揭示了真理独立于其所在系统的陈述存在，即某些真实陈述既不能被证明也不能被反驳。这一理论激励了艾伦·图灵在 1936 年撰写论文，开启了现代计算理论。1940 年，戈德尔逃离纳粹统治下的奥地利，定居新泽西州普林斯顿，成为阿尔伯特·爱因斯坦在高级研究院的密友。晚年他因偏执拒绝进食非妻子制作的食物，于 1978 年死于饥饿。
1966 年，美国数学家保罗·科恩（Paul Cohen）因证明连续性假说和选择公理的独立性而获得菲尔兹奖章。戈德尔当时声称自己在 1940 年代已证明该结果，但无法从笔记中重建证明。
Plato 给 Claude 的第一个任务是确认戈德尔的工作簿中是否包含选择公理独立性的证明。Claude 的回答是：“是的，几乎。”Plato 解释称，戈德尔距离完整证明仅一步之遥，虽然有一个定义是错误的，但他两年前曾拥有正确的定义。Claude 重建的证明架构被认为具有统一模式，使得集合论结果得以连贯呈现。
当 Claude 向 Plato 展示重建的选择公理独立性证明时，该证明通过了 Coq 证明助手（一种验证数学证明有效性的程序）的检验。Plato 认为，如果戈德尔发表了关于选择公理的著作，他可能会赢得 1940 年的菲尔兹奖章。
在与 Claude 的进一步交互中，Plato 要求模型提取戈德尔已有证明、已绘制证明或仅有证明想法的内容。Claude 发现了 663 个相关条目。将这些结果输入 Coq 验证后：
- 约 400 个结果被完全验证；
- 约 200 个结果经过修复后成立（需更精确的定理陈述或添加假设）；
- 约 50 个结果为假。
值得注意的是，戈德尔本人在重读笔记时偶尔会添加边缘注释，如“错误！”或“schlecht! [坏的]”，这与 AI 识别出的部分无效结果相吻合。
学界反应与未来展望
印第安纳州圣母院大学的逻辑学教授 Joel David Hamkins 尚未查看 Claude 对戈德尔证明的重建细节，但他表示，如果该重建成立，将是显著且具有历史意义的发现。Hamkins 强调，存在类似科恩证明的结构并不意味着戈德尔拥有完整证明，但这表明他在探索道路上走得很远。鉴于戈德尔拥有众多突破性思想，其笔记本充满令人兴奋的内容并不奇怪。
Plato 补充道，继续研究戈德尔的手稿有望揭示更多宝藏。Claude 指出，这些课本包含了十多个逻辑和数学基础的主题。此外，戈德尔关于物理学和宇宙学的笔记本目前仍是未知领域，Plato 计划在完成当前的逻辑项目后开始探索这部分内容。
