フェルマーの最終定理の形式化

本記事は、Claude AIモデルが研究者らと協力して生成した、フェルマーの最終定理（FLT）の初の完全なコンピュータ検証証明を報じています。実験において、Claudeは主に11日間自律的に作業し、Lean証明アシスタントとProve2Me協力プラットフォームを用いて、同定理の証明を形式化しました。完成した証明はLeanコード1300万行で構成され、29,500個の中間定理を検証しています。この作業は、1995年のアンドリュー・ワイルズ卿の証明の簡略版に従っています。著者らは、Anthropic研究者のPeng Tianyiを中心に、定理自体は新しくないものの、この成果は形式数学の分野において重要であると強調しています。自動形式化は、複雑な証明の検証、数学文献の誤りの発見、人間のレビュワーの負担軽減に役立ち得ます。この証明をレビューしたインペリアル・カレッジ・ロンドンのKevin Buzzardは、現代数学文献の自動形式化への大きな一歩として称賛しています。記事は、このプロジェクトが数学的結果を厳密に検証し、数学的知識の信頼性を維持するためのAIの潜在能力を実証していると結論付けています。

(出典：Anthropic)