奥地利逻辑学家库尔特·哥德尔（Kurt Gödel）是20世纪最具原创性的思想家之一。他于1931年提出的不完备定理彻底重塑了数学界，并为数字时代奠定基础。然而，在1930年代取得开创性成果后，哥德尔公开发表的论文寥寥无几，其留下的数万页未出版手稿长期引发科学史学界关注。
自2017年起，赫尔辛基大学逻辑学家扬·冯·普拉托（Jan von Plato）领导团队解读哥德尔1940年代初撰写的16本“工作簿”。这些共计1009页的手稿密密麻麻写满数学与逻辑推演，且大多采用已过时的加贝尔斯伯格（Gabelsberger）德文速记法。由于解读难度极大，团队此前每周仅能破译一页。
AI介入：几天完成人类数年工作量
转折发生在今年9月。冯·普拉托向人工智能模型Claude寻求帮助。短短几天内，Claude不仅提供了全套材料的全面摘要，更揭示出哥德尔已证明了数百个鲜为人知的定理。
“我惊呆了，”冯·普拉托表示，“这些工作簿不仅包含数十项预见20世纪70至80年代才问世成果的洞见，还涉及14个未被深入研究的逻辑主题。哥德尔远远超越了那个时代。”
冯·普拉托于2017年启动该项目，初衷是为了应对从赫尔辛基大学强制退休的局面。他自学加贝尔斯伯格速记法——自称全球仅六人掌握——并组建小型团队，获得欧洲研究委员会250万欧元资助。今年8月，在法国一场关于AI与定理证明的会议上，计算机科学家建议他利用Claude辅助解读。回到赫尔辛基后，他将转录文本及此前撰写的六本相关著作输入模型。
“几天内，我就收到了一份650页的工作簿解释。虽然必须逐页核对，但这基本上是一项人类无法独立完成的工作，”冯·普拉托指出，“人类一次只能读一页，往往忘记前文，一年仅能阅读约50页，无法在脑海中统筹全局。而AI能将千页内容连接起来，将哥德尔的所有著作视为一个整体。”
重构历史：证实哥德尔早于科恩触及核心证明
哥德尔的不完备定理表明，在任何数学系统中，都存在既不能被证明也不能被证伪的真命题。这一发现激励艾伦·图灵撰写1936年论文，开启现代计算理论。1966年，美国数学家保罗·科恩因证明连续统假设和选择公理的独立性获得菲尔兹奖。当时哥德尔曾回应称，自己早在1940年代就已证明该结果，但未能从笔记中重构完整证明以服众。
冯·普拉托交给Claude的首要任务，便是核查工作簿中是否存在选择公理独立性的证明。结果显示：几乎肯定存在。“他只是差一步，”冯·普拉托分析道，“有一个定义哥德尔搞错了，但他两年前已有正确定义。若再坚持几个月，他最终会得出正确结论。其证明结构美妙，使集合论结果遵循统一模式。”
当Claude展示重构的证明后，冯·普拉托将其输入Coq证明辅助程序进行验证，结果顺利通过。冯·普拉托认为，若哥德尔当时发表该工作，理应获得1940年的菲尔兹奖。“也许他觉得科恩获奖是一种错失。”
海量发现：663个定理待挖掘
在进一步交互中，冯·普拉托要求Claude提取工作簿中所有哥德尔拥有证明、草拟证明或构思思路的定理。AI共找出663个。经Coq验证：约400个原样通过；约200个经修正后通过（需更精确陈述或补充假设）；约50个被判定错误。这与哥德尔本人在笔记中标注的“falsch!”（错误！）或“schlecht!”（糟糕！）相符。
印第安纳大学圣母院学院逻辑学教授乔尔·戴维·汉金斯（Joel David Hamkins）尚未看到重构证明，但他表示，若该证明站得住脚，“将是非凡且具有历史意义的”。他指出，笔记中有类似科恩证明的内容，表明哥德尔走在正确道路上，尽管历史学家仍需界定AI与哥德尔各自的贡献比例。
冯·普拉托相信，继续研究手稿将揭示更多宝藏。Claude指出，工作簿中包含十多个过去80多年间未被发现的逻辑和数学基础主题。此外，哥德尔的物理和宇宙学笔记本仍是一片未知领地，冯·普拉托计划在完成当前逻辑项目后着手探索。