Claude完成费马大定理形式化证明
Checking that a major mathematical proof is correct can take years. Formalization—converting the mat...
Anthropic的Claude用AI完成了费马大定理的形式化证明，比专家预期时间短得多，还验证了2.9万多个相关定理。
Claude完成了费马大定理的首个形式化证明，这是数学史上最著名的定理之一。该证明包含超过1300万行代码，是迄今为止最大的Lean证明。Claude的证明验证了超过29,000个相关定理，涵盖多个以前未形式化的数学领域。费马大定理最初由安德鲁·怀尔斯在1995年证明，距离其提出已超过350年。
Checking that a major mathematical proof is correct can take years. Formalization—converting the mat...
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 💬 164 🔄 301 ❤️ 2736 👀 194208 📊 492 ⚡
