开发者借助Claude Code完成三元哥德巴赫猜想形式化证明

独立开发者Charlie Reams借助Claude Code，完成三元哥德巴赫猜想的Lean 4形式化证明。项目累计形成约19.4万行代码，未使用表示证明缺口的“sorry”占位，形式化推理通过机器检查。在整理数学家Harald Helfgott于2013年发表的原证明时，项目发现并修补了11处问题，涉及常数、不等式、引用数据和主弧尺度等。证明依赖的外部附加假设由5项缩减至2项，剩余两项为已公开的数值验证结果。