Fermat 是 Anthropic 于 2026 年 9 月启动的一个大型数学形式化研究项目，目标是把怀尔斯的费马大定理证明完整翻译成 Lean 形式化语言，由 AI 系统辅助完成审查与补全。2026 年 9 月 4 日，Anthropic 在 Science 上发表论文，正式公布这一成果。由于传统人工验证这类证明通常需要数年时间，Fermat 被视为检验 AI 能否承担严格数学验证工作的标志性尝试。
Fermat 项目的近期进展
当前焦点与观察点
围绕 Fermat 的讨论主要集中在三点。其一是技术路线：纯粹依赖神经网络的推理能力不足以支撑数万行级别的形式化证明，因此 Anthropic 采取了神经符号结合的架构，由模型生成证明片段、由 Lean 这样的证明助手承担最终的正确性判定。Gary Marcus 的评论也把这一点视作 AI 领域在'严谨性'问题上的方向性信号。
其二是行业竞争格局。OpenAI 随后在 arXiv 上发布 MechAlign，聚焦用 LLM 审查 Lean 项目级的语义对齐，说明数学形式化已成为头部 AI 公司共同投入的方向，围绕形式化数学的模型评测与工具生态正在快速成型。
其三是学术与工程层面的可持续性。把费马大定理这样规模的证明形式化，涉及大量数学结构建模和长程一致性维护，AI 的贡献边界——究竟是大幅加速，还是仅承担辅助性补全——仍是外界观察的焦点。后续值得关注的包括形式化产物的社区复用情况、相关工具链的开源程度，以及这一范式能否推广到费马大定理之外的其他未形式化重大成果。