Anthropic宣布，其AI模型Claude在基本自主运行11天后，完成费马大定理的首个端到端、可由计算机检查的Lean形式化证明。该项目生成约1300万行Lean代码，证明约3.03万个定理，其中约2.95万个中间定理纳入最终证明，整体由Lean完成验证。项目由研究人员发起，借助Prove2Me平台和多智能体协作完成，消耗约60亿输出Token，完整证明已公开至GitHub。
Anthropic宣布，其AI模型Claude在基本自主运行11天后，完成费马大定理的首个端到端、可由计算机检查的Lean形式化证明。该项目生成约1300万行Lean代码，证明约3.03万个定理，其中约2.95万个中间定理纳入最终证明，整体由Lean完成验证。项目由研究人员发起，借助Prove2Me平台和多智能体协作完成，消耗约60亿输出Token，完整证明已公开至GitHub。