💡 站外导读：在基础科学与纯数学领域，人类严谨性历来被奉为至高无上的圣殿。然而，英国独立开发者查理·里姆斯（Charlie Reams）日前完成的一项惊人壮举，彻底震撼了全球数学界与计算机科学界：他借助 Anthropic 旗下的命令行代码智能体 Claude Code，成功完成了对著名数论难题——“三元哥德巴赫猜想”（弱哥德巴赫猜想）的全流程机器形式化证明！整个工程累计产出高达 19.4 万行 Lean 4 代码，最不可思议的是，代码中没有出现哪怕一个允许逻辑跳过的 sorry 占位符，所有数学定理推导均通过了交互式定理证明器的严格语法与代数校验。更令人惊叹的是，AI 在形式化推演过程中，自主揪出并修补了 13 年前人类顶级数学家原版证明中的 11 处隐蔽数学漏洞！
哥德巴赫猜想是数论史上最著名的未解难题之一，其弱形式（三元哥德巴赫猜想）陈述为：“任何大于 5 的奇数都可以表示为三个质数之和”。早在 2013 年，秘鲁著名数学家哈拉尔德·埃尔夫戈特（Harald Helfgott）曾发表了一篇长达数百页的手稿，宣称从理论上彻底证明了弱哥德巴赫猜想。尽管国际数学界普遍认可其证明的大致框架，但由于手稿计算量极其浩瀚、引理错综复杂，人类审稿专家几乎无法对每一行代数推演进行绝对无误的逐字核验。
整整十三年过去，当大语言模型进化至具备高阶数理抽象与代码推演能力的今天，独立开发者 Charlie Reams 选择以 Lean 4 形式化语言为标尺，联手 Claude Code 重新挑战这座数学高山。这项耗时数月的极客工程，最终交出了一份令整个科学界起立致敬的硬核答卷。
一、19.4 万行“零 sorry”代码：机器证明的极致严谨闭环
在 Lean、Coq 或 Isabelle 等形式化定理证明语言中，当研究者遇到一段极其繁琐、暂时无法完成推导或意图跳过的引理时，通常会写入 sorry 关键字来欺骗编译器，让下游证明继续进行。因此，在形式化数学社区，“包含 sorry”的证明往往被视为未完工的草稿。
Charlie Reams 在 GitHub 公开的完整仓库中，19.4 万行 Lean 4 代码实现了彻底的“零 sorry（Zero Sorry）”！这意味着整套庞大的数学证明大厦，从最基础的皮亚诺算术公理、群论、傅里叶分析、狄利克雷级数，到极其晦涩的哈代-利特尔伍德圆法（Circle Method），全部由机器内核（Lean Kernel）完成了严丝合缝的类型检查与逻辑推导，不存在任何逻辑模糊地带。
二、超越人类审稿极限：AI 自主揪出并修补 11 处致命漏洞
在这场史诗级的人机协作中，Claude Code 展现出的并不仅仅是死板的代码编写工具属性，而是化身为一位具备极致敏锐嗅觉的“超人类审稿员”。
在将 Helfgott 于 2013 年发表的原始论文逐段翻译并形式化重构的过程中，AI 自主发现了多达 11 处关键数学纰漏。这些漏洞人类顶级同行评议审稿人历经 13 年都未能察觉，具体涵盖：
- 常数笔误与代数符号反转：在多处复杂的渐近展开式中，原作者无意中写错了关键常数的阶数与符号；
- 边界不等式局部不成立：在复积分鞍点近似法推导中，部分不等式在特定极限临界点无法收敛；
- 外部引用数据偏差：引用的早期数论计算文献中存在未经核实的离散数据截断误差；
- 主弧（Major Arcs）尺度混淆：在圆法分析的核心环节，对主弧与次弧的分割区间定义存在微小重叠与逻辑缺口。
面对这些曾足以推翻论文严谨性的漏洞，Claude Code 展现了惊人的推演韧性：它不仅准确定位了逻辑断裂点，更结合现代解析数论的最新工具，逐一完成了严格的引理重写与修补，确保了最终 Lean 4 证明大厦的绝对坚固。更具学术价值的是，Reams 团队借助 AI 的化简能力，将该证明所依赖的外部额外未证明假设，从最初的 5 项大幅精简至仅剩 2 项已在超级计算机上完成海量穷举验证的公开数值结论！
三、科学范式重构：从“同行评议信任”迈向“机器形式化验证”
长期以来，纯数学的发展受制于“证明的可阅读性危机”。随着现代数学前沿越来越深奥，像望月新一关于 ABC 猜想的长达数百页的 IUT 理论，往往因为全球仅有极少数专家能够读懂而陷入旷日持久的学术争端与互不信任。
Charlie Reams 与 Claude Code 的成功，向全球学术界昭示了一条通往“绝对真理”的确定性通路：未来数学界的“证明完成”，判定标准将不可逆转地从“依赖数位权威专家的主观同行评议”，转向“完全依赖开源交互式证明器内核的物理代码跑通”。AI 正在将数学研究从作坊式的手工演算，推向工业化、模块化、可自动装配的机器证明大生产时代。
四、传统人工同行评议与 AI 形式化验证全维度横向评测
为了直观展现基于 Claude Code + Lean 4 的形式化数学突破对基础科学研究带来的颠覆性变革，我们对两种验证范式进行深度对比：
| 核心对比维度 | 传统学术同行评议 (Peer Review) | Claude Code + Lean 4 机器形式化验证 |
|---|---|---|
| 严密性与信任基石 | 基于审稿人精力与声誉的主观抽查（易遗漏） | Lean 4 内核每一步严格代数校验，绝对无漏 |
| 隐蔽漏洞识别力 | 极低（Helfgott 原作 11 处漏洞历经 13 年未察） | 极高（类型推导与符号反差自主触发语法拦截） |
| 知识模块化复用 | 分散在长篇 PDF 论文中，他人难以直接引用 | 19.4 万行纯净代码直接并入 Mathlib 全球数学库 |
| 工程推进与迭代周期 | 动辄数年，审稿人常因论文浩瀚而放弃或延期 | 单人借助智能体高并发交互，数月内攻坚完成 |
| 终极验证状态 | “大致合理，缺乏严重硬伤”的或然性结论 | Zero Sorry，编译器 Exit 0 的确定性数理铁证 |
📝 站长洞察 (Editor’s Insight)
Charlie Reams 这次带给全球科技界的震撼，其意义甚至远远超越了攻克弱哥德巴赫猜想本身。它从最底层的认识论层面，打破了“大语言模型只会进行概率性胡说八道与逻辑幻觉”的陈旧偏见。
当我们将以 Claude Code 为代表的高阶智能体，与 Lean 4 这种具备确定性因果约束的形式化验证系统深度绑定时，AI 的概率发散能力就变成了寻找证明路径的“超级探索雷达”，而形式化编译器则成为了绝不妥协的“终极裁判员”。这种“大模型探索生成 + 严谨编译器硬核裁判”的双螺旋架构，不仅将彻底重写基础数学、理论物理的科研路径，更将深刻改变商业软件工程中的底层安全验证——在不远的将来，不能通过形式化机器证明的系统，将无法被允许部署在人类社会的关键生产设施之上。
Claude Code 能用于数学定理形式化证明吗？
可以。本文案例显示，Claude Code 可配合 Lean 4 将复杂数论证明逐步形式化，并通过定理证明器内核完成严格校验，适合高复杂度、强逻辑约束的数学工程。
什么是 Lean 4 的零 sorry 证明？
“零 sorry”指证明代码中不使用 sorry 占位符跳过未完成部分，意味着每一步推导都已被形式化补全并通过内核检查，证明更完整、更可验证。
AI 真的能发现论文里的数学漏洞吗？
在本文案例中可以。Claude Code 在形式化重构过程中识别并修补了 11 处原论文漏洞，说明 AI 不仅能写代码，也能辅助做严谨的数学审查与验证。
如何用 Lean 4 复现这类大规模证明？
先把命题拆成可复用的引理链，再用模块化文件组织证明。优先补齐基础库与定义一致性，借助自动化战术处理重复步骤，最后用 CI 持续跑全量验证，避免后期回归。
AI 辅助形式化最容易踩哪些坑？
最大风险是“看似通过、实则语义偏移”。要严格对齐原论文定义、边界条件和符号约定，避免把非构造性结论误写成可构造证明；同时保留人工审查关键引理，防止自动补全掩盖漏洞。
![年度回顾：2023 年成为微服务的转折点 [译]](http://paooo.com/wp-content/uploads/2024/03/cb5d618e-prime-02-330x220.webp)
![Ilya——塑造世界的人工智能科学家 [译]](http://paooo.com/wp-content/uploads/2025/04/sre-ai-thumb-post-8709-1793853365-330x220.avif)
