把数学证明变成一份“不能跳步的程序”
想象你请人检查一份极长的合同。人类专家会依靠经验，略过显然成立的部分；计算机却要求每个定义、每次引用和每一步推导都写清楚，少一个环节也不放行。数学的形式化证明也是这样：它不是请 AI 再讲一遍证明，而是把人类证明翻译成机器可以逐条验算的代码。
据 Nature 报道，Anthropic 的 Claude 高级原型首次把费马大定理的既有证明转成了可由计算机核验的形式化代码。整个项目约有 1300 万行，Claude 用了 11 天。报道还称，同一工程此前预计需要人类投入 10 年。这个对比很醒目，但目前所有关键数字都来自这一篇报道，尚缺官方代码、独立复现和更多信源交叉核验。
它没有重新证明费马大定理
费马大定理说的是：当整数 时，不存在正整数 、、 满足
这句话很短，证明却极其复杂。Andrew Wiles 与 Richard Taylor 在 1994 年完成了公认的人类数学证明。本次工作处理的正是这份既有证明：Claude 协助把自然语言中的数学论证翻译成形式系统，而不是独立发现一条新的证明路线。
两者的差别很重要。自然语言证明允许数学家写“显然”“同理可得”，因为同行知道中间省略了什么。形式化证明不能这样做。它必须把定义、前提和推导关系全部编码，交给证明助手核验。Lean 是这类工作常用的证明编程语言；它和 Coq 一样，不会因为作者有名就相信结论，只按预先声明的逻辑规则检查每一步。
因此，最后的可信度并不来自 Claude“说自己做对了”，而来自证明助手的小型内核能否机械检查通过。检查通过说明形式推导成立，却不表示软件理解了证明是否优雅、重要，或为何值得研究。
1300万行意味着什么？
这个数字首先说明的不是证明变得更简洁，而是机器要求极高的细节密度。可以把它理解为：数学家交出的是一张足够专业的人能读懂的施工图，形式化工程则要继续补齐每个尺寸、接口和验收步骤，让检查系统不必依赖常识。
Nature 引述 Rutgers University 数论学家 Alex Kontorovich 的评价：机器能把人类数学家的工作转成如此庞大的、可核验的证明，令他震惊。Anthropic 于 9 月 4 日宣布这项成果。
报道还把它与另一项 AI 辅助形式化工作相比：今年 2 月，AI 完成了对 Maryna Viazovska 在 8 维和 24 维空间球堆积成果的认证。Imperial College London 数学家 Kevin Buzzard 判断，这次费马大定理项目的复杂度可能又高出一个数量级。University of Toronto 数论学家 Daniel Litt 也据此评价，如果系统能形式化费马大定理，它或许能处理非常广泛的数学成果。这些仍是数学家的判断，不是已经经过系统测试的能力边界。
真正值得关注的是研究流程
形式化和自动证明不是一回事。前者把已有数学完整编码并核验；后者让机器自己寻找证明路线。LLM——也就是 Claude 这类大语言模型——可以协助翻译表达、补足步骤和搜索可用路径，但最终把关的仍是证明内核。
这次工作的分量，也正在这里。过去，形式化一项大型数学成果常被视为漫长的人工工程。如果 11 天这一结果能够被完整复现，它意味着 AI 可能大幅压缩“把论文改写成机器可检查对象”的时间。数学家便能更系统地检查庞大的知识库，也可能发现一些长期被接受的结果存在缺口。Buzzard 对 Nature 表示，两年前，这种设想还像幻想。
它并不等于 AI 已经能够取代数学研究。更准确的说法是：AI 可能先改变研究成果的验收方式。证明不再只由同行阅读，也能多一道逐步、机械的逻辑检查。
局限与未知
- 1300 万行的统计口径尚不清楚：是否包括 Lean 代码、依赖库、生成文件和中间产物，报道没有披露。
- “11 天对 10 年”的比较缺少估算主体、工程范围和计算方法，不能直接当作严格的效率倍数。
- 现有材料没有提供代码仓库，也没有说明成果是否已经完成公开编译、专家审查和第三方复现。因此，“首次”和“完成”等核心说法目前仍应视为 Nature 转述的单一信源结论。