数学界震动！Claude一口气写下19万行源码，揪出13年前证明错误

人类数学家的处境，看来是越来越不好过了……

费马大定理这边，1000个Claude Fable 5.2组队跑了30个小时，把完整的形式化证明做了出来。

就在今天，又有人带着Claude把13年前获证的「三元哥德巴赫猜想」证明形式化了。

干这件事的是独立开发者Charlie Reams，他敲下19.4万行Lean 4代码，整个库「零sorry」。

更让人意外的是，Claude自己发现2013年的原版证明里藏着好几处错误。

它没多犹豫，顺手就把这些数学漏洞补上了。

一个人加一个Claude，写出19.4万行源码

先要把概念分清：平时说的「1+1」是强哥德巴赫猜想，到现在也没人能彻底证出来。

至于「三元哥德巴赫猜想」，也叫弱哥德巴赫猜想，说的是——

任何大于5的奇数，都能写成三个质数之和。

2013年，秘鲁数学家Harald Helfgott宣布彻底证明了这道困扰人类271年的难题。

那在当时是全球数学界的一件大事。

可麻烦也跟着来了：Helfgott的证明太长、太琐碎。光是主干手稿就有300页，里面全是不等式放缩和常数计算，一段接一段。

此后十几年，Helfgott本人陆续出了好几个版本，用来修正细节。

但计算过程冗长得让人发怵，全球也没有几个数学家愿意花精力，把每一个常数从头到尾核对一遍。

独立开发者Charlie Reams决定把这事交给Claude Code去啃。

打开GitHub仓库calr3/ternary-goldbach（cde-moebius分支），会看到一个让人震撼的数字工程：

整整19.4万行Lean代码，外加辅助脚本和技术文档。

这场战役里，Charlie Reams管的是定顶层目标、拆任务指令。

绝大部分Lean形式化代码、自动化脚本甚至文档，都是Claude Code一手完成的。

最后跑出来的结果让所有人震撼：19.4万行源码，0个sorry！

在Lean语言里，sorry意思是跳过没证完的步骤；零sorry就说明每一行推理都经过了极严格的机器验证，一处空都没留。

顺手给顶级数学家挑错改作业，一共揪出11处问题。Helfgott的证明之所以难核对，难就难在「全是数」。

证明走的是圆法：问题被切成主弧和劣弧两块，主弧算「收入」，劣弧算「开销」，收入稳稳压过开销，定理就站得住。

这种活儿人眼盯到第50页就发怵，Lean不会。

仓库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。Claude没有照抄，换了一种拆法绕过去，算出7.04，仍在所需的7.284以内。

另外还有一处「硬伤」：定理13.2.1的证明把两种尺度的主弧搅在了一起，这一段等于被重新搭了一遍。

修完之后，主弧「收入」从原书的1.058259降到1.049，劣弧「开销」从1.00948涨到1.0376。两者之差即证明的安全垫，从0.04877 x²/κ缩到0.0114 x²/κ，缩水四分之三还多，但依然大于零。

原作者亲自下场，揭开两大「未竟前提」。

事情发酵后，所有人都想知道：Harald Helfgott看到自己的成名作被AI挑出错又修好，会是什么反应？

结果Helfgott本尊很快在X上露面，态度相当坦诚——今年10月4日，Charlie Reams就已私下联系过他，告知形式化工作跑通了。

这一个月里，一人一AI又干了件大事：把整个证明依赖的外部额外假设（公理）从最初的5项一路砍到只剩2项。

在这个仓库里，全部解析数论推导逻辑已100%形式化且零sorry，但在Lean外部仍挂着两项既有的数值验证结果当假设：Platt的广义黎曼猜想（GRH）数值验证，以及偶数哥德巴赫猜想局部验证至4x10^18。

把这两块人类早就算好、还没搬进Lean内核的「巨型数字垫脚石」放进去，三元哥德巴赫猜想的大厦就严丝合缝了。

超级智能正在给「证完了」重新下定义。

过去，一份几百页的证明算不算数，得靠少数几位专家花上几年去啃。啃完了，也未必有人敢拍胸脯打包票。

如今标准换成了另一句话：能不能过内核。

照这个势头，数学界最硬核的同行评审，或许很快只剩一句话——

这话是：「别发PDF了，先把你的证明喂给Claude跑出零sorry再说。」