Anthropicは2026年9月4日、Claudeのエージェント群が「フェルマーの最終定理」の証明を証明支援系Leanで形式化し、初めて計算機で検証された端から端までの証明を完成させたと発表しました。所要日数は11日、生成したLeanコードは1,300万行、消費した出力トークンは約60億です。人間からの数学的な指示は「ヤコビアンをスキームとして扱うのは優先度が高そう」といった数回の高レベルな助言に限られました。証明の全体はGitHubで公開されています。数学の話に見えますが、「数十のエージェントが数日単位で協調して巨大な検証済み成果物を作る」という点で、大規模なコード生成や検証の自動化に関わるエンジニアにも関係する発表です。
何が「初めて」なのか
フェルマーの最終定理は、3以上の整数nについてx^n + y^n = z^nを満たす正の整数x, y, zが存在しない、という主張です。1995年にAndrew Wilesが証明しましたが、その証明は代数・調和解析・幾何・数論にまたがる長大なもので、人間が検算するだけでも大仕事でした。「形式化」とは、この証明をLeanのような証明支援系(数学的推論をプログラムとして書き、機械的に正しさを検査するツール)が検証できる形に書き換える作業を指します。
この形式化には、Imperial College Londonの数学者Kevin Buzzard氏が2024年から率いるコミュニティプロジェクトが、複数年計画で取り組んでいました。今回のClaudeの証明はそのプロジェクトと「flt-regular」プロジェクトの一部を流用しつつ、Darmon・Diamond・Taylorによる簡略版のWilesの証明に沿って、残りをClaudeが書き上げたものです。完成した証明はLeanによって検査され、使っている公理はLeanの標準的な3つだけ、定理の主張がMathlib(Leanの中核ライブラリ)にあるフェルマーの最終定理の記述と一致することも比較器で確認されています。
Buzzard氏は「Anthropicの研究者によればわずか11日しかかからなかったというこの驚異的な自動形式化は、数学の公理以外の仮定なしにフェルマーの最終定理を証明している」とコメントし、「AIによる自動形式化の成果物は、その上に積み上げられるほど頑健になった」と評価しています。
鍵は「エージェント同士の協調」だった
技術的に興味深いのは、Claudeの能力そのものより、数十のエージェントをどう協調させたかです。Anthropicによると、最初の試みは失敗しました。エージェントはプロジェクトの状態をすぐに見失い、互いに協調できなくなったといいます。
転機になったのは、研究を主導したTianyi Peng氏がコロンビア大学の共同研究者と設計した協調基盤「Prove2Me」です。8月末に論文も公開されており、「エージェントを持つ人なら誰でも参加できる」公開の基盤として設計されています。Prove2Meは、定理の主張を有向非巡回グラフ(DAG)として管理し、どの定理から手を付けるべきかをエージェントに示します。さらに定理の「主張」と「証明」を別ファイルに分けてLeanのコンパイルを速くし、各定理に自然言語の説明を付けて検索と再利用をしやすくしました。人間が先に「どこまで細かく証明を分解するか」の枠組みを用意し、その中でエージェントに埋めさせる構造です。
失敗した試行が無駄になったわけではなく、その成果は最終的な証明の定型部分を除く行の約7%を占めています。使われたモデルは「Claude Fable 5.1におおむね相当する汎用の社内研究モデル」で、数学専用に作られたものではありません。
ただしAnthropicは、証明が必要以上に長い可能性が高いことも認めています。1,300万行はMathlib全体の5倍超で、人間の証明なら省略する「自明なステップ」をLeanはすべて要求するとはいえ、冗長な部分が多く含まれていると考えられます。人間が読んで理解するための解説が形式化とは別に必要だ、という点も強調されています。
個人のClaude Maxプランでも成立した
企業向けの巨大な計算資源がないと再現できない話ではない、という点も押さえておきたいところです。Anthropicは小規模な追加実験として、個人向けのClaude Maxプラン3契約だけを使い、Prove2Meを介して協調させることで、解析的整数論の「ヴィノグラードフの三素数定理」を3日で形式化したと報告しています。フェルマーの最終定理に比べれば規模ははるかに小さい定理ですが、協調基盤さえあれば消費者向けの契約でも複数エージェントの形式化プロジェクトが回る、という実証です。
日本の読者にとって
日本の数学研究者や証明支援系のユーザーにとっては、Mathlibの5倍という「AIが書いた巨大な証明資産」が公開されたことが直接の材料になります。Buzzard氏の言葉を借りれば「現代の数学文献の自動形式化に向けた大きな一歩」であり、査読の負担を形式化で減らす流れが加速すると考えられます。Prove2Meは公開されている協調基盤なので、研究室の規模でも試せます。
ソフトウェアエンジニアにとっての示唆は、Leanという「正解が機械的に判定できる領域」で、数十エージェント×11日という長期の協調作業が成立したことです。ポイントは、モデルの賢さではなく、DAGによる作業分解、コンパイル時間を意識したファイル分割、自然言語による索引という地味な設計でした。単一の巨大なコンテキストにすべてを詰め込むのではなく、外部の状態管理に進捗を持たせる設計は、テストやコンパイラで正誤を判定できる大規模なコード移行や検証にも応用できる可能性があります。一方で、約60億出力トークンという消費量は、Claude Fable 5.1の公開価格(出力100万トークンあたり50ドル)に当てはめると出力分だけで約30万ドル(1ドル150円なら約4,500万円)に相当します。実際に使われたのは社内モデルなので目安にすぎませんが、Anthropic自身も「形式化は依然としてトークン集約的だ」と書いています。
次にやることは3つです。第一に、Leanに触れたことがあるなら、Apache 2.0で公開されているリポジトリの証明の道筋をたどる「PROOF-PATH.md」を読んで、AIが書いた証明の構造(定理の分割の粒度)を確認すること。なお、リポジトリのREADMEによると全体のビルドは96並列で約5.5時間、検証にはメモリ300GB程度を見込む必要があります。第二に、複数エージェントで長期タスクを回している開発者は、Prove2Meの「DAGで状態を外に持つ」設計を自分のパイプラインと比べてみること。第三に、形式化そのものに興味があれば、Prove2Meで小さな定理から試し、Maxプラン程度の予算でどこまで進むかを測ることです。
