11 月 13 日，《卫报》报道，赫尔辛基大学逻辑学家 Jan von Plato 领导的团队借助 Anthropic 的 Claude 模型，破译了库尔特·哥德尔（Kurt Gödel）写于 20 世纪 40 年代初的 16 本工作笔记，发现这位不完备定理的提出者证明了数百条此前无人知晓的定理，其中包括一个与后来获菲尔兹奖的工作仅差一步的选择公理独立性证明。
一周一页到几天全部读完
哥德尔 1978 年去世后留下数万页未发表手稿，其中这 16 本「工作手册」共 1,009 页，大部分用早已失传的德语速记体 Gabelsberger 写成——von Plato 自学了这种速记，自称「全世界只有六个人能读」。自 2017 年起，他的团队借助欧洲研究理事会 250 万欧元资助推进解读，进度约为每周一页。
转折发生在今年 9 月。8 月，von Plato 在法国一场 AI 与定理证明的会议上遇到计算机科学家，对方建议他试试 Claude。他把手稿转录、自己写的六本哥德尔专著及相关二手文献喂给模型，几天内就得到了一份 650 页的完整解读。
「我惊呆了。」von Plato 说，「这些手册不仅包含数十条直到七八十年代才被证明的结果的预演，还有 14 个逻辑学主题至今没人研究过。哥德尔远远走在了时代前面。」他补充道，人工解读一年只能读约 50 页，「人类一页一页读还会遗忘，而 AI 能把一千页里的所有片段连起来，把哥德尔的全部写作看作一个整体。」
与菲尔兹奖擦肩的证明
第一个任务是验证一桩悬案：1966 年，美国数学家 Paul Cohen 因证明连续统假设与选择公理的独立性获菲尔兹奖，哥德尔当时回应自己早在 40 年代就已证明，但被同行追问时未能从笔记中重构出证明。Claude 在手稿中找到了答案：是的，几乎完成——只有一个定义写错了，而哥德尔两年前用过正确定义，「再继续几个月就能得到」。von Plato 把 Claude 重构的证明送进证明助手 Coq 验证，通过了。他认为如果哥德尔当年发表这项工作，1940 年的菲尔兹奖就是他的。
Claude 还从手稿中提取出哥德尔有证明、有证明梗概或有证明思路的定理共 663 条。送入 Coq 后：约 400 条原样通过，约 200 条经修正后通过（如补全条件或收紧表述），约 50 条是错的——von Plato 说这不足为奇，哥德尔自己重读笔记时也会在页边批注 falsch!（错误）或 schlecht!（糟糕）。
学界：功劳算谁的，交给历史学家
未参与项目的圣母大学逻辑学教授 Joel David Hamkins 表示，如果这一重构证明站得住脚，「将是了不起且具有历史意义的发现。不过其中多少归 Claude、多少归哥德尔，是历史学家的工作」。他提醒：「笔记里存在与（Cohen 证明）相似的东西，不等于他完成了它，只能说明他走在路上。没有告诉任何人的工作不会被记入功劳——但哥德尔的开创性想法太多了，笔记里满是激动人心的内容也许并不奇怪。」
哥德尔 1931 年发表的不完备性定理揭示了任何足够强的数学系统中都存在不可判定命题，启发了图灵 1936 年奠基现代计算理论的论文。他 1940 年逃离纳粹统治下的奥地利，定居普林斯顿高等研究院，与爱因斯坦结为挚友。von Plato 表示，手稿中仍有十多个 80 多年间无人发现的逻辑学与数学基础主题待挖掘，哥德尔的物理学与宇宙学笔记则是他下一步要探索的「未知领域」。
核心总结
- 赫尔辛基大学团队用 Claude 解读哥德尔 1,009 页 Gabelsberger 速记笔记，人工进度每周一页，Claude 几天内产出 650 页完整解读
- Claude 提取出 663 条有证明基础的定理：Coq 验证约 400 条原样通过、约 200 条修正后通过、约 50 条有误
- 手稿中包含仅差一步的选择公理独立性证明，重构后通过 Coq 验证；哥德尔 1966 年曾自称早已证明但未能当场重构
- 手稿还包含数十条七八十年代结果的预演，以及 14 个至今无人研究的逻辑学主题
- 外部学者肯定其历史价值，同时提醒「多少归 Claude、多少归哥德尔」仍待历史学家评判
原文：‘Ahead of his time’: AI helps unlock discoveries hidden in notebooks of man who transformed maths（卫报，2026 年 11 月 13 日）
