クロード、フェルマーの最終定理を11日間で形式化

Anthropicは2026年9月5日、クロードがフェルマーの最終定理の初の完全形式化・機械検証済みLean 4証明を完了したと発表した。クロードはほぼ自律的に11日間で証明を生成し、Lean形式化は1300万行のコードに及び、29,500件の中間定理を証明した。インペリアル・カレッジのケビン・バザード氏はこれを「驚異的な自動形式化の成果」と評し、現代数学の自動形式化への道筋を示すものだと述べた。

クロードは11日間にわたりほぼ自律的に作業し、フェルマーの最終定理のコンピューター検証済み証明を生成した。形式化は1300万行のLeanコードに及び、29,500件の中間定理を証明しており、主要な数学的証明ライブラリであるMathlibの5倍以上の規模である。

Prove2MeとClaude Codeベースのマルチエージェント・ハーネスを用いて、エージェントのチームは2週間弱で証明を完了し、Claude Fable 5.1にほぼ相当する汎用の社内研究モデルから約60億トークンの出力を消費した。この実行は、Anthropicの研究者であるTianyi Peng氏とコロンビア大学グループの協力者らが構築したオープンな協働プラットフォームProve2Meに依存していた。Prove2Meは定理ステートメントの有向非巡回グラフを管理し、数十のClaudeエージェントが並行して次にどの部分証明を試みるかを決定するために使用した。

1637年にピエール・ド・フェルマーによって最初に提唱されたフェルマーの最終定理は、1995年にアンドリュー・ワイルズが画期的な解決策を発表するまで証明されないままであった。何年もかかると予想された仕事が11日間で完了した。完全な証明は、Rustで書かれた独立した証明カーネルであるnanodaによって独立に検証され、1,052,234件の宣言すべてが正しいことが確認された。

ケビン・バザード氏はより広い意味合いを強調した。「FLTの自動形式化が今可能ならば、我々は現代数学文献の自動形式化に向けて大きな一歩を踏み出したことになります。そのような自動形式化技術は新たなツールをもたらし、現在の数学コーパスにおける誤りを根絶し、査読者の負担を軽減するでしょう。」