Anthropic 于 2026 年 9 月 4 日发表研究文章，表示 Claude 已完成费马大定理（Fermat’s Last Theorem，FLT）的完整 computer-checked proof。根据 Anthropic 的说法，Claude 以大部分自主的方式工作约 11 天，把一个供人类读者理解的长篇数学证明，转换成 Lean proof assistant 可以逐步检查的形式。
这项成果的背景不是 AI 突然找到一个人类未知的初等证明。Andrew Wiles 早在 1995 年已经发表 FLT 的第一个正确证明；这次的主题是 formalization，即把已有的数学推理改写成计算机可以用算法核查的形式。Anthropic 自己也把新意放在 verification，而不是把它包装成另一个 Riemann hypothesis 式的全新数学结果。
Anthropic 表示，Claude 在过程中写了约 1,300 万行 Lean，并完成 30,300 个中间 theorem，其中 29,500 个最终被纳入证明。这个规模很能说明形式化的工作量：人类证明会省略被认为明显的步骤，但 Lean 要求每一个逻辑连接都能被检查。文章又表示，最终 proof 超过 Mathlib 主要社区数学库五倍以上。
背后的工作流并不是一个单一聊天窗口。Anthropic 说，数十个 Claude agents 通过 Prove2Me 协作，先用 directed acyclic graph 管理 theorem statements，再并行处理定义、子定理和证明。这种设计针对了长任务常见的记忆衰退和状态失焦问题：代理需要共享一张可搜索、可重用、可追踪的证明图。
Lean 的价值在于它会检查形式逻辑，而不是因为模型说「已证明」就接受结果。Anthropic 表示，完成的 proof 已经由 Lean 核查，使用 Lean 的三个标准公理；文章也提到 Kevin Buzzard 查看过 proof，以及另一个 comparator 确认 theorem statement 与 Mathlib 的 FLT statement 相符。这些是重要的可追溯信号，但目前仍应把它视为 Anthropic 的研究发布和开放 proof artifact，读者仍要按自己的标准重跑、审阅和独立验证。
对 AI agent 研究来说，这个案例显示瓶颈正在由「模型能否产生一段看似合理的推理」转向「代理能否维持长期状态、拆分依赖、处理失败并交付可核查的 artifact」。Anthropic 说，早期尝试曾因 agents 失去项目状态而失败，最后靠共享 DAG、编译加速和 theorem search 才让多代理流程稳定下来。
对数学社群来说，formalized proof 不会取代人类可读的 exposition，也不会自动回答研究结果是否值得相信的全部问题；它更像一个可重跑的逻辑底座。当 AI 产生更多证明或研究假设时，能否同时交付 Lean、Rocq 或其他 proof assistant 的形式化版本，可能会成为降低 referee 负担和捕捉错误的重要工作流。
这条新闻最值得记住的不是「AI 证明了费马大定理」这句容易误读的标题，而是 agentic research 开始把协作、形式化、编译和验证放进同一个长任务。数学新意、工具可核查性、研究者审阅和独立重现，仍然是四件不同的事；把它们分开，才不会把一个很有价值的验证工程误报成 AI 取代数学家。
