Claude 辅助完成 19 万行代码 形式化三元哥德巴赫猜想证明

独立开发者 Charlie Reams 借助 Claude Code 完成三元哥德巴赫猜想的形式化证明，累计产出 19.4 万行零 sorry 的 Lean 4 代码，所有推理均通过机器严格验证。过程中 AI 自主发现 2013 年 Harald Helfgott 原版证明里的 11 处问题，包括常数写错、不等式不成立、引用数据偏差、主弧尺度混淆等漏洞并完成修补。后续二人又将证明依赖的外部额外假设从 5 项精简至仅剩 2 项已有的公开数值验证结果，大幅推进了该证明的严谨性闭环。这一事件也推动数学界对「证明完成」的判定标准向机器可验证的形式化方向转变。