芬兰逻辑学家Jan von Plato把哥德尔1940年后16本工作簿、共1009页的转写稿交给Claude。据他在维也纳大学的演讲，Claude几天内给出一份从650页扩到1084页的解读，并列出663条具备定理雏形的结果。在Josef Urban等人协助做形式化验证后，约400条完全成立，约200条核心思路正确但需要前置假设，55条有误，另有几条仍在核验。
速记先由人转录，Claude读的是英文稿
哥德尔1978年去世，留下此前未发表的大量手稿。1931年的不完备定理影响了图灵，此后他的工作笔记却用加贝尔斯贝格速记写成，全球能读的人很少。von Plato在2017年接近强制退休时启动这项工作，并申请到欧洲研究理事会250万欧元资助。他说，现在全世界能读这种速记的大概只有六个人，自己是其中一个。
他锁定的是哥德尔1940年定居普林斯顿之后的16本工作簿。von Plato发现当时的AI读不懂速记，转录必须人工完成。团队花了数年把笔记转成现代英文。即便如此，笔记高度压缩、跳跃很快，人工进度大约每周一页、一年约50页。今年夏天，法国一场“AI与定理证明”会议上，几位计算机科学家建议他试Claude。教授随后把1009页转写稿、自己的6本专著，以及一批现代逻辑学文献一起交给模型。更多模型进展见AI资讯。
663条雏形，约400条被证明成立
von Plato把Claude称作具有“莫扎特式”视野的数字工具：人读到后面会忘掉前面，模型可以把上千页笔记和相关文献放在同一次上下文里对照。报道称，它先整理出663条具备定理雏形的结果。形式化验证之后，约400条完全成立，约200条思路正确、但要补上前置假设，55条是错的。按这个节奏回看，哥德尔在1940年代初抵美后不到三年里，大约每两天就有一条新结果。
选择公理：架构在，定义写错一行
选择公理长期悬而未决：它能不能从其他基础公理推出来。1963年，Paul Cohen用力迫法证明了它的独立性，并于1966年获得菲尔兹奖。典礼上Alonzo Church公开说，哥德尔早在1942年就在类型论框架下证明了可构成性公理的独立性，并相信可以推广到选择公理，后来兴趣转向哲学。Cohen本人2002年回忆，当面询问时哥德尔承认有一套方法，但否认与类型论有关，而且不肯透露细节。1967年6月30日，哥德尔在给W. Rautenberg的信里说，自己当年只得到“部分结果”。王浩也曾写到，哥德尔后悔没有把这项工作做完。
Claude的解读是：哥德尔在Cohen之前20多年已经构造出等价的数学架构，用一串无穷的0和1表示“可能世界”，再用对角线论证说明其中不存在那样的选择函数。卡住的是定义。报道称，他在关键的“有限支撑”上一行写错了；笔记另一处其实写过正确定义，1960年代重看时他忘了。von Plato把Claude还原的证明交给证明助手Coq，结果全部通过。他把这篇人机合著论文发给哥德尔专家金森晶宏（Akihiro Kanamori）。金森当时不知道有AI参与，读后认为它在数学和历史上都很敏锐。
笔记里还有量子测量和时间闭环
同一批笔记里，还有一些要到1970、1980年代才被重新发现的逻辑结果，例如构造性公理的独立性和函数解释中的强规范化。Claude还列出14个至今仍少有人做的题目，并展开成约50页大纲。
物理学部分更靠后。1935年爱因斯坦、波多尔斯基、罗森发表EPR论文，质疑量子力学是否完备；报道称波多尔斯基前一年听过哥德尔讲不完备性。哥德尔1935年原计划研究量子力学，后来转向集合论。Claude在笔记里看到，他计算过耦合系统测量后的状态变化，用的不是1932年冯·诺依曼的办法，而是后来被称为吕德斯规则的更新方式。吕德斯1951年才正式提出这条规则。
1949年，哥德尔给出爱因斯坦场方程的一个解：宇宙整体在旋转，离轴足够远时光锥倾斜，时间可以绕成闭环。Claude读完后的判断是，他不是随口一说。笔记里有他翻过的天文观测，试图用统计看星系旋转平面是否存在科里奥利力造成的偏差。1978年，哥德尔因拒绝食用非妻子烹制的食物、最终饥饿去世。
常见问题
Q：Claude是直接读哥德尔的速记原件吗？ A：不是。加贝尔斯贝格速记先由Jan von Plato团队用数年转成现代英文。Claude读的是这1009页转写稿，以及教授的专著和现代文献。
Q：到底新证出了多少条定理？ A：报道中的细账是663条定理雏形。形式化验证后约400条完全成立，约200条思路正确但需要前置假设，55条有误，还有几条未核完。开头流传的“440多条”不如这组数字精确。
Q：哥德尔有没有比Cohen更早证明选择公理独立？ A：Claude还原出的架构和Cohen后来的证明等价，但哥德尔在“有限支撑”的定义上写错一行，正式证明仍是Cohen在1963年完成的。还原后的证明已通过Coq验证。
相关文章
