RecodeX 重构消息，独立开发者Charlie Reams借助Claude Code完成三元哥德巴赫猜想的形式化证明，累计产出19.4万行不含sorry的Lean 4代码，全部推理均通过机器严格验证。过程中AI自主发现2013年Harald Helfgott原版证明中的11处问题，包括常数写错、不等式不成立、引用数据偏差、主弧尺度混淆等，并完成修补。此后两人将证明所依赖的外部额外假设从5项精简至2项已有的公开数值验证结果，进一步推进证明的严谨性闭环。