Anthropic 宣布，Claude 在基本自主运行 11 天后，将怀尔斯路线的费马大定理证明完整转换为 Lean 可逐步校验的形式，生成约 1300 万行代码并证明约 3.03 万个定理。这是首个端到端经机器验证的费马大定理 Lean 证明，本质是大规模自动形式化，而非新的数学发现。