Anthropic 开源费马大定理形式化证明：Claude 写出近 3 万个定理
Anthropic 在 GitHub 开源了费马大定理的完整 Lean 4 形式化证明。该证明由 AI 智能体生成，包含 29,511 个定理和超 1300 万行代码，并通过了两个独立内核的严格验证。这意味着 AI 首次独立攻克了现代数学中最复杂的宏大证明形式化工程。
Anthropic 在 GitHub 开源了费马大定理的完整 Lean 4 形式化证明。该证明由 AI 智能体生成，包含 29,511 个定理和超 1300 万行代码，并通过了两个独立内核的严格验证。这意味着 AI 首次独立攻克了现代数学中最复杂的宏大证明形式化工程。