Anthropic 于近日宣布，旗下 AI 模型在基本自主运行11天后，成功完成了对费马大定理（FLT）的首个端到端、经过计算机检查的 Lean 形式化证明。这项工作并非由 AI 重新发现该定理的数学证明，而是将已有数学证明转换为 Lean 证明助手能够逐步验证的形式。Lean 是一种用于编写和验证形式化数学证明的证明助手，能够通过计算机检查证明中的逻辑步骤。 在这一过程中，Claude 生成了约1300万行 Lean 代码，并证明了约3.03万个定理，其中约2.95万个中间定理最终被纳入费马大定理的完整证明。整个证明由…