AI数学推理能力迎来重大突破！Anthropic近日宣布，Claude模型在清华姚班校友彭天翼发起的项目中，用时仅11天，基本自主完成了费马大定理的首个端到端、经计算机验证的形式化证明。Claude生成了约1300万行Lean 4代码，证明了约2.95万个中间定理，规模达数学定理库Mathlib的5倍以上。该证明由机器逐行验证，从机制上杜绝了AI幻觉问题。这是迄今最大的Lean项目，标志着AI在高阶数学推理领域从"辅助"迈向"可信任的自主证明"阶段，成为AI数学推理能力的里程碑事件。