AI 解开了哥德尔手稿

赫尔辛基大学的 Jan von Plato 从 2017 年起啃哥德尔 1940 年代初的 16 本手稿，1009 页全是过时的德语速记，人工一年只能看 50 页；今年 9 月他改用 Claude 梳理，几天就拿到 650 页解释，一共提取出 663 个定理，Coq 验证后约 400 个成立、约 200 个要修正、约 50 个是错的；最重磅的是哥德尔当年离证明选择公理独立性只差一步，这个结果后来由科恩在 1966 年拿了菲尔兹奖。

来源：https://www.theguardian.com/scie ... o-transformed-maths