人工智能在基础科学研究领域的应用正在创造历史。近日，独立开发者 Charlie Reams 借助Claude Code成功完成了对三元哥德巴赫猜想的形式化证明。此次突破累计产出了高达19.4万行且零 sorry 的Lean4代码，所有的数学推理均通过了机器的严格验证。
机器火眼金睛:自主揪出并修补13年前的11处漏洞
在这项艰巨的证明过程中，人工智能展现出了超越人类传统审稿的极致严谨性。
AI 在运行和推导中自主发现了数学家 Harald Helfgott 于2013年发表的原版证明中的11处关键问题。这些被成功揪出的漏洞涵盖了常数写错、不等式不成立、引用数据偏差以及主弧尺度混淆等多个维度，并且 AI 均逐一完成了修补。
在此基础之上，研究人员进一步将该证明所依赖的外部额外假设从最初的5项大幅精简至仅剩2项已有的公开数值验证结果，从而极大地推进了该证明严谨性闭环的构建。
推动范式转变:数学界的“证明完成”正迈向机器可验证时代
这一里程碑式的事件不仅攻克了数学史上的重要难题，也在更深层次上推动了整个数学界对“证明完成”这一概念的判定标准发生根本性转变——从传统的同行评议逐步向完全依靠机器可验证的形式化方向大步迈进。
