GitHub上一个名为calr3/ternary-goldbach的仓库，近来在数学圈与AI圈同时刷了屏。打开其cde-moebius分支，能看到一座庞大的代码工程：19.4万行Lean 4代码，外加若干辅助脚本与技术文档。真正抓人眼球的不是体量，而是一个数字，零sorry。
熟悉Lean的人清楚这两个字的分量。sorry是该语言中标记“此处尚未证完”的占位符，一个形式化项目是否成立，关键就看有没有留这种后门。零sorry，等于宣告每一行推理都通过了内核的严苛检验，没有一处含糊。
这份代码形式化的对象，是三元哥德巴赫猜想，也叫弱哥德巴赫猜想：任何一个大于5的奇数，都能写成三个质数之和。需要区分的是，坊间常说的"1+1"其实是强哥德巴赫猜想——每个大于2的偶数都能拆成两个质数之和，那个问题至今悬而未决。
弱版本的攻克者是数学家Harald Helfgott。2013年，这位秘鲁学者宣布彻底解决了这个困扰人类271年的难题，一度轰动全球。可掌声过后，麻烦随之而来：证明实在太长太繁，仅主干手稿就厚达300页，塞满了连篇累牍的不等式放缩与常数运算。此后十余年，Helfgott本人陆续推出多个版本修订细节，但冗长的演算劝退了几乎所有想通读全文的人——放眼全球，找不出几位数学家愿意把每个常数从头核到尾。
核不下去的根源在于“全是数”。这份证明用的是圆法：把问题拆成主弧与劣弧两块，主弧好比“收入”，劣弧好比“开销”，只要收入稳稳压过开销，定理即告成立。这种论证靠人眼校验，翻到第50页大抵就败下阵来。
独立开发者Charlie Reams决定换条路走，把这块硬骨头丢给Claude Code。分工相当明确：他负责设定顶层目标、拆解任务指令；绝大多数Lean形式化代码、自动化脚本乃至文档，均由Claude Code一手包办。类似的打法此前已有先例，费马大定理的形式化证明，正是由1000个Claude Fable 5.2组队、耗时30小时完成的。
真正让数学圈坐不住的，是过程中的一段插曲。Claude在逐行核对时发现，2013年的原版证明里竟藏着11处与原书对不上的地方，随后二话不说，把漏洞挨个补齐。仓库README中逐一列出了这些问题，其中三处最具代表性。
第一处是常数失准。书中(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的推导把两种尺度的主弧混在了一起，这一整段等于被推倒重搭。修补完成后，各项数字随之变动，主弧“收入”从原书的1.058259降到1.049，劣弧“开销”从1.00948涨到1.0376。两者之差，亦即证明的安全垫，从0.04877 x²/κ缩至0.0114 x²/κ，缩水超过四分之三。所幸这个数依然大于零，大厦未倾。
这场实验也让人重新掂量“证完了”三个字的分量。一份几百页的证明算不算证完，过去要靠少数几位专家花上数年去啃，啃完也未必敢打包票；如今，标准正换成另一句话，过没过内核。
至于证明本身的完备程度，也在这一个月里被继续推进。整个工作依赖的外部假设，已从最初的5项一路削减到只剩2项。眼下，仓库内的解析数论推导已100%形式化且零sorry，但在Lean内核之外，仍挂靠两项既有的数值验证结果作为前提，其一是Platt完成的广义黎曼猜想（GRH）数值验证，其二是偶数哥德巴赫猜想的局部验证至4×10^18。这两块由人类早已算好、只是尚未搬进Lean内核的巨型数字垫脚石，构成了整座大厦仅剩的缺口；补入之后，三元哥德巴赫猜想的形式化证明便告严丝合缝地闭环。
而被AI“改了作业”的Helfgott本人，反应出乎意料地平和。事件传开后，他很快在X上现身，坦诚回应了外界的好奇，早在10月4日，Reams就已私下告知他，形式化工作已经跑通。
