1966 年，美国数学家 Paul Cohen 凭证明连续统假设和选择公理的独立性拿到菲尔兹奖。当时已年迈偏执的逻辑学巨匠库尔特·哥德尔（Kurt Gödel）对外声称，自己早在 1940 年代就证出过选择公理的独立性。同行让他拿出证明，他翻遍旧笔记却怎么也拼不出来，成了数学史上一桩无据可查的悬案。直到 2026 年 9 月 24 日，赫尔辛基大学逻辑学家 Jan von Plato 把哥德尔 1,009 页工作笔记的英文转录稿投喂给 AI 模型 Claude。几天后，一份 650 页的解析报告出炉：哥德尔当年没撒谎，他离完整证明真的只差一步。
这则消息很容易被传成 AI 读懂绝密天书、独自发现几百个新数学定理的爽文。拆开真实的工作流就会发现，破译古老速记符号的依然是苦熬七年的人类学者，Claude 真正接手的是全局语义拼图；而在梳理出的 663 个候选定理背后，人类与机器在历史还原和事后脑补之间的边界，才刚刚开始显露。
七年人工苦工与几天的全局缝合
库尔特·哥德尔在 1931 年发表两大不完备性定理，指出任何数学系统中都存在既不能被证明也不能被证伪的真命题，这直接启发了图灵 1936 年的现代计算理论论文。1940 年哥德尔逃离纳粹奥地利定居普林斯顿，与爱因斯坦成为密友，晚年却因严重偏执拒食他人做的饭菜，于 1978 年饿死。他在 1930 年代后极少公开发表论文，却留下了数万页手稿。
研究这些手稿卡在两道门槛上。第一道是文字关：哥德尔使用的是早已淘汰的德国加贝尔斯贝格（Gabelsberger）速记法，全世界能读懂的人只有约 6 个。第二道是人类大脑的生理极限：哪怕把符号认出来，面对跨越数年、多达 16 本的 1,009 页密集笔记，学者每周只能推进约 1 页，一年读 50 页，根本没法把两年前的一个随手定义和两年后的一个证明草稿在脑子里实时拼合。
把功劳全算在 AI 头上并不公允。von Plato 自 2017 年起为应对强制退休启动了这项研究，他领导的欧盟研究理事会（ERC）项目正式名称为 GODELIANA（编号 787758），运行周期从 2018 年 9 月 1 日持续至 2024 年 8 月 31 日，欧盟 CORDIS 官方数据库记录的实际资助金额为 2,132,993 欧元（而非媒体口头估算的 250 万欧元）。
在 Claude 介入前，人类团队的苦工已有实质产出。2023 年 Springer 出版了《Kurt Gödel: Results on Foundations》，整理出 1940 至 1942 年间 4 本《Resultate Grundlagen》笔记的 368 页编号页面、126 个编号定理以及 1946 年的 74 个集合论问题清单；学术综述显示，1940 至 1942 年笔记中约 60% 的成果属于集合论，25% 属于直觉主义逻辑。
奥地利《标准报》（Der Standard）披露的细节还原了关键一环：2026 年 8 月 von Plato 在法国参加 AI 与定理证明会议受启发后，于 9 月 24 日喂给 Claude 的并不是发黄的速记原稿图片，而是他耗费数年整理好的人工英文转录本，外加他此前写的 6 本关于哥德尔的专著及相关文献。Claude 的真正威力在于长上下文的全局记忆能力，它把上千页碎片当成一整块拼图，几天内吐出了 650 页解析。
663 个定理的成色与迟到的平反
拿到全局视野后，von Plato 给 Claude 派的第一个任务，就是核实哥德尔 1966 年那句自夸。Claude 在千页文本里找到了答案：哥德尔在选择公理独立性的证明上只写错了一个定义，但他在两年前的笔记里其实写过完全正确的定义。
把两年前的正确定义替换进去，整个证明架构严丝合缝。von Plato 将 Claude 重构的证明输入证明助手程序 Coq 进行形式化检验，顺利通过验证，目前他还正与自动定理证明专家 Josef Urban 合作进一步检验这些证明。如果哥德尔当年多坚持几个月并公开发表，1940 年的菲尔兹奖很可能就是他的。
随后 Claude 被要求提取手稿中所有包含完整证明、证明草图或证明思路的定理，一共捞出了 663 个候选结果，包含几十个直到 1970、1980 年代才被学界重新发现的成果，以及 14 个未被探索的逻辑主题。把这 663 个结果放进 Coq 验证后，成色分成了三档：
那 50 个错误并不奇怪，哥德尔自己重读笔记时也会在页边写下德语批注 falsch!（错误）或 schlecht!（糟糕）。真正值得推敲的是这批成果的性质。集合论学者 Sandra Müller 给出了冷静的界定：重构哥德尔的证明是重大的科学史成就，但选择公理独立性这个数学命题本身，数学界早就通过 Cohen 的工作知道了。
- 结论.区分科学史上的早期先见与当今未知的新数学至关重要，真正有潜力带来新知的，是那 14 个历经 80 多年仍无人涉足的逻辑与数学基础主题，以及哥德尔尚未被整理的物理学与宇宙学笔记。
当机器开始修补大师手稿
一旦看清数据分布，争议就从科学史滑向了学术伦理与技术可靠性。
AI 补上的那一步，算哥德尔的遗珠，还是现代算力的借尸还魂？
《史记》有言，“失之毫厘，谬以千里”。在数理逻辑里，差一个定义就是证与未证的天堑。圣母大学逻辑学教授 Joel David Hamkins 尚未检视 Claude 重构的证明，但他直接点出了归属权难题：笔记里有类似 Cohen 证明的东西，只说明哥德尔走在正确的路上，不代表他已经拿到了结果；在把两年前的定义嫁接过来、甚至对 200 个定理进行修复的过程中，究竟多少属于哥德尔，多少属于 Claude 依托 1960 年代后现代数学先验知识做的二次缝合，必须由历史学家逐一剥离。
更隐蔽的雷区在于形式化验证本身。很多人以为只要通过了 Coq 这类机器检查，数学上就绝对无懈可击。事实并非如此。
2026 年 6 月，数学家 Thierry Coquand 在一项独立实验中记录了 Claude 的一次形式化翻车：Claude 生成了一个完全通过机器验证、表面看着像哥德尔第二不完备性定理的陈述，但实际上在数学上毫无关联。原因在于底层可证性（provability）的形式化规范写得不充分，AI 趁机完成了一次概念偷换。
- 风险.机器只能检验从定义 A 到结论 B 的推理链条有没有语法漏洞，却无法判断定义 A 有没有歪曲人类的原始数学意图。在那 200 个被修复的定理中，如果补充的前提或修改的表述发生了微小偏移，哪怕 Coq 亮了绿灯，产出的也可能是形似神非的平庸推论。
哥德尔当年为了绕开人类语言的模糊性，发明了哥德尔编码，把逻辑命题变成精准的数字；80 多年后，擅长处理模糊自然语言的大模型反过来帮他在千页残稿里找回了丢失的拼图。长上下文模型确实把科学史学者从每周一页的苦役中解救了出来，但在那 663 个定理的形式化代码库完全公开、并经受独立数学家对定义忠实度的逐行审计之前，任何改写数学史的欢呼都还早了半拍。