📖 AI 总结

文章报道了Anthropic宣布Claude完成费马大定理首个端到端形式化证明的消息。这项工程由清华姚班校友、哥伦比亚大学助理教授Tianyi Peng主导，耗时仅11天，产出约1300万行Lean代码和超过3万个中间定理，规模是Lean核心数学库Mathlib的5倍以上。Claude并未提出新证明，而是将人类数学家可读的证明完整翻译为计算机可逐行验证的形式化语言，消除了所有“显然”步骤。过程中，团队通过Prove2Me平台将多个Agent组织为协作系统，解决了早期协作混乱问题，最终消耗约60亿个输出Token。该成果被数学家Kevin Buzzard评价为“非凡的自动形式化成果”，其意义在于表明大规模复杂数学文献的形式化工作可能首次具备自动化提速条件，而不再依赖多年人工工程。