ClaudeがFermatの最終定理を形式証明
原題: Formalizing Fermat's Last Theorem
なぜ重要か
AIによる数学証明の自動形式化が実用段階に入ったことを示し、研究数学の検証コスト削減と信頼性向上に向けた新たな基盤を提供する。
Anthropicは2026年9月4日、AIアシスタントClaudeが11日間でFermatの最終定理（FLT）の完全なコンピューター検証済み証明を生成したと発表した。ClaudeはLean言語で1,300万行のコードを記述し、29,500の中間定理を証明。人類が350年以上解けなかった数学の難問を、AIがほぼ自律的に形式化した。
Anthropicは、AIアシスタントClaudeが世界初の完全なコンピューター検証済みFermatの最終定理（FLT）証明を生成したと発表した。
FLTは1637年頃、Pierre de Fermatが「n＞2の場合、aⁿ＋bⁿ＝cⁿを満たす正の整数a、b、cは存在しない」と書き残した命題。1995年にSir Andrew Wilesが129ページに及ぶ証明を発表するまで、350年以上にわたって未解決だった。1908年には10万ドイツ金マルク（現在価値で100〜200万ドル相当）の懸賞金が設けられ、最初の1年だけで621件の誤った証明が提出されるほど注目を集めた。
Wilesの証明を発表後、これを計算機が自動検証可能な形式に変換する「形式化」の試みが始まった。2024年にはImperial College LondonのKevin BuzzardがLean証明支援系を用いた多年にわたるコミュニティプロジェクトを立ち上げていた。
今回、AnthropicのResearcherでColumbia大学グループに所属するTianyi Pengが、ClaudeによるFLT形式化の可能性を検証したところ、予想を大幅に上回る結果が得られた。Claudeは11日間でほぼ自律的に作業を進め、Lean言語で1,300万行のコードを記述、29,500の中間定理を証明する形で、エンドツーエンドの形式証明を完成させた。
この成果についてKevin Buzzardは「数学の公理以外を一切仮定せずFLTを証明した卓越した自動形式化の達成」と評価し、「AIの自動形式化の成果物が積み重ねられるほど堅牢になっていることが示された」とコメントした。
Anthropicは、AIが証明を生産するにつれて形式化が容易になれば、新たな数学的成果の検証にかかる数年単位の負担を軽減できると説明。数学の知識体系への信頼を維持する上で重要な前進と位置付けている。なお今回の成果は新たな数学的発見ではなく、既存のWiles証明をコンピューターが検証可能な形に変換・確認したものである点を強調している。