Claude Code写19.4万行Lean4：三元哥德巴赫猜想形式化验证零sorry

人工智能正在基础科学领域留下实打实的成果。独立开发者 Charlie Reams 用 Claude Code 完成了三元哥德巴赫猜想的形式化证明，累计产出 19.4 万行 Lean4 代码，没有一处 sorry，全部数学推理都经机器严格验证。

机器还顺带当了一回审稿人：自主发现并修补了 13 年前的 11 处漏洞。

整个证明过程中，AI 表现出比传统人工审稿更细的严谨劲。它在运行和推导时自己找出了数学家 Harald Helfgott 2013 年发表的原版证明里的 11 处关键问题，涉及常数写错、不等式不成立、引用数据有偏差、主弧尺度混淆等多个方面，并逐一把它们补上。

在此基础上，研究人员又把该证明依赖的外部额外假设从最初的 5 项压缩到只剩 2 项，且都是已有的公开数值验证结果。证明的严谨性由此向前推进了一大步。

数学界判断“证明完成”的标准，正在朝机器可验证的方向走。

这件事的分量不止于攻克一道数学难题。它还在更深层面推动数学界重新界定什么叫“证明完成”——从过去依赖同行评议，逐步转向完全依靠机器验证的形式化路径。