Claude仅用11天完成费马大定理完整计算机可验证证明：1300万行Lean代码验证2.95万条中间定理
talkingdev • 2026-09-07
3200 views
Anthropic宣布其AI系统Claude在Lean证明助手中仅用11天，就完成了费马大定理的首个完整计算机可验证证明。该定理由Andrew Wiles于1995年首次给出手工证明，其形式化验证长期被视为极其复杂的工作。Claude生成的证明通过Prove2Me和Lean双重验证，涉及约1300万行代码，并证明了29500条中间定理。这一成果展示了AI在数学形式化验证中的巨大潜力，有望显著降低定理证明的人工成本，推动数学研究与AI辅助推理的深度融合。
核心要点
- Claude在11天内用Lean完成费马大定理首个完整计算机可验证证明。
- 该证明涉及约1300万行代码，并验证了29500条中间定理。
- 结果表明AI可大幅减轻数学定理形式化验证的繁重工作。