费马大定理是过去半个世纪最负盛名的数学成果之一。日前，美国人工智能（AI）公司Anthropic宣布，基于其开发的AI聊天机器人Claude 的进阶版模型，该定理首次被转化为计算机可验证的代码。
该模型仅用11天便完成了一个人类预计需要10年才能完成的项目。这一结果表明，AI 将在核验数学家的工作以及产生新的数学推理方面发挥越来越重要的作用。
美国罗格斯大学的数论学家Alex Kontorovich表示，AI 能够将人类数学家的工作转化为长达1300万行、无懈可击的证明，这一事实“令我大为震撼”。
加拿大多伦多大学的数论学家Daniel Litt表示：“如果它能形式化费马大定理，那么它大概能形式化任何东西。”
1637年，法国数学家Pierre de Fermat提出，当整数n>2时，关于x、y、z的方程x? + y? = z?不存在正整数解。这就是费马大定理，但Fermat只提出了这一论断，并未给出证明。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天内就完成了。但据Anthropic称，与MathLib不同，Claude生成的代码包含29500个“中间定理”，因此不能立即被数学家使用。Buzzard表示，将其中一部分整合到MathLib中是可能的，但需要工作量巨大。因此，如果AI能够核验任何数学证明，数学界可能面临一个“噩梦般的场景”，即出现多个不兼容的Lean库。
不过，对于Claude的工作，Buzzard依然表示欢迎。“以前，我有99.9%的把握认为该证明是正确的，在Claude的工作后，我现在是100%确信。”
Buzzard指出，按照当前的发展速度，AI或许不久就能审视整个数学知识库，甚至可能发现某些著名结论是错误的。两年前，这还是个幻想。
“随着论文数量增多、篇幅变长、内容更复杂，同行评议变得更加耗时，效果也变差了。”美国加州大学圣地亚哥分校的数学家Frederick Manners说。许多数学家希望，AI 形式化和Lean认证能极大地简化同行评议工作，因为这一工作在数学领域尤其令人感到痛苦。
0
评论 (0)