AI 助力解读哥德尔工作簿，发现数百个未知定理
AI unlocks Gödel's notebooks, said to contain hundreds of proved theorems
AI 导读
《卫报》报道，赫尔辛基大学逻辑学家 Jan von Plato 自2017年起研究哥德尔1940年代初写下的16本共1,009页工作簿，此前进展约每周一页。9月起借助 Claude，几天内得到650页全卷解读，Claude 提取出663个定理，其中约400个经 Coq 验证成立、约200个修复后成立、约50个为误，并近乎复原了选择公理独立性的证明。