Claude Fable 5.2、1000体のエージェントが「フェルマーの最終定理」を30時間で形式化

1000体のAIが自らタスクを分解し進行、従来の11日間から28.7時間へと大幅短縮

　米アンソロピックは2026年11月9日、初期版のClaude Fable 5.2をベースとする1000体のAIエージェントを用いて、フェルマーの最終定理の証明を約30時間で形式化したことを明らかにした。実際の所要時間は28.7時間である。形式化とは、人間が記述した数学の論証を、コンピュータのプログラムである証明支援系言語Leanが論理的誤りの有無を機械的に検査できるコードへと翻訳・再構築する作業を指す。

　フェルマーの最終定理は、3以上の整数nについてa?＋b?＝c?を満たす正の整数a、b、cが存在しないというものであり、1995年にアンドリュー・ワイルズらによって証明された。今回の実験では、エージェント群に対して60の目標命題と、既存の47の補題を与えた上で作業が開始された。

　最大の特徴は、AIが自律的に組織化を行った点にある。システムは1体のリードエージェントと999体のヘルパーエージェントで構成された。標準的なリレーショナルデータベースであるPostgreSQLとバージョン管理システムGitを中心とする汎用的な環境で、情報の共有や作業の分担が図られた。リード役は開始直後に全体指示や担当割り当てなどを管理する5つの共有テーブルを作成し、ヘルパー役がタスクを引き受け、進捗を記録する仕組みを自ら構築した。

　このアプローチは、アンソロピックが同年9月に公表した形式化の成果と比較して劇的な効率化を達成している。前回は数十体のエージェントと人間の研究者の指示、および証明管理専用のプラットフォームProve2Meを利用し、約11日間を要した。生成されたコードは約1300万行に及んだ。一方、研究者による追加の指導を行わなかった今回の実験では、専用プラットフォームを使用せずに実行時間を約89％削減し、出力された証明の長さも前回の約7分の1へと大幅に圧縮された。消費された出力トークンも約60億から約20億へと減少している。

　同社によれば、同じ1000エージェントの環境下で従来のClaude Opus 5.5を用いた場合、18時間経過時点で全体の26％しか形式化が進まず、その後30時間までほとんど進展が見られなかった。Fable 5.2の推論能力とタスク管理能力の高さが際立つ結果となった。

　汎用ツールのみで1000体ものAIが協調し、難解な数学的証明を完遂した事実は、システム開発や研究のあり方をどう変えるのか。そして、多数の自律AIを安全に制御するための背後にあるセキュリティ技術とはどのようなものか。次ページでその詳細と今後のビジネスへの波及効果を紐解く。