形式化费马大定理

Anthropic 的一篇文章，介绍其分享的首个经计算机完整校验的费马大定理证明。文中说明 Claude 在约 11 天里基本自主地用 Lean 编程语言写出该证明，并描述了形式化的完成方式，以及这项工作对数学研究可能意味着什么。文章还简述了费马大定理的背景与 1995 年 Andrew Wiles 的原始证明。