クロード、11日でフェルマー最終定理の完全形式化証明を完了

9月4日、AnthropicはAIモデルClaudeが11日間でフェルマー最終定理の完全な形式化証明を達成したと発表した。同プロジェクトは清華大学姚班出身の彭天翼氏らが主導し、数十のClaudeエージェントが協調して進められた。約60億トークンを消費し、形式証明支援系Leanを用いて約1300万行のコードと約2万9500個の中間定理が生成された。 本成果の核心は、数学論文の省略した検証プロセスをコンピュータで自動化した点にある。Claudeは従来の証明経路を忠実に再現し、Frey楕円曲線やモジュラ性といった高度な数論を機械検証可能な形式に翻訳した。工程管理にはProve2Meプラットフォームが活用され、命題と証明を分離して依存関係を管理することでエージェントの並列処理を最適化した。 検証プロセスには多重の安全策が設けられた。Leanのコアチェックに加え、Rust製の独立検証器nanodaが105万回以上の宣言を再検証。最終命題が原本を忠実に反映しているか確認するcomparatorがMathlibと照合した。依存公理は基礎論理のみで、未完成箇所は存在しないことが確認された。 Anthropicは本プロジェクトがAIによる大規模数学形式化の実用性を示したと指摘する。一方で生成コードは既存のMathlibの5倍規模に及ぶなど冗長性が高く、人間が読用するための最適化には依然として工数が必要であると認めている。今後はコードの圧縮とモジュール化を進め、AI生成証明の信頼性と実用性を両立させることが課題となる。