Claudeが11日間の自律稼働でフェルマーの最終定理を機械検証。AI長時間タスクの限界が変わる
Anthropicは2026年9月4日、Claudeが11日間の自律稼働で、フェルマーの最終定理の初のコンピュータ検証済み完全証明を作成したと発表した。1995年にAndrew Wilesが証明を達成し350年以上の懸案に決着したこの数学難問を、今度はAIが初めて機械検証することに成功した。
発表の概要
「AIに任せられるのは短時間の単純作業だけ」。この認識を根底から問い直す成果が公開された。
Claudeは複数エージェントが並列協働する「Prove2Me」プラットフォーム上で11日間稼働し、1,300万行のLeanコードを生成。2万9,500個の中間定理を含む計3万300件の定理を証明し、Leanの標準3公理だけで最終証明の検証を完了した。消費した出力トークンは約60億。単独エージェントによる自律試行は失敗したが、DAGで定理の依存関係を追跡しメモリ劣化を防ぐアーキテクチャが突破口となった。
中小企業が注目すべきは「構造」だ。複数エージェント協働でAIの長期稼働時のコンテキスト劣化を克服した手法は、業務調査・法令解釈・文書作成など長時間を要する複雑な業務へのAI投入を現実に近づける。
“If the automatic formalization of FLT is possible now, then we have taken a big step towards automatic formalization of the modern mathematical literature.”
（筆者意訳：FLTの自動形式化が今や可能なら、現代の数学論文全体の自動形式化に向けた大きな一歩を踏み出したことになる）
── Kevin Buzzard氏（ロンドン大学インペリアル・カレッジ、数学者）、Anthropic研究発表より
出典: Anthropic「Formalizing Fermat’s Last Theorem」（2026年9月4日）
