Anthropic、Lean 4でフェルマーの最終定理の完全な機械検証証明を公開

Fermat's Last Theorem in Lean 4

Anthropicは、定理証明支援系Lean 4とMathlibを用いて、フェルマーの最終定理の完全な機械検証証明を完成させ、GitHubで公開しました。証明はFrey、Serre、Ribet、Wiles、Taylor-Wilesの手法に基づき、約60,475モジュール、100万以上の宣言から構成されます。Leanカーネルによる検証に加え、Rust製の独立したカーネルnanodaでも検証され、Leanの標準的な3つの公理のみに依存していることが確認されています。ソースコードはAIエージェントによって生成され、Leanが正しさを保証しています。