Claude 读完了哥德尔的速记笔记，Coq 判了 50 条定理不成立

一周一页。这是赫尔辛基逻辑学家 Jan von Plato 啃哥德尔 1940 年代初笔记的速度。16 本工作笔记，全是 Gabelsberger 速记，全世界能读的大概就六个人。von Plato 从 2017 年开始做，拿的是 250 万欧元的 ERC 经费。今年 9 月，von Plato 把转写稿、自己写的六本书和二手文献一起丢给 Claude，几天后拿回一份 650 页的解读，按 von Plato 的说法是逐页核对过的。《卫报》的报道：https://www.theguardian.com/science/2026/nov/13/kurt-godel-notebooks-ai-helps-unlock-hidden-discoveries-man-who-transformed-maths

最大的发现，是一个几乎完整的选择公理独立性证明，那个年代最重要的悬案之一。里面有一个定义写错了，正确版本出现在两年前的另一本笔记里。von Plato 把重建后的证明丢进 Coq 证明助手，通过了。接着是更大的任务：把哥德尔证过的、勾勒过的、有过想法的定理全列出来。Claude 找出 663 条。放进 Coq 一跑，约 400 条原样成立，约 200 条需要修补，要么把表述收紧，要么补一个前提，还有约 50 条直接是错的。Claude 还标出了十几个哥德尔没继续往下走的逻辑学方向。

这些数字都是 von Plato 的说法，经《卫报》转述，论文还没出。圣母大学的 Joel David Hamkins 没看过这份重建，但泼的冷水很到位：多少是 Claude、多少是哥德尔，得交给历史学家判；而且你没告诉任何人的工作，是拿不到功劳的。

真正该记住的是那 50 条。一个能以超人广度读速记、读档案的模型，会产出很多看起来很自信的定理，这里大约每 13 条就有一条是错的。让整件事可信的不是模型，是逐页核对的人，加上一个完全不在乎解释写得多漂亮的证明检查器。读，已经变便宜了。验证才是贵的、值钱的那一步，而在数学里，这一步已经有机器了。

说明：clauday 的内容由 Claude 参与撰写。