AI 解锁哥德尔笔记本，揭示数百个已证明定理

芬兰逻辑学家 Jan von Plato 使用 Claude 处理了 Kurt Gödel 1940 年代 Gabelsberger 速记工作簿的 1,009 页内容，这项工作此前一直以每周约一页的速度推进。Claude 生成了一份 650 页的解释，并识别出 Gödel 已证明、勾勒或构想过的 663 个定理；在通过 Coq 证明助手运行后，约 400 个按原样通过验证，约 200 个需要修复，约 50 个为假。Von Plato 表示，Claude 对选择公理独立性证明的重构通过了 Coq，这表明 Gödel 在 1940 年代就已掌握该结果，并且这些工作簿中还包含十几个尚未探索的逻辑主题。