费马大定理首获计算机可验证的形式化证明

Anthropic研究人员利用Claude AI在11天内完成了费马大定理的首个完整计算机可验证的形式化证明1。这一突破性成就标志着人工智能在自动形式化复杂数学证明方面迈出重要一步。Claude采用Lean编程语言独立工作，生成了1300万行代码并证明了29500个中间定理，总共产生了30300个定理证明1。这一成就规模空前，Claude的证明是迄今为止最大的Lean证明，超过Mathlib主要数学证明库规模的5倍1。

相比之下，英国数学家Andrew Wiles在1995年发表的原始证明仅为129页，但耗时数月才能完成验证1。费马在1637年提出的这一定理曾在350多年间吸引了无数数学家的关注，1908年甚至被悬赏100000德国金马克1。研究人员通过Prove2Me平台和Claude多代理系统实现了这一形式化目标，该过程消耗了约60亿个输出令牌1。数学家Kevin Buzzard对这项成就评价称："这一非凡的自动形式化成就证明了费马大定理，只依赖数学公理"1。研究团队还用三个个人Claude Max订阅在仅三天内完成了Vinogradov三素数定理的形式化1。

Researchers at Anthropic have achieved a major milestone in automated mathematics by using Claude AI to produce the first fully computer-verifiable formal proof of Fermat's Last Theorem in just 11 days 1. The AI system independently wrote the proof in the Lean programming language, generating a codebase of 13 million lines that formally verified 29,500 intermediate theorems, with a total of 30,300 theorem proofs 1. This accomplishment far exceeds the time originally anticipated for such a task and showcases Claude's capability to automate the formalization of intricate mathematical proofs at an unprecedented scale.

The resulting proof represents the largest Lean formalization ever created, surpassing the size of Mathlib, the primary library of major mathematical proofs, by more than five times 1. In contrast, Andrew Wiles' original proof of the theorem, published in 1995, comprised 129 pages and required months to verify 1. The project relied on the Prove2Me platform and Claude's multi-agent system architecture, consuming approximately 6 billion output tokens throughout the process 1. Kevin Buzzard commented on the achievement, stating that it was "an extraordinary feat of automated formalization that proves Fermat's Last Theorem based solely on mathematical axioms" 1.

The broader significance of this breakthrough extends beyond Fermat's Last Theorem itself. Anthropic researchers demonstrated comparable efficiency by formalizing the Vinogradov three-prime theorem using just three personal Claude Max subscriptions within three days 1. These developments suggest that AI-assisted formal verification could substantially accelerate the pace at which mathematical research advances and undergoes validation, potentially transforming how mathematicians approach proof formalization in the future.