Anthropic 称 Claude 协助用 Lean 形式化费马大定理

Anthropic 发布了一项新研究，介绍 Claude 如何协助研究人员在 Lean 中形式化费马大定理。Lean 是一种证明助手，会逐行检查数学论证是否成立。这项工作并不是说模型独立发现了新的证明，而是展示 AI 在数学中的一个更实际前沿：把高度压缩、依赖大量背景知识的人类证明，转化为机器可以检查的形式化代码。

费马大定理是数学史上最著名的结果之一。Andrew Wiles 在 20 世纪 90 年代完成证明，但原始证明依赖深层数论和代数几何工具。形式化这样规模的结果，与写一篇面向读者的解释性证明完全不同。每个定义、定理依赖、变换和逻辑步骤都必须明确到足以让证明助手验证。即便对专家来说，这也是漫长而细致的工程。

Anthropic 在文章中把 Claude 描述为证明工程中的协作者。模型可以提出 Lean 代码，帮助把数学表述翻译成形式语法，修复报错，并建议如何连接中间引理。研究人员仍然需要判断路线是否数学上可靠，审查生成代码，并在证明状态复杂时继续引导系统。换句话说，这项工作体现的是 AI 辅助能力的进步，而不是人类数学判断的消失。

这一成果重要，是因为形式证明是语言模型较难通过的一类测试。模型可能写出听起来很有说服力但其实错误的文本，而 Lean 不会接受逻辑不成立的证明。这形成了一种自动反馈机制，大量错误会被系统直接暴露。成功标准也随之改变：研究人员不只看 AI 能不能写出漂亮的证明段落，而是看它能否在严格形式系统中持续帮助完成可验证工件。

对更广泛的 AI 市场而言，这项研究指向一种知识工作模式。模型可以承担繁琐的翻译、搜索和修复循环，帮助科学和技术团队提高速度。形式数学、程序验证和安全关键工程都不只需要流畅文字，还需要可审计推理链和外部工具能够检查的结果。如果模型更擅长在这些约束中工作，它们就可能让专家团队更高效，同时保留专家审查带来的可信度。

Anthropic 也谨慎地把这项工作称为一步进展，而不是终点。大规模定理形式化仍然困难，系统仍依赖人类规划和纠错。但这篇研究加入了一个越来越清晰的趋势：前沿 AI 系统正在从“回答得像不像”转向“能否在严苛环境中产出可验证成果”。