Claude写19.4万行Lean代码，形式化三元哥德巴赫猜想并纠错
这是真要把人类数学家，逼上绝路啊...... 费马大定理，30个小时1000个Claude Fable 5.2组队，完成了完整的形式化证明。 就在今天，一人+Claude竟把13年前获证的「三元哥德巴赫猜想」证明形式化了。 这波操作出自独立开发者Charlie Reams之手，狂敲19.4万行Lean 4代码，全库上下
这一回，人类数学家恐怕真要感到压力了。
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）还大。
第三处，纠错顺带纠到了别人头上。
Helfgott原证明引用了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²/κ，缩水超过四分之三，可它依然大于零。
原作者亲自下场，揭开两大「未竟前提」
事情传开后，大家最想知道的是——
自己的成名作被AI挑出错、又给修好，原作者Harald Helfgott会怎么反应？
Helfgott本尊很快出现在X上，态度相当坦诚：今年10月4日，Charlie Reams就已私下联系过他，告知形式化工作跑通了。
这一个月里，一人一AI又办成一件大事——
整个证明所依赖的外部额外假设（公理），从最初的5项一路削减到只剩2项！
眼下这个仓库里，全部解析数论推导逻辑已100%形式化、零sorry，但Lean外部仍挂着两项既有的数值验证结果当假设：
Platt的广义黎曼猜想（GRH）数值验证，以及偶数哥德巴赫猜想的局部验证，后者验到4x10^18。
把这两块人类早就算好、却还没搬进Lean内核的「巨型数字垫脚石」放进去，三元哥德巴赫猜想这座大厦就严丝合缝了。
超级智能正定义，什么叫「证完了」
几百页的证明算不算「证完了」，过去得等少数几位专家啃上几年，啃完也未必敢拍胸脯。
如今标准换成了另一句话：过没过内核。
也许用不了多久，数学界最硬核的同行评审就只剩一句话：
以后投稿或许会多一道关卡：先把证明交给Claude跑一遍，确认没有一处sorry，再谈发PDF的事。
参考资料：
https://x.com/jdlichtman/status/2120301890504441905
