大模型
x.com ·
@AnthropicAI
Claude完成费马大定理首次形式化证明，为Lean最大证明
Anthropic宣布Claude完成费马大定理的首次形式化证明，这是Lean证明助手中最大的证明，包含超过1300万行代码，并证明了29000多个相关定理。该成果标志着AI辅助数学证明的重要进展。
AI推荐理由 Anthropic官方宣布Claude完成费马大定理的首次形式化证明，这是Lean证明助手中最大的证明，包含1300万行代码和29000个定理，具有里程碑意义。信息具体、来源权威，对AI在数学推理领域的应用价值极高。
95
正文
验证一个重大数学证明是否正确可能需要数年时间。形式化——将数学推理转换为Lean等计算机证明助手可以验证的形式——可以提供帮助。
上个月，Claude完成了费马大定理的第一个形式化证明，这是有史以来最著名的定理之一。这是一个专家认为需要很多年的项目。这是有史以来最大的Lean证明。
费马大定理于1995年由安德鲁·怀尔斯爵士首次证明，距离其被猜想已超过350年。我们的证明总计超过1300万行代码，提供了机器验证。更重要的是，它证明了该证明所需的超过29,000个其他定理，涵盖了许多此前从未被形式化的数学领域。
我们认为这是巩固数学知识核心的漫长过程中的一大步，建立在三个世纪数学家的工作和数百名Lean和Mathlib贡献者的基础上。我们乐观地认为，人工智能辅助的数学证明验证将有助于减轻数学审稿的负担，在一个比以往产生更多证明的时代。
您可以在我们的科学博客上阅读有关过程的信息：
anthropic.com/research/forma…
并在GitHub上查看完整证明：
github.com/anthropics/fer…
您的浏览器不支持视频标签。
🔗 在Twitter上查看
查看原文（中文正文为 AI 翻译）
Checking that a major mathematical proof is correct can take years. Formalization—converting the mathematical reasoning into a form computer proof assistants like Lean can verify—can help.
Last month, Claude completed the first formalized proof of Fermat’s Last Theorem, one of the most famous theorems of all time. This was a project experts thought would take many years. It is the largest Lean proof ever written.
Fermat’s Last Theorem was first proven in 1995 by Sir Andrew Wiles, more than 350 years after it was conjectured. Our proof, which totals over 13 million lines of code, provides machine verification. More importantly, it proves over 29,000 other theorems that the proof requires, across many areas of math which had never before been formalized.
We see this as a major step in the long process of firming up the core of mathematical knowledge, building on work from three centuries of mathematicians and hundreds of contributors to Lean and Mathlib. We are optimistic that AI-assisted verification of mathematical proofs will help reduce the burden of refereeing mathematics in an era where more proofs are being produced than ever before.
You can read about the process on our Science Blog:
anthropic.com/research/forma…
And see the complete proof on GitHub:
github.com/anthropics/fer…
Your browser does not support the video tag.
🔗 View on Twitter