由 Jan von Plato 领导的研究项目正利用人工智能来解码库尔特·哥德尔的私人笔记，他是历史上最具影响力的逻辑学家之一。由于哥德尔发表的作品相对较少，这些用几乎已过时的速记法编写的笔记被认为包含数百个已证明但隐藏了数十年的定理。
解锁逻辑学家的私人笔记
该项目专注于库尔特·哥德尔的笔记，他的工作从根本上改变了数学和逻辑。虽然哥德尔因其贡献而闻名，但他以发表缓慢著称，有时甚至要等待数十年才发布他在 Dialectica 解释等复杂主题上的初步想法。
这些笔记提供了对其思维过程罕见的、未经过润色的视角。通过解码这些笔记，研究人员希望找回哥德尔在世时从未与公众分享的大量数学内容。
“AI 解锁了哥德尔的笔记，据称其中包含数百个已证明的定理”
— AI unlocks Gödel's notebooks, said to contain hundreds of proved theorems
Gabelsberger 速记法的挑战
获取这些笔记的主要技术障碍是哥德尔使用了 Gabelsberger 速记法。这种速记系统在 1920 年左右在学校中教授，但后来在技术上变得过时，导致世界上极少数人能够阅读它。
作为哥德尔研究领域的领先专家，Jan von Plato 据报道在 2017 年开始该项目前自学了这种速记法。为了扩大工作规模，他的团队利用欧洲研究委员会提供的 250 万欧元资助，在现有的速记法转录文本上训练 AI 模型，以实现解码过程的自动化。
Hacker News 讨论与观点
关于这一进展的 Hacker News 讨论包含了关于 AI 与历史数学交汇点的各种观点。一位以 'semolinapudding' 为名的评论者表达了对该项目的兴奋，指出哥德尔的工作如此重要，即使是少量的产出也将是“巨大的事件”。
其他参与者讨论了速记法的实用性。例如，一位名为 'hobo123' 的评论者指出，虽然 Gabelsberger 速记法通常被认为是过时的，但它仍被一些人在 2020 年代初期继续使用。另一位评论者 '2aFds' 指出，AI 的有效性可能源于它是在仍广泛可用的预先存在的速记法转录文本上进行训练的。
讨论还涉及该项目的社会影响。一位名为 'alterom' 的评论者建议，这可以通过提供一种在早期建立对问题的思考记录的方法来改变“不发表就淘汰”的文化，即使工作仍未完成。相反，另一位评论者 'cyanydeez' 推测，笔记中关于逻辑的最复杂批判最终可能会达到当前大语言模型的“令人发狂的极限”。
局限性与不确定性
虽然该项目有望揭示数百个定理，但具体的数学内容和成功“解锁”的定理确切数量仍有待详细说明。此外，还有一个持续的问题是，与标准的数学证明相比，AI 能多大程度上捕捉到哥德尔为人熟知的细致、高水平的逻辑批判。