Anthropic AI 在11天内证明了费马大定理
费马大定理——过去半个世纪最负盛名的数学成果之一——首次被转化为计算机可验证的代码，所用工具是先进的人工智能（AI）聊天机器人Claude的原型。
一台机器能够将人类数学家的工作转化为长达1300万行、无懈可击的证明，这“彻底震撼了我”，新泽西州皮斯卡塔韦市罗格斯大学的数论学家Alex Kontorovich表示。Claude的制造者、位于加利福尼亚州旧金山的Anthropic AI公司于9月4日宣布了这一突破。该模型在11天内完成了一个原本预计需要人类花费10年时间完成的项目。
这一结果表明，AI将在验证数学家工作以及产生新的数学推理方面扮演越来越重要的角色。按照目前的发展速度，AI不久便能审查整个数学知识库，甚至可能发现某些著名结果是错误的，这并 非不可想象。“两年前，这还是个幻想，”伦敦帝国理工学院的数学家Kevin Buzzard表示。
数学家们对AI数学能力飞速提升的速度越来越感到惊讶。这其中就包括该技术“形式化”证明的能力——即将数学论证从自然语言翻译成正式的、计算机可验证的代码，通常使用编程语言Lean。
今年2月，AI在AI辅助“形式化”领域实现了另一个里程碑，它验证了Maryna Viazovska关于（8维或24维空间中）最有效球体堆积方式的菲尔兹奖获奖成果。但Buzzard表示，费马大定理的工作在复杂性上完全是另一个量级。“难度大约高出了一个数量级，”他说。
加拿大多伦多大学的数论学家Daniel Litt对此表示赞同。“如果他们能形式化费马大定理，那他们大概能形式化任何东西。”
费马大定理的原始证明由安德鲁·怀尔斯和理查德·泰勒于1994年完成，是20世纪数学的里程碑式成果。其陈述看似简单：不存在任何整数x、y、z，使得当n大于2时，有xⁿ + yⁿ = zⁿ。法国数学家皮埃尔·德·费马于1637年提出了这一论断，但没有留下证明，它因此被称为“他的”最后定理——尽管在数学中，一个命题只有在被严格证明为真之后，才能获得“定理”的称号。
（解决这个特定方程——或者说知道它无解——本身并没有太多实际用途，但怀尔斯为解决该问题所发展的技术帮助将数学的不同分支联系了起来。该证明为怀尔斯赢得了2016年的阿贝尔奖，这是数学界最负盛名的奖项之一。）#人工智能 #商业 #科技 #美国 #大模型 #AI #数学