费马大定理是过去半个世纪最著名的数学成果之一。9月4日，人工智能（AI）公司Anthropic宣布，其Claude模型仅用11天，就将英国数学家安德鲁·怀尔斯1995年完成的费马大定理证明转化为计算机可逐步验证的形式化证明。
Anthropic在社交平台X上发布证明结果。图片来源：Anthropic社交平台X截图
“机器竟然能够把人类数学家的工作转化为一份长达1300万行、坚不可摧的证明，这完全让我震撼。”美国罗格斯大学数论学家亚历克斯·孔托罗维奇说。
英国《自然》网站在7日发表的文章中称，这一成果表明，AI将在数学家的工作中发挥越来越重要的作用，不仅可帮助检验数学证明，也可能参与产生新的数学推理。按照目前的发展速度，AI审查整个人类数学知识库，已不再是遥不可及的事，甚至可能发现一些广为人知的数学结论中是否藏着错误。而在两年前，这还只是幻想。
数学证明是一连串严密的逻辑步骤，只要其中一环出错，整个证明就可能坍塌。面对动辄数百页、涉及大量复杂理论的证明，单靠人工逐一核验每个环节，几乎是不可能完成的任务。
费马大定理就是一个典型。1637年，法国数学家皮埃尔·德·费马提出了这个命题：当整数n大于2时，不存在满足xn+yn=zn的正整数x、y、z。
1908年，德国曾悬赏一笔奖金（今天约合100万至200万美元），向数学家征集费马大定理的证明。仅第一年，就收到了621份证明，但没有一份站得住脚。直到上世纪90年代，英国数学家安德鲁·怀尔斯才真正攻克了这一难题。他在1995年5月发表了长达129页的证明，横跨数论多个分支，汇集了大量现代数学成果。该证明通过了数学界审查并得到认可，费马大定理就此尘埃落定。
数学家安德鲁·怀尔斯于1995年发表了费马大定理的证明，距离皮埃尔·德·费马提出该猜想已过去了350多年。图片来源：英国《自然》杂志网站
所谓“形式化”证明，就是把数学证明翻译成一种极其严格、精确的语言，让计算机能够自行验证其中的每一步，而不需要依赖人的主观判断。
近年来，AI进行数学形式化的能力进步很快。今年2月，AI辅助数学形式化取得一项里程碑式进展，成功对菲尔兹奖得主玛丽娜·维亚佐夫斯卡关于8维和24维空间中最有效球体堆积方式的研究成果完成了计算机验证。不过，英国伦敦帝国理工学院数学家凯文·巴扎德说，费马大定理的形式化工作“可能更困难一个数量级”。
