記事一覧へ
重要な数学の証明が正しいかどうかを確かめるには、何年もかかることがあります。形式化、つまり数学的な推論を、Lean のようなコンピュータ上の証明支援系が検証できる形に変換することが、その助けになります。
先月、Claude は、史上最も有名な定理のひとつであるフェルマーの最終定理について、初の形式化された証明を完成させました。専門家が何年もかかると考えていたプロジェクトでした。これは、これまでに書かれた中で最大の Lean の証明です。
フェルマーの最終定理は、予想から 350 年以上を経た 1995 年に、アンドリュー・ワイルズ卿によって初めて証明されました。私たちの証明は合計 1,300 万行を超えるコードで、機械による検証を提供します。さらに重要なのは、この証明が必要とする 2 万 9,000 を超えるほかの定理も証明していることです。これらは、それまで形式化されたことのなかった数学の多くの分野にまたがっています。
私たちはこれを、数学的知識の中核を固めていく長いプロセスにおける大きな一歩だと考えています。3 世紀にわたる数学者たちの仕事と、Lean と Mathlib への数百人の貢献者の仕事の上に成り立っています。これまで以上に多くの証明が生み出されている時代にあって、AI による数学の証明の検証が、数学の査読の負担を減らす助けになると、私たちは期待しています。
そのプロセスについては、Science Blog でお読みいただけます: https://www.anthropic.com/research/formalizing-fermats-last-theorem
証明の全体は GitHub でご覧いただけます: https://github.com/anthropics/fermats-last-theorem
Claude数学研究ai-thinking
Claude がフェルマーの最終定理の形式化証明を完成、Lean 史上最大規模
出典: Anthropic（@AnthropicAI）さんの X の投稿を、日本語に翻訳して紹介しています。 原文はこちら ↗
14,0931,8743,8424,768,218
原文を表示 / Show original
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: https://www.anthropic.com/research/formalizing-fermats-last-theorem
And see the complete proof on GitHub: https://github.com/anthropics/fermats-last-theorem