数学里程碑：Claude 用 11 天完成费马大定理的形式化证明
Anthropic 表示，一个 Claude 模型经过约 11 天大致自主运行，首次在 Lean 中完成了费马大定理的端到端形式化，并通过计算机检查。该模型并未重新发现新的数学证明，而是将安德鲁·怀尔斯已有的证明转换为 Lean 证明助手能够逐步验证的形式。Claude 生成约 1300 万行 Lean 代码，证明了约 3.03 万个定理，其中近 2.95 万个被纳入最终证明。多个 Claude 智能体通过 Prove2Me 平台协作，追踪定理依赖关系并并行完成任务。Lean 仅使用三条标准公理完成最终检查，完整证明已发布在 GitHub 上。这项成果显示，人工智能自动形式化大型数学成果取得进展，但它不是新的数学发现，也不能取代人类审阅。
本文来源：AIbase，仅供学习参考，版权归原作者所有。