费马大定理是过去半个世纪最负盛名的数学成果之一。9月4日，美国人工智能（AI）公司Anthropic宣布，其开发的AI聊天机器人Claude 的进阶版模型，将该定理首次转化为计算机验证代码。

　　该模型仅用11天便完成了这个人类预计需要10年才能完成的项目。这一结果表明，AI将在核验数学家的工作以及产生新的数学推理方面发挥越来越重要的作用。

　　美国罗格斯大学的数论学家Alex Kontorovich表示，AI能够将人类数学家的工作转化为长达1300万行的严谨证明，这一事实“令我大为震撼”。

　　加拿大多伦多大学的数论学家Daniel Litt表示：“如果它能形式化费马大定理，那么它大概就能形式化任何东西。”

　　1637年，法国数学家费马提出，当整数n>2时，关于x、y、z的方程xn + yn = zn不存在正整数解。这就是费马大定理，但费马只提出了这一论断，并未给出证明。1994年，数学家Andrew Wiles和Richard Taylor完成了对费马大定理的原始证明。这是20世纪数学领域的一个里程碑式成果。

　　近年来，AI数学能力的提升速度令数学家震惊。比如该技术“形式化”证明的能力，即将数学论证从自然语言翻译成一种形式化的、可计算机验证的代码，通常使用Lean编程语言。今年2月，AI实现了一个里程碑式成就，形式化验证了数学家Maryna Viazovska 获得2022年菲尔兹奖的成果——关于8维和24维球体堆积的问题。

　　用Lean语言形式化数学证明，需要向Lean编译器输入该证明依赖的所有预备概念和已知事实。为了实现越来越复杂的成果的形式化，数学家精心创建了一个名为MathLib的Lean代码库。

　　自2024年以来，英国帝国理工学院的数学家Kevin Buzzard领导了一个专门针对费马大定理的项目，旨在扩展MathLib，使其能够形式化Wiles和Taylor证明所需的数千页预备成果。

　　Buzzard估计项目需要10年才能完成。而Claude在11天内就完成了自己的Lean认证。但Anthropic称，与MathLib不同，Claude生成的代码包含29500个“中间定理”，因此不能立即被数学家使用。Buzzard表示，将其中一部分整合到MathLib中是可能的，但工作量巨大。因此，即便AI能够验证任何数学证明，数学界仍可能面临一个“噩梦般的场景”，因为出现了多个不兼容的Lean库。

　　不过，对于Claude的工作，Buzzard依然表示欢迎。“以前，我有99.9%的把握认为该证明是正确的，在Claude的工作完成后，我现在是100%确信。”

　　Buzzard指出，按照当前的发展速度，AI或许不久就能审视整个数学知识库，甚至可能发现某些著名结论是错误的。两年前，这还是个幻想。

　　“随着论文数量增多、篇幅变长、内容变复杂，同行评议变得更加耗时，效果却更差了。”美国加州大学圣地亚哥分校的数学家Frederick Manners说。许多数学家希望，AI 形式化和Lean认证能极大地简化同行评议工作，因为这在数学领域尤其令人感到痛苦。（徐锐）