Anthropicは2026年9月4日、Claudeが約11日間ほぼ自律的に動き、フェルマーの最終定理（FLT）の初の、端から端まで機械検証可能な証明をLeanで完成させたと発表した。最終証明には約2万9500個の中間定理を用い、証明過程では約3万300個を機械検証可能な形で示した。Leanコードは約1300万行で、主要な数学ライブラリMathlibの5倍超に達する。
FLTの人間向け証明は1995年のWilesらによる129ページで、検証だけでも数か月を要した。形式化は自明な段も省略できず、Imperial College Londonの共同プロジェクトでは初期計画だけで86ページ、完了まで数年が見込まれていた。初期の複数エージェントは進捗を見失い失敗したが、定理依存をDAGで管理する協調基盤Prove2Meに切り替えたことで完走した。消費した出力トークンは約60億、使った内部研究モデルはClaude Fable 5.1とおおむね同水準だという。
完成証明はLeanの標準公理3つのみに依拠し、未証明箇所を通すsorryは含まない。MathlibのFLT命題との一致も比較ツールで確認され、GitHubで公開されている。AIが大量の証明を出すほど人間の査読は追いつかなくなるため、論文と並ぶ形式化成果物が標準になる、と同社とKevin Buzzard氏は見ている。エンジニア視点では、長時間エージェントを「次に何を証明・実装すべきか」見える化する基盤と、機械検証可能な成果物の両方を設計しないと、大規模自動作業は破綻しやすい。