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