ClaudeがFermatの最終定理を11日で形式証明
मूल शीर्षक: Formalizing Fermat's Last Theorem
यह क्यों महत्वपूर्ण है
AIが複雑な数学証明を自律的に形式化できることが示され、数学研究の検証プロセスを根本的に変える可能性がある。
Anthropicは2026年9月4日、AIアシスタントClaudeがFermatの最終定理（FLT）の完全なコンピュータ検証済み証明を11日間で作成したと発表した。Claudeはほぼ自律的に動作し、Lean言語で1,300万行のコードと29,500の中間定理を証明した。
Anthropicは、ClaudeがFermatの最終定理（FLT）の初の完全なコンピュータ検証済み証明を作成したと発表した。FLTとは、1637年頃にPierre de Fermatが「nが2より大きい場合、aⁿ + bⁿ = cⁿを満たす正の整数a、b、cは存在しない」と主張した定理である。
最初の正式な証明はSir Andrew Wilesが1995年に発表し、129ページに及ぶもので、検証に数ヶ月を要した。その後、オランダのコンピュータ科学者Jan Bergstraがこの証明の「形式化」（コンピュータが自動検証できる形式への変換）を提案。2024年にはImperial College LondonのKevin BuzzardがLean proof assistantを使った形式化プロジェクトを開始した。
Anthropicの研究者Tianyi Peng（Columbia大学でAI形式化ツールを開発）がClaudeでFLTの形式化を試みたところ、予想を超える結果が得られた。Claudeは11日間でほぼ自律的に動作し、Lean言語で1,300万行のコードを記述、29,500の中間定理を証明して、数学の公理のみを前提とする完全な証明を完成させた。
Kevin Buzzardはこの成果について「代数、調和解析、幾何学、数論の自動形式化を含む並外れた成果であり、AIによる形式化の成果物が十分に堅牢で積み重ねが可能なことを示している」とコメントした。
Anthropicは、AIが証明を生成する機会が増える中、形式化による検証の容易化が数学的知識への信頼を高めると述べている。