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

这是真要把人类数学家，逼上绝路啊......

费马大定理，30个小时1000个Claude Fable 5.2组队，完成了完整的形式化证明。

就在今天，一人+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的证明把两种尺度的主弧混在了一起，这一段等于被重新搭了一遍。

Claude修完之后，主弧「收入」从原书的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再说。」

参考资料：

https://x.com/jdlichtman/status/2120301890504441905

本文来自微信公众号“新智元”，作者：桃子，36氪经授权发布。