北京
新智元报道
这是真要把人类数学家，逼上绝路啊......
费马大定理，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
编辑：桃子
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
