米Anthropicは、同社のAIモデル「Claude」を用いた自律型マルチエージェントシステムにより、現代数学の最大の金字塔とされる「フェルマーの最終定理」について、定理証明支援系言語「Lean」を用いた完全な形式的検証（Formalization）に世界で初めて成功したと発表しました。
フェルマーの最終定理は1995年にアンドリュー・ワイルズ氏によって数学的に証明されましたが、その長大かつ難解な証明構造ゆえに、コンピュータによる厳密な一行ごとの形式的検証の完了にはコミュニティ全体で数十年を要すると見込まれていました。
今回のプロジェクトでは、コロンビア大学の研究グループが開発したエージェント連携基盤「Prove2Me」を採用し、Claudeが複数のサブエージェントに分かれて定理の依存関係を自律的に分担・解決。
わずか11日間の連続自律推論により、1,300万行を超えるLeanコードと約29,500個の中間定理を自動構築し、完全なエラーフリー証明を樹立しました。
本成果はFreek Wiedijk氏が提唱した「形式化すべき100の数学定理リスト」の最後の難問を完結させるものであり、AIが高度な学術研究において人間の頭脳を補完・加速する決定的な証拠となりました（一次ソース：Anthropic Research 公式発表 / GitHub リポジトリ）。