2026年9月4日、Anthropicの研究チームが**「Claudeがフェルマーの最終定理の完全な機械検証（形式化）証明を達成した」**と発表し、大きな話題となりました。
これは「AIが新しい数学的証明を発見した」わけではなく、**既存の数学的証明をコンピュータが確実に正しいと判定できる形に全行書き換えた（形式化した）**という成果です。
**プロジェクトの主要データ**
* **達成方法**: 定理証明支援系プログラミング言語 **Lean** による自動形式化
* **所要期間**: 11日間（Claudeのエージェント群によるほぼ完全な自律稼働）
* **証明コードの規模**: 約1,300万行（標準数学ライブラリMathlibの5倍以上）
* **構築・使用された定理**: 約30,300個の定理を証明し、うち29,500個を本編に使用
* **ベースとなった証明**: アンドリュー・ワイルズによる1995年の証明をもとに、ダルモン、ダイアモンド、テイラーらがまとめた簡略版
**技術的背景と意義**
* **人間との違い**: 人間が書く数学の証明論文には「自明であるため省略」とされる思考の飛躍が多数含まれますが、Leanのような検証系言語ではステップ一つひとつの厳密な論理構築（仮定から結論までのノーギャップな展開）が要求されます。
* **成果のポイント**: もともと数学者ケビン・バザード（Kevin Buzzard）らが率いるコミュニティ主導で数年がかりの計画として進められていたプロジェクトでした。AIエージェント同士のタスク管理・依存関係グラフ（DAG）化ツールなどを導入したことで、11日間で一気に走破されました。
* **数学界からの評価**: 「数学理論としての新しい発見はない」と冷静に受け止められつつも、「これまで人間が膨大な時間を費やしていた『証明の厳密な検証』をAIが代替できること」を実証した歴史的転換点として高く評価されています。
成果物および Lean コードは GitHub（anthropics/fermats-last-theorem）で公開されており、誰でも手元の環境で検証プログラムを再現・実行可能です。