Anthropicは、内部モデルがprove2.meプラットフォームを使用し、フェルマーの最終定理の完全な証明をLeanを用いて形式化したと発表しました。

この成果により、Freek Wiedijk氏が提示していた「形式化すべき100の課題」リストの最後の定理が完了し、20年にわたるベンチマークが終了することになります。

形式化された証明は、1995年のDarmon-Diamond-Taylorによる記述に基づいています。数学的な議論の内容自体は既存の文献を忠実に追ったものですが、自動形式化の可能性を示す重要な進展となりました。

このコードベースは1,340万行を超える膨大な規模です。96コアの環境において、Leanの数学ライブラリの約20倍のコンパイル時間を要すると報告されています。

出典: Fermat's Last Theorem: Anthropic has beaten me to it（Hacker News Frontpage、2026-09-05）