人工智能公司Anthropic利用Claude模型与多个智能体，在11天内完成了费马大定理的形式化证明。
数学界迎来里程碑。人工智能公司Anthropic成功创建了费马大定理的形式化证明。令人惊叹的是，一组人工智能智能体仅用11天就完成了这项艰巨任务，确认人类在1990年代提出的数学证明是完全正确的。
费马大定理曾困扰数学家几个世纪。直到1995年，数学家Andrew Wiles才终于证明了它。该定理非常直观：当n是大于2的整数时，不存在能满足等式aⁿ+bⁿ=cⁿ的正整数a、b和c。
虽然定理看似简单，证明却极度困难。17世纪，数学家Pierre de Fermat提出该谜题，并声称自己发现了一个绝妙的证明，可惜篇幅太长，写不下教科书页边的空白处。
此后，无数数学家尝试寻找证明皆以失败告终。Andrew Wiles曾秘密研究了7年，于1993年宣布突破。但复杂的证明环环相扣，一步出错就会全盘崩溃。Andrew Wiles的证明曾被发现有一处缺陷，他与合作者Richard Taylor花了大约1年的时间才将其修复。
将数学定理进行形式化，是解决该隐患的良方。形式化工作将定理转化为计算机代码，让机器接管推演，梳理逻辑并找出漏洞。目前，已经有200万行形式化数学代码存储在Mathlib数据库中。
今年早些时候，伦敦帝国理工学院的Kevin Buzzard在伦敦主持召开了专家会议。此前，他正致力于一个为期5年的项目，目标是将Andrew Wiles和Richard Taylor长达100页的证明用Lean编程语言进行形式化，以便对其进行机器校验。
Kevin Buzzard曾对项目充满信心，而人工智能的快速发展让他意识到，项目完成速度将远超预期。如今，Anthropic公司的进展彻底超越了这一努力，迅速解决了这个难题。
Kevin Buzzard在Anthropic公司发表的声明中指出，该证明没有留下任何除数学公理之外的假设。简而言之，问题已彻底解决。
Kevin Buzzard评价道，这不仅实现了代数、调和分析、几何和数论的自动形式化，也证明了人工智能自动形式化成果足够稳健，可作为后续研究的基础。这标志着人类向自动形式化现代数学文献迈出了一大步。
根据Anthropic公司发布的结果，其Claude模型在11天内不间断、自主地运行撰写证明。其间有多个不同的智能体协作，分别攻克定理的一小部分。
公司透露，人类专家偶尔会提供高水平指导以维持方向。其间智能体曾数次丢失对项目状态的掌控并停止协作。有趣的是，在引入人类数学协作工具Prove2Me后团队才取得成功，该工具能帮助智能体跟踪进度并决定下一步任务。
Anthropic公司的形式化代码库包含高达1300万行Lean代码，涵盖了约29500个作为垫脚石的中间定理。这使该证明的规模达到先前Mathlib所有成果总和的5倍以上，成为有史以来用Lean写成的最大规模数学证明。
原文：https://www.newscientist.com/article/2587839-fermats-last-theorem-formalised-by-ai-agents-in-just-11-days/