数学界震动！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跑