核心结论：芬兰赫尔辛基大学逻辑学家 Jan von Plato 团队从 2017 年起破译哥德尔 1940 年代初写下的 16 本、共 1009 页加贝尔斯贝格（Gabelsberger）德文速记笔记，人工进度只有每周一页；2026 年 9 月起接入 Claude，几天内就产出 650 页（后扩至 1084 页）整卷解读，梳理出 663 条带证明或证明雏形的候选结果，其中约 400 条经 Coq 形式化验证成立、约 200 条补前置假设后成立、约 50 条为错。最重磅的发现是：哥德尔早在科恩（Paul Cohen）发明力迫法、1966 年凭选择公理独立性拿菲尔兹奖的二十多年前，就构造出了等价的证明架构，只差一个 "有限支撑" 定义写错一行；Claude 还原的证明经 Coq 全部验证通过。原因在于这类材料的瓶颈不是读懂单个词，而是上千页思路的跨页关联 —— 人类读到后面忘了前面，AI 能把全部笔记和整个人类逻辑学文献同时摆在视野里。流程分四步：人工先把速记转写成现代英文、把转写稿和学术文献喂给 Claude、AI 产出整卷解读、再由计算机科学家协助做形式化验证。下面把背景、成果和争议讲清。
一、项目背景：80 年没人读完的 "天书"
- 笔记来源：哥德尔 1940 年定居普林斯顿高等研究院（IAS）后写下的 16 本工作簿，共 1009 页；他 1931 年提出不完备定理后，大量手稿从未发表，身后留下数万页。
- 破译难点：笔记用已过时的加贝尔斯贝格德文速记写成，全球能读的人极少；且内容高度浓缩、跳跃、充满直觉草图和未展开公式，读懂英文转写也不等于读懂哥德尔的思路。
- 人工瓶颈：von Plato 团队多年维持每周约一页的速度；他 2017 年临近强制退休时申请到欧洲研究理事会 250 万欧元资助，自学速记并主导项目。
- 转折：2026 年夏在法国一场 "AI 与定理证明" 会议上，计算机科学家建议他试试 Claude；8—9 月正式接入。
二、AI 怎么上手：输入与产出对照
| 环节 | 内容 |
|---|---|
| 输入 | 1009 页转写稿、von Plato 自己写的 6 本哥德尔专著、大量现代逻辑学与科学文献 |
| 产出 | 几天内给出 650 页整卷解读，后续追问下扩充到 1084 页 |
| 人类做法 | 逐页消化，每周约一页，且跨页关联容易丢失 |
| Claude 的优势 | 上千页笔记与文献 "同时在场"，直接把第 12 页的灵感和第 890 页的公式连起来；von Plato 称之为拥有 "莫扎特式" 视野的 "数字怪物" |
三、成果盘点：663 条候选定理怎么落地
Claude 从工作簿中提取 663 条带证明、证明草图或证明思路的候选结果，验证口径如下：
| 类别 | 数量级 | 处理方式 |
|---|---|---|
| 表述成立、经 Coq 验证 | 约 400 条 | 直接确认 |
| 思路正确、补前置假设后成立 | 约 200 条 | 调整陈述或假设 |
| 错误 | 约 50 条 | 哥德尔本人常在页边批注 falsch（错）/schlecht（差），不意外 |
| 仍在验证 | 少数几条 | 持续核对 |
换算下来，哥德尔在 1940 年代初逃难到美国的短短不到三年里，几乎每两天就证明一条新定理。此外 Claude 还列出 14 个隐藏在笔记中、至今无人研究的全新逻辑课题，并可在追问下展开成 50 页大纲。
选择公理：差一步改写数学史
- 选择公理断言：即使没有统一规则，也能从无穷多双 "无左右之分的袜子" 里各挑一只；它能否从其他基础公理推出，长期悬而未决。
- 1963 年科恩发明力迫法证明其独立性，1966 年获菲尔兹奖；哥德尔 1966 年曾自称 1940 年代已证出，但被同行要求复现时无法重建。
- Claude 翻出的真相：哥德尔构造了等价的 "可能世界（哥德尔空间）" 架构，用对角线论证假设万能选择函数 F，再构造集合 K 制造自指矛盾，证明该世界里不存在这样的选择函数；唯一的硬伤是关键的 "有限支撑" 定义写错一行，而正确定义他在两年前就写过，只是后来翻看时忘了。
- 还原证明经形式化证明助手 Coq 全部验证通过；人机合著论文送给哥德尔专家金森晶宏（Akihiro Kanamori），他在不知道有 AI 参与的情况下评价其 "数学与历史上都极其敏锐深刻"。
笔记里的超前彩蛋
- 量子力学：1935 年 EPR 论文前，哥德尔就计算过纠缠耦合系统测量后的状态变化，没有沿用冯・诺依曼 1932 年旧法，而用了 1951 年才由吕德斯正式提出的吕德斯规则。
- 哥德尔宇宙：1949 年他解出广义相对论场方程的旋转宇宙解，光锥倾斜可形成闭环时间曲线；笔记显示他不是玩笑，而是翻遍数百页天文观测数据，想用统计学验证我们的宇宙是否在旋转。
- 另有构造性公理独立性、函数解释强规范化证明等结果，要到 1970—80 年代才被后人重新发现。
四、为什么说 "离菲奖只差最后一步"
- 科恩凭选择公理独立性证明拿了 1966 年菲尔兹奖，这是该问题的最高荣誉。
- Claude 还原出的架构表明，哥德尔 1940 年代已走到正确证明门口，只卡在一行定义；von Plato 判断他若再继续几个月就能完成正确证明。
- 这不是说哥德尔当年就该领奖 —— 证明当时并未成形、未发表；它说明这段被埋没的笔记本可能提前二十年改写这一领域的历史。
五、学界反应与局限
- 圣母大学逻辑教授 Joel David Hamkins 尚未看到 AI 还原的选择公理证明，他表示若经得起审查，将 "非常了不起且有历史意义"；有相似思路不等于拿到最终版本，但说明哥德尔走在正确路上。
- 局限：候选定理中约 50 条本身是错的，AI 产出仍需人工与形式化工具逐条验证；笔记解读属于历史重建，不代表哥德尔当年完整发表过这些结果。
- 下一步：von Plato 计划继续挖掘这 16 本逻辑笔记的十几个未探索主题，之后再研究哥德尔的物理学与宇宙学笔记。
【常见问题】
问题 1：Claude 破译哥德尔笔记到底做出了什么，挖出多少条新定理？
回答 1：Claude 在几天内完成 1009 页哥德尔速记笔记的整卷解读，提取 663 条候选定理，约 400 条经 Coq 验证成立、约 200 条补假设后成立、约 50 条错误；还发现哥德尔 1940 年代已接近选择公理独立性的完整证明，相关成果震撼数学界。
问题 2：为什么说哥德尔离菲尔兹奖级证明只差最后一步？
回答 2：科恩凭选择公理独立性证明获 1966 年菲尔兹奖，而 Claude 发现哥德尔二十多年前就构造出等价的哥德尔空间与对角线论证架构，只在 "有限支撑" 定义上写错一行，正确定义他自己两年前就写过；还原证明经 Coq 验证通过，说明他当年离完整证明只差临门一脚。
问题 3：哥德尔笔记为什么 80 年没人破译，Claude 为什么能做到？
回答 3：笔记用已灭绝的加贝尔斯贝格德文速记写成，且高度浓缩、跨页跳跃，人工进度每周仅一页；Claude 能把上千页笔记和全部相关文献同时关联，补上人类读到后面忘记前面的短板，几天内产出 650 页解读。
问题 4：Claude 发现的哥德尔超前成果还有哪些？
回答 4：除选择公理外，笔记里有 1951 年才正式提出的吕德斯规则的早期使用、哥德尔旋转宇宙与闭环时间曲线的统计学验证尝试，以及 14 个至今无人研究的全新逻辑课题和一批 1970—80 年代才被重新发现的结果。
问题 5：这项破译成果可信度如何，AI 说的都算数吗？
回答 5：不算直接采信：候选定理逐条经 Coq 形式化验证，约 50 条被判定为错误；选择公理证明的重建仍待学界同行审查，Hamkins 等专家尚未看完；AI 产出定位是历史重建与辅助，最终结论以数学界审查为准。
【参考资料】
- [2026-11-14]（Claude 破译哥德尔天书，80 年笔记震撼数学界）36 氪（新智元）
- [2026-11-13]（AI model reveals hidden mathematical proofs in Kurt Gödel's obscure notebooks）Journal Signal
- [2026-11-13]（"Ahead of His Time"：AI Helps Uncover Discoveries Hidden in Gödel's Notebooks）美国普林斯顿高等研究院（IAS）官网
【免责声明】
本文基于媒体报道与研究项目公开信息整理，笔记解读与定理验证仍在进行中，选择公理证明的重建尚未完成同行评审；"离菲奖只差一步" 为媒体比喻，不代表哥德尔当年已完成证明或应获菲尔兹奖，具体数学结论以正式发表论文与学界审查为准。