Claude用19万行Lean代码揪出13年前弱哥德巴赫证明错误

一场围绕13年前弱哥德巴赫猜想证明的形式化审查，把AI推到了数学证明的裁判席上。Claude没有重新证明猜想，而是把Harald Helfgott那套数百页的解析数论证明翻译成Lean形式化语言，让编译器像验算器一样逐步推导。真正的震动发生在推导卡住的地方：机器不认“显然”，也不替人类补步骤，原证明里被时间掩埋的漏洞因此一个个现形。

Claude把13年前的弱哥德巴赫猜想证明搬进Lean，19万行代码里亮起红灯

弱哥德巴赫猜想也就是“奇数哥德巴赫猜想”：每个大于5的奇数都可以写成三个素数之和。Helfgott在2013年给出证明，此后一直是解析数论里的重量级成果。把这种级别的证明形式化，公认是以年为单位的工程，因为证明不是一段散文，而是一条极长的逻辑链，断一环，后面全塌。

Claude这次交出的约19万行Lean代码，目标不是生成一个新证明，而是把原证明的每一步都变成机器可检查的命题。Lean内核只认逻辑规则：只要有一行推导对不上，整份证明就过不了。也正是在这种“零容忍”的检查下，Claude发现了原书中的多处硬伤。

0.5其实是0.8102，一条积分不等式当场越界

最先暴露的是关键常数写错。原式把一个常数写成0.5，正确值应是0.8102；连带修正之后，项目最终采用的是0.8764。对解析数论证明来说，常数不是装饰，它直接决定上下界能不能闭合。

紧接着，一条不等式被证明压根不成立。书中(5.32)在v=2时出错：一个积分实际算出来是0.53344，超过了书里给出的上界0.37273·log 4，约0.5167。机器不会因为“作者是专家”就放行，积分值一摆出来，这一步就无法通过。

Claude还发现原证明引用的外部结果也有问题。证明引用了Ramaré 1995年论文里的一步，声称某个乘积不超过8，实际约为8.0845。Claude没有硬着头皮照抄，而是换了一种拆法绕过去，得到7.04，仍在所需的7.284以内。除此之外，定理13.2.1的证明把两种尺度的主弧混在了一起，这一段等于被重新搭了一遍。

安全垫从0.04877缩到0.0114，证明仍然站得住

修完这些错误后，证明的“账本”发生了变化。主弧“收入”从原书的1.058259降到1.049，劣弧“开销”从1.00948涨到1.0376。两者之差，也就是证明的安全垫，从0.04877 x²/κ缩到0.0114 x²/κ，缩水四分之三还多。

但关键结论没有翻车：这个差值仍然大于零。也就是说，修正之后证明依旧成立，只是余量比原书薄了很多。对数学证明而言，安全垫缩小不是小事，它意味着后续任何一步再出偏差，都可能把整个论证推到零以下；但至少在这一轮机器检查中，Helfgott的证明框架经受住了修补。

Helfgott在X上回应：公理从5项砍到2项

事情发酵后，外界最关心原作者会怎么反应。Helfgott很快在X上现身，态度极其坦诚。早在今年10月4日，Charlie Reams就已经私下联系过他，告知形式化工作已经跑通。

更关键的是，在这一个月里，一人一AI又干了一件大事：把整个证明依赖的外部额外假设从最初的5项一路砍到只剩2项。在这个仓库里，全部解析数论推导逻辑已经100%形式化且零sorry，但Lean外部依然挂靠两项既有的数值验证结果作为前提假设：Platt的广义黎曼猜想数值验证，以及偶数哥德巴赫猜想局部验证至4×10^18。

这两块人类早已算好、但还没搬进Lean内核里的“巨型数字垫脚石”，一旦放进去，整个三元哥德巴赫猜想的大厦就严丝合缝地闭环了。所谓“零sorry”，在Lean里意味着没有留下任何未证明的占位符；对数学界来说，这比一句“我检查过了”硬得多。

编译器坐上裁判席，数学同行评审多了一道“零sorry”

这场风波的意义不只在Helfgott的证明被修了几