11日間・1300万行：ClaudeがFermatの最終定理の初のコンピュータ検証可能な証明を完成——しかし「自律」という言葉は精査が必要

2026年9月4日、Anthropicは公式ブログにて、同社の内部研究モデルが11日間でFermatの最終定理（Fermat's Last Theorem、略称FLT）の完全なLean形式化証明を書き上げたと発表した。内容は1300万行のコード、3万300件の中間定理（うち2万9500件が最終証明に採用）、約60億の出力トークンに上る。これは史上初めてコンピュータが完全に検証したFermatの最終定理の証明である。Anthropicの公式ブログはこれを「史上最大規模のLean証明ファイル」と称し、そのサイズは数学証明ライブラリMathlibの5倍を超えるという。

この件を詳しく分解する前に、しばしば混同されがちな概念を整理しておく必要がある。今回起きたのは「AIが新たな数学を発見した」のではなく、「AIが既存の人間の証明を、機械が一歩一歩検証できる形式言語へと変換した」ということだ。1995年、英国の数学者Andrew Wilesが129ページの論文でFermatの最終定理を証明した。それこそが350年来の難問を真の意味で解いた数学的発見である。Claudeが行ったのは形式化（formalization）——Wilesの証明に含まれる代数的整数論・算術幾何・Galois表現論といった複雑な推論の連鎖を、証明支援系Leanが自動的に正しさを検査できるコードへと翻訳すること——である。大雑把な比喩を使えば、新しい小説を書いたのではなく、すでに存在する小説を別の言語に一字一句翻訳し、新たな言語においても各文の論理が成り立つことを確認した、ということだ。

技術的仕組み：1つのエージェントが11日間動き続けたわけではない

Anthropicが使用したプラットフォームはProve2Me——有向非巡回グラフ（DAG）で定理間の依存関係を追跡するオープンソースの協調形式化プラットフォームだ。この構造により、数十のClaudeエージェントが並列で作業できる。ある部分証明が定理AとBを必要とする場合、それぞれ別のエージェントに割り当てて同時に進めることができ、互いにブロックし合わない。Anthropicによれば、今回のタスクでは「数十の」Claudeエージェントが同時並行で協働し、累計で約60億の出力トークンを消費した。

「11日間」とは実経過時間（wall-clock time）を指し、単一のエージェントが順番に11日間作業したわけではない。この違いが意味することは二つある。一つは、並列化によってタスクの難易度が大幅に分散されたこと。もう一つは、システム全体の調整能力——タスク分解・依存関係管理・部分証明の結合——こそが今回の成功の核心変数であり、単発の推論品質だけではない、ということだ。

タスクを実行したモデルはAnthropicによって「おおむねFable 5.1相当」の内部研究版と説明されており、具体的なパラメータ規模は公開されていない。コロンビア大学の研究員Tianyi Pengが全体を通じてごく少量の高水準な指示——例えば「Jacobian as a scheme sounds high priority」といった一言——を提供したほかは、残りはシステムが自律的に判断した。

Kevin Buzzardの二重の立場

帝国理工大学の数学者Kevin Buzzardの反応は特に注目に値する。彼はただの傍観者ではないからだ。2024年、BuzzardはFLTのLean化を人力で段階的に完成させようとする数学コミュニティの集団的形式化プロジェクトを立ち上げた人物であり、そのプロジェクトは数年を要すると見られていた。

AnthropicSubmitの証明を確認したBuzzardは公式に次のように述べた：

「この卓越した自動形式化の成果は、数学の公理以外に何ら仮定を置くことなくFermatの最終定理を証明している。代数・調和解析・幾何・数論の自動形式化を含み、AIによる自動形式化の産物はすでに十分に堅牢であり、後続の研究の基盤となり得る。この証明は多層的である。」

「自律」の境界はどこにあるか

Anthropicの発表にある「largely autonomously（大部分は自律的に）」という表現は、この報道の中で最も注意深く読む必要がある言葉だ。SiliconAngleなど複数のメディアによると、Claudeの最初の形式化の試みは失敗に終わり——成功にはサードパーティツールであるProve2Meの導入が必要だった。これは、いわゆる「自律」が特定のツールチェーンと既存の数学的資産というフレームワークの中での自律であり、白紙から始めた自律ではないことを示している。

これは成果そのものの価値を損なうものではないが、一つのことを示唆している。AIが「文書化された人間の知識体系」の中で長期タスクを実行する場合、その信頼性の表れ方は、オープンエンドな探索を行う場合とは大きく異なる。2万9500件の中間定理を正確に組み合わせられたのは、Lean言語自体の形式検証機構によるものだ——推論の各ステップをLeanのカーネルがリアルタイムに検査し、誤りは伝播しない。これは「ガードレール付きのマラソン」であり、際限のない自由な疾走ではない。

AI数学競争の現在地

この出来事を2026年のAI数学分野のより大きな文脈の中に置いてこそ、その位置づけが見えてくる。今年初め、OpenAIの内部モデルAstraが学界を80年にわたり悩ませてきたErdős単位距離問題の解決を含む数学的成果を発表した。Anthropicもまた、別の未公開モデルがRiemann予想において検証済みゼロ点の割合を41.6%からさらに前進させたと発表していた。この三つの方向——Erdős組合せ問題・Riemann予想・FLT形式化——は「新たな数学の発見」「既知の限界の前進」「既存の数学の検証」という三種類の異なるタスク類型に属し、技術的難易度も意義もまったく異なる。

FLT形式化は第三の類型に属する。工学的検証に最も近く、数学的創造から最も遠いが、長期・高精度・検証可能なタスクにおけるAIの実行能力を最も直接的に示すものでもある。現在、数学コミュニティにとっての重要な問いは次の通りだ。2万9500件の中間定理のうち、どれだけがMathlibに収録され、将来の研究で再利用可能なモジュールとなるのか。大部分が今回のタスクのための一時的な産物にすぎないとすれば、AIの産出物と人間の数学的蓄積をつなぐパイプラインはいまだ欠如している。

真のマイルストーンとは何か

この出来事の深層的な意義は、AIがFermatの最終定理を「証明した」こと（それは1995年にWilesが成し遂げた）にあるのではなく、AIが一種の新たな能力の組み合わせを示したことにある。すなわち、相互に依存する2万9500ステップの論理推論において、マルチエージェントの並列スケジューリング・DAG依存追跡・Leanカーネルによるリアルタイム検証の三者を連携させ、長期タスクにおける累積エラー率をゼロに抑えた、ということだ。

この能力の境界は注目に値し、同時に慎重に扱う必要がある。形式化タスクには、人間の自然言語タスクにはない重要な特性がある。各ステップに機械が判定できる正誤がある、ということだ。これは今回の成功の基盤であると同時に、その限界でもある。現実世界の大多数のタスクには、常に誤りを受け止めてくれるLeanカーネルのような検証機構が存在しない。同じマルチエージェントアーキテクチャをリアルタイム検証層のないタスクに適用した場合、2万9500ステップ無誤りという実績を再現できるかどうか、現時点で答えるための公開データはない。

Anthropicの今回の開放的な姿勢は評価に値する。証明コードはApache 2.0ライセンスのもとGitHubで公開されており、Leanカーネルとnanodaの独立カーネルによる検証もすでに完了し、サードパーティが自ら確認できる。これは珍しい「有言実行」——プレスリリースを発するだけでなく、生の成果物を公開して誰でも検査できるようにする姿勢だ。学術界による真の検証は、数学者たちがこの1300万行のコードを深く精査するにつれ、今後数ヵ月にわたって徐々に行われていくだろう。それまでの間、「AIは形式数学のマイルストーンの閾値を越えた」は根拠のある判断と言える。一方、「AIが人類の数学史上最も偉大な証明の一つを自律的に完成させた」というのは、注釈を添えて初めて成立する言い回しだ。