Anthropic AI 用 Claude 在 11 天内“形式化”费马大定理证明

英文标题：🔶 Anthropic AI 'formalizes' proof of Fermat's last theorem in just 11 days

Anthropic AI 宣布，其高级原型 AI 聊天机器人 Claude 首次将费马大定理转化为可由计算机验证的形式化代码。该项目生成了一份长达 1300 万行的严格证明，仅用 11 天完成，而人类此前预计需要 10 年。数学家认为，这一成果的复杂度显著高于此前 AI 对高维球体最密堆积问题证明的形式化工作。该进展表明，AI 未来可能在验证数学研究、辅助产生新推理，乃至系统审查既有数学知识方面发挥更大作用。

打开原文相关 2 · 机会 0

中文

安德鲁·约翰·怀尔斯于 1998 年在普林斯顿大学办公室里，与写在黑板上的费马大定理合影。

数学家安德鲁·怀尔斯于 1994 年完成了费马大定理的证明，距离皮埃尔·费马提出这一猜想已过去 350 多年。图片来源：AP Photo/Charles Rex Arbogast/Alamy

费马大定理是过去半个世纪中最受瞩目的数学成果之一。如今，借助人工智能（AI）聊天机器人 Claude 的高级原型版本，它首次被转化为可由计算机验证的代码。

AI 攻克已有 80 年历史的数学难题——研究人员感到震惊

美国新泽西州皮斯卡塔韦市罗格斯大学数论学家 Alex Kontorovich 表示，一台机器能将人类数学家的工作转变为一份长达 1300 万行、无懈可击的证明，这“完全颠覆了我的认知”。总部位于美国加利福尼亚州旧金山的 Claude 开发商 Anthropic AI 于 9 月 4 日宣布这一突破。该模型在 11 天内完成了这一项目，而此前预计人类需要 10 年才能完成。

这一结果表明，AI 将在核查数学家工作以及产出新的数学推理方面发挥日益重要的作用。按照当前的进展速度，AI 或许很快便能审阅全部数学知识库，甚至可能发现一些知名结论其实是错误的。伦敦帝国理工学院数学家 Kevin Buzzard 表示：“两年前，这还是一种幻想。”

数学家感到震撼

数学家们越来越惊讶于 AI 数学能力飙升的速度。这其中包括该技术“形式化”证明的能力——即将以自然语言表达的数学论证，转换为通常采用 Lean 编程语言编写、可由计算机认证的形式化代码。

今年 2 月，AI 辅助“形式化”取得了另一项里程碑：它认证了 Maryna Viazovska 关于在 8 维或 24 维空间中最有效球体堆积方式的菲尔兹奖获奖工作。Maryna Viazovska的成果获得了认证。但 Buzzard 表示，费马大定理的工作在复杂度上完全是另一个级别。“它可能要难一个数量级，”他说。

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

“这令人难以置信”：AI 如何改变数学

费马大定理最初的证明由 Andrew Wiles 和 Richard Taylor 于 1994 年完成，是 20 世纪数学的一项里程碑式成果。其表述看似简单：当 n 大于 2 时，不存在任何整数 x、y 和 z，使得 x n + y n = z n。法国数学家皮埃尔·德·费马于 1637 年提出这一断言，却没有留下证明；它因此被称为“他的”最后定理——尽管在数学中，一项陈述只有在被严格证明为真后，才能获得“定理”的称号。

（单独来看，求解这一特定方程——或知道它不存在解——并没有太多实际用途；但怀尔斯为攻克该问题而发展出的技术，帮助连接了相距甚远的数学学科。这项证明还让怀尔斯获得了阿贝尔奖。阿贝尔奖是数学界最受推崇的奖项之一，他于 2016 年获奖。）

English / 原文

Andrew John Wiles poses next to Fermat's Last Theorem, written on a chalkboard in his Princeton university office in 1998.

Mathematician Andrew Wiles completed the proof to Fermat’s last theorem in 1994, more than 350 years after Pierre Fermat proposed the conjecture.Credit: AP Photo/Charles Rex Arbogast/Alamy

Fermat’s last theorem, one of the most celebrated mathematical results of the last half-century, has been turned into computer-verified code for the first time, using an advanced prototype of the artificial-intelligence (AI) chatbot Claude.

AI cracks 80-year-old mathematics challenge — researchers are astonished

The fact that a machine could turn the work of human mathematicians into a 13-million-line-long, ironclad proof “just completely blew my mind”, says Alex Kontorovich, a number theorist at Rutgers University in Piscataway, New Jersey. Claude-maker Anthropic AI, of San Francisco, California, announced the breakthrough on 4 September. The model finished in 11 days a project that was expected to take humans 10 years.

The result shows that AI will play an increasingly important part in checking the work of mathematicians — as well as in producing new mathematical reasoning. At the current pace of progress, it is not unthinkable that AI could soon be able to scrutinize the entire library of mathematical knowledge, perhaps finding that some well-known results are wrong. “Two years ago, that was a fantasy,” says Kevin Buzzard, a mathematician at Imperial College London.

Mathematicians astounded

Mathematicians have been increasingly astounded by the pace at which AI’s mathematical skill have soared. This includes the technology’s ability to ‘formalize’ proofs — translating mathematical arguments from natural language into a formal, computer-certifiable code, typically in the programming language Lean.

In February, AI achieved another milestone in AI-aided ‘formalization’, when it certified the Fields-medal-winning work on the most efficient ways to pack spheres (in a space of 8 or 24 dimensions) of Maryna Viazovska. But Buzzard says that the Fermat’s last theorem work was on a whole other level of complexity. “It was maybe an order of magnitude more difficult,” he says.

Daniel Litt, a number theorist at the University of Toronto, Canada, agrees. “If they can formalize Fermat's last theorem, they can probably formalize anything.”

‘It is incredible’: How AI is transforming mathematics

The original proof of Fermat’s last theorem, completed in 1994 by Andrew Wiles and Richard Taylor, was a landmark result of twentieth-century mathematics. The deceptively simple statement is that there cannot be any whole numbers x , y and z such that x n + y n = z n , if n is greater than 2. French mathematician Pierre de Fermat had made this claim in 1637 but did not leave behind a proof, and it became known as ‘his’ last theorem — even though in mathematics, a statement earns the ‘theorem’ badge only after it has been rigorously proven to be true.

(By itself, solving this particular equation — or knowing that it has no solutions — does not have much practical use, but the techniques Wiles developed to crack the problem helped to bring distant disciplines of mathematics together. The proof earned Wiles an Abel Prize, one of the most coveted awards in mathematics, in 2016.)