独立开发者借助 Claude Code 完成了三元哥德巴赫猜想（弱哥德巴赫猜想：任何大于 5 的奇数都可以表示成三个质数之和）的形式化证明，产出约 19.4 万行 Lean 4 代码、辅助脚本与技术文档，全库保持零 sorry，即没有跳过任何未证完的步骤，全部数学推理经过机器严格验证。这项工作的价值不只是 "把已有证明翻译成代码"：在形式化逐条核对 2013 年原版证明的过程中，AI 辅助发现了原证明中 11 处与原稿对不上的地方，包括常数取值偏差、个别不等式不成立、引用乘积上界偏紧以及主弧尺度混用等问题，并在形式化过程中完成修补和重建；修正后证明的安全垫明显收窄，但仍然大于零。目前整套解析数论推导已在 Lean 内闭环，外部仍挂靠两项人类早已算好的数值验证结果作为前提。这一案例体现的方向是：长证明的核对标准正在从少数专家多年通读，转向机器内核可检查、可复跑的形式化验证。
一、先分清：三元哥德巴赫猜想是什么
| 项目 | 内容 |
|---|---|
| 猜想名称 | 三元哥德巴赫猜想，又称弱哥德巴赫猜想 |
| 命题表述 | 任何大于 5 的奇数，都可以表示成三个质数之和 |
| 与强哥德巴赫猜想的区别 | 强哥德巴赫猜想（偶数表为两个质数之和）至今未被彻底证明；三元版本属于较弱的命题 |
| 原版证明 | 2013 年 Harald Helfgott 宣布完成证明，主干手稿约 300 页 |
| 证明方法 | 圆法：把问题拆成主弧（收入）和劣弧（开销），只要收入稳定大于开销，定理即成立 |
| 本次工作 | 用 Lean 4 对该证明做机器可检查的形式化验证，并核对、修补其中细节 |
二、这次形式化证明的工程规模
| 指标 | 数据 |
|---|---|
| 代码规模 | 约 19.4 万行 Lean 4 代码、辅助脚本与技术文档 |
| 未证占位 | 全库零 sorry，没有留未完成的证明步骤 |
| 验证方式 | 全部推理由 Lean 内核机器严格验证 |
| 代码仓库 | GitHub calr3/ternary-goldbach，cde-moebius 分支 |
| 人机分工 | 人负责设定顶层目标、拆解任务指令；Claude Code 承担绝大多数形式化代码、自动化脚本与文档 |
在 Lean 这类定理证明语言里，sorry 表示暂时跳过尚未证明的步骤。零 sorry 意味着证明链条上每一步都有形式化依据，不存在 "先空着以后补" 的环节。
三、形式化核对中发现的几类问题
原版证明篇幅长、不等式放缩和常数计算密集，长期以来很少有人能从头到尾逐条复核。形式化过程中，仓库 README 列出了 11 处与原书对不上的地方，典型类型如下：
| 问题类型 | 原稿情况 | 形式化处理 |
|---|---|---|
| 常数取值偏差 | (6.77) 式把关键常数写成 0.5，正确值为 0.8102；连带修正后项目采用 0.8764 | 按重新核算后的常数进入证明链条 |
| 不等式不成立 | (5.32) 在 v=2 时，积分实际算出 0.53344，超过原稿上界 0.37273・log 4（约 0.5167） | 重新核算并调整相关推导 |
| 引用上界偏紧 | 引用 Ramaré 1995 年论文的一步，声称某乘积不超过 8，实际约为 8.0845 | 换用另一种拆分方式绕开，得到 7.04，仍在所需的 7.284 以内 |
| 主弧尺度混用 | 定理 13.2.1 的证明把两种尺度的主弧混在一起 | 该段证明被重新搭建 |
四、修补之后证明还稳不稳
修正会改变主弧和劣弧的数值对比，也就是证明的 "安全垫"：
| 数值项 | 原稿 | 修正后 |
|---|---|---|
| 主弧（收入） | 1.058259 | 1.049 |
| 劣弧（开销） | 1.00948 | 1.0376 |
| 安全垫（差值） | 0.04877 · x²/κ | 0.0114 · x²/κ |
安全垫缩水约四分之三还多，但仍然大于零，证明在修正后的形式化链条上依然成立。这个结果也说明：长证明里的常数和上界一旦偏紧，留给后续推导的容错空间会被明显压缩，机器核对的价值正在于把这些容易被人眼放过的细节逐项压实。
五、还剩下两项外部数值前提
整套解析数论推导已经 100% 形式化且零 sorry，但证明在 Lean 外部仍挂靠两项既有的数值验证结果作为前提假设：
- Platt 完成的广义黎曼猜想（GRH）相关数值验证；
- 偶数哥德巴赫猜想局部验证至 4×10¹⁸ 的数值结果。
这两块属于人类早已计算完成、但尚未搬进 Lean 内核的 "巨型数字垫脚石"。把它们作为外部前提接入后，整个三元哥德巴赫猜想的形式化大厦闭环。后续如果这两块数值结果也被纳入 Lean 形式化内核，整个证明的形式化依赖还会进一步收窄。
六、AI 辅助形式化证明的工作方式
分工流程
- 人确定顶层目标：把哪一份既有证明搬进定理证明语言；
- 人拆解任务指令，划分模块和中间定理；
- Claude Code 生成 Lean 形式化代码、自动化脚本和配套文档；
- Lean 内核反复编译检查，未通过的步骤回到模型补全；
- 核对原稿常数、不等式和引用上界，发现偏差后重新推导或换拆分方式；
- 全库达到零 sorry，证明链条机器可复跑。
相比人工通读的优势
- 不会因篇幅长而跳过中间常数和不等式；
- 每一步都要求类型检查通过，模糊表述无法留在证明里；
- 脚本化流程便于反复复跑和后续扩展；
- 发现问题后可以在形式化框架内直接修补，而不是停留在文字批注。
七、怎么理解这次事件的意义
- 证明标准在变化：一份几百页的手写证明算不算 "证完了"，过去要等少数专家花数年通读；现在越来越多的判断标准是 "过没过定理证明内核"；
- AI 承担的是核对与落地：顶层数学判断仍由人把握，AI 主要承担把证明形式化、跑通检查、核对常数这类高强度重复工作；
- 不等于推翻原版结论：本次工作是对 2013 年证明的形式化复核与细节修补，三元哥德巴赫猜想的数学结论本身由原证明给出；
- 行业背景：同期 AI 辅助形式化还覆盖了费马大定理等经典命题，长证明的机器验证正在成为数学研究工程化的一个方向。
八、小结
Claude 辅助完成的 19.4 万行 Lean 4 代码，把三元哥德巴赫猜想的证明推进到了零 sorry、机器可验证的状态；过程中还揪出并修补了原稿里的常数偏差、不等式偏紧和尺度混用等问题。需要清醒看到的是，证明仍挂靠两项外部数值前提，形式化验证是对既有数学结论的严格落地，而不是 AI 独立提出了新定理。随着定理证明工具和 AI 辅助流程成熟，长证明的复核、归档和复用会越来越依赖机器可检查的形式化形态。
【常见问题】
问题 1：这次 Claude 辅助完成的三元哥德巴赫猜想形式化证明，代码规模和验证标准是什么？
回答 1：本次三元哥德巴赫猜想形式化证明共产出约 19.4 万行 Lean 4 代码、脚本与文档，全库零 sorry，没有跳过任何未证步骤，全部推理由 Lean 内核机器严格验证；代码托管在 GitHub calr3/ternary-goldbach 仓库的 cde-moebius 分支。
问题 2：三元哥德巴赫猜想和强哥德巴赫猜想是一回事吗？
回答 2：不是。三元哥德巴赫猜想即弱哥德巴赫猜想，命题是任何大于 5 的奇数都可表为三个质数之和，2013 年已有原版证明；强哥德巴赫猜想指偶数可表为两个质数之和，至今尚未被彻底证明，本次形式化证明对应的是三元版本。
问题 3：形式化核对三元哥德巴赫猜想证明时，AI 具体发现了哪些类型的问题？
回答 3：核对中发现原稿共 11 处对不上的地方，包括常数取值偏差、个别不等式在特定取值下不成立、引用乘积上界偏紧、主弧两种尺度混用等；AI 辅助重新核算常数、调整推导并更换拆分方式，修补后安全垫收窄但仍大于零。
问题 4：这份形式化证明是否已经不依赖任何外部前提？
回答 4：还没有。整套解析数论推导已在 Lean 内零 sorry 闭环，但外部仍挂靠两项人类已完成的数值验证结果：Platt 的 GRH 相关数值验证，以及偶数哥德巴赫局部验证至 4×10¹⁸ 的结果；这两块尚未搬进 Lean 内核，是当前形式化链条的外部前提。
【参考资料】
- [2026-11-13]（数学界震动，Claude 一口气写下 19 万行源码，揪出 13 年前证明错误）36 氪（新智元授权发布）
- [2026-11-13]（数学界震动！Claude 一口气写下 19 万行源码，揪出 13 年前证明错误）新浪财经（今日头条转载）
- [2026-11-13]（Claude Assists in Completing 190,000 Lines of Code, Successfully Formalizing the Ternary Goldbach Conjecture）AIbase
- [2026-11-13]（Claude Helps Complete 190,000 Lines of Code for the Formal Proof of the Ternary Goldbach Conjecture）C114Pro
- [2026-11-14]（Claude 19 万行代码与三元哥德巴赫猜想形式化验证相关报道聚合）智源社区
- [2026-09-08]（11 天、30 万美元：AI 攻破 358 年数学难题的最后一关）36 氪
- [2026-09-05]（Claude Just Formalized Fermat in 11 Days on 6 Billion Tokens）TensorFeed.ai
【免责声明】
本文内容基于公开报道与代码仓库信息整理，仅用于 AI 辅助数学形式化验证的技术趋势交流，不构成数学结论正确性的独立背书。文中代码行数、问题数量、常数数值、安全垫比例及外部前提均来自公开来源与特定仓库版本，定理证明的最终状态以 Lean 内核编译结果、仓库更新和数学界同行评审为准；形式化验证不能替代对数学命题本身的研究判断。引用的外部资料版权归原出处所有，如表述存在偏差，以原始文献和官方仓库为准。