11天、30万美元：AI攻破358年数学难题的最后一关

Anthropic的AI模型Claude在11天内完成了费马大定理的形式化证明，生成了1300万行Lean代码。这项工作不仅展示了AI在形式化数学证明方面的强大能力，还为未来的数学验证提供了新途径。尽管成本高达30万美元，但其意义在于将复杂的人类证明转化为机器可独立验证的形式。