Anthropic 于 9 月 4 日对外披露，其旗下 AI 模型 Claude 在一次长达 11 天的自主运行中，完成了费马大定理的完整形式化证明。这项成果被描述为首个端到端、且通过 Lean 证明助手严格校验的版本，意味着从定理陈述到最终证明的每一个逻辑步骤，均由机器自动生成并验证。

费马大定理由法国数学家皮埃尔·德·费马在 1637 年提出，直到 1994 年才由安德鲁·怀尔斯给出完整证明，其原始论证篇幅超过百页，涉及现代数论多个深层分支。将如此复杂的证明转化为 Lean 可识别的形式化语言，历来被视为一项高难度工程，此前相关工作多停留在局部模块验证阶段。

本次运行中，Claude 被赋予较高自主权，系统仅在关键节点提供有限监督。据 Anthropic 介绍，模型在 11 天内持续推理、迭代和修正自身策略，最终生成一套完整的 Lean 代码库，其中包含定义、引理及最终定理的验证记录。整个过程未依赖人类预先编写的证明框架。

这一成果的意义不仅在于单个定理的突破。形式化证明在软件验证、数学研究和 AI 安全等领域具有工具性价值，而 AI 能够长时间独立处理此类任务，也为自动化数学发现和验证提供了新的可能性。Anthropic 表示，后续将进一步探索 Claude 在更广泛数学任务中的自主推理能力。

不过，业内也有研究者提醒，当前成果尚需公开复现和独立审计，其方法论是否适用于其他复杂数学问题仍有待检验。Claude 此次所展示的持续规划与自我纠错能力，至少已为 AI 与形式化方法的结合提供了一个值得关注的实证案例。