Claude 修正费马大定理领域证明：19.4 万行源码零疏漏，揪出原版多处错误

独立开发者 Charlie Reams 借助 AI 助手 Claude，完成了对 2013 年 Harald Helfgott 关于「三元哥德巴赫猜想」证明的形式化工作。该项目在 GitHub 仓库 calr3/ternary-goldbach 中上线，包含 19.4 万行 Lean 4 代码及技术文档，且未使用任何表示证明暂缺的'sorry'标记。在三元哥德巴赫猜想领域，Harald Helfgott 于 2013 年宣布证明了大于 5 的奇数均可表示为三个质数之和。其原始手稿长达 300 页，依赖复杂的圆法计算和大量常数推导，导致人工核对困难且易出错。Claude 不仅完成了代码实现，还自主发现了原证明中的多处错误。具体包括将关键常数从错误的 0.5 修正为正确的数值、指出书中关于积分上界的不成立不等式，以及通过改变拆分方法解决了 Ramaré 1995 年论文引用中的误差问题。此外，AI 助手还重构了原证明中将两种尺度的主弧混淆的部分，重新计算了主弧与劣弧的差值，虽然证明的安全垫数值有所缩小，但依然满足大于零的要求，确保了定理成立。原作者 Harald Helfgott 通过社交媒体 X 对此事发表了回应，并确认 Charlie Reams 曾在今年 10 月 4 日与其私下沟通形式化进展。双方合作进一步将证明依赖的外部假设从最初的 5 项削减至仅存的 2 项。经过此次形式化处理，整个证明逻辑在 Lean 内核中实现 100% 形式化，仅剩余两项基于人类已验证的数值结果作为前提假设：Platt 对广义黎曼猜想的数值验证以及偶数哥德巴赫猜想至 4×10^18 的局部验证。这一成果标志着数学证明标准的变化，即从依赖少数专家耗时多年的纸质审阅，转向通过机器内核验证零疏漏来确立定理的完整性，为人工智能在基础科学领域的应用提供了新的范式。