费马大定理的形式化
内容摘要
本文报道了费马大定理的首个完整计算机验证证明，该证明由Claude AI模型与研究人员合作生成。在一项实验中，Claude主要在11天内自主工作，使用Lean证明助手和Prove2Me协作平台，形式化了一个该定理的证明。最终的证明包含1300万行Lean代码，验证了29,500个中间定理。这项工作遵循了安德鲁·怀尔斯爵士1995年证明的简化版本。作者们，由Anthropic研究员彭天益领导，强调虽然定理本身并非新成果，但这一成就对形式化数学领域具有重要意义。自动化形式化可以帮助验证复杂证明、发现数学文献中的错误，并减轻人类审稿人的负担。帝国理工学院的凯文·巴扎德审查了该证明，称赞这是迈向现代数学文献自动形式化的重要一步。文章最后指出，该项目展示了人工智能在严格验证数学结果和维护数学知识可信度方面的潜力。
(来源：Anthropic)