Claude がフェルマーの最終定理を11日で形式化、Lean 1,300万行の計算機検証済み証明を公開

要約

Anthropic は 2026-09-04、フェルマーの最終定理（FLT）の、初となる end-to-end で計算機検証済みの証明を公開しました。Claude が 11日間ほぼ自律的に稼働して、証明支援系 Lean のコードとして書き上げたものです。

数字が異様です。Lean のコードは 1,300万行、途中で証明した補助定理は 29,500件（生成したものを含めると 30,300件）。これは Lean のコミュニティ共有ライブラリ Mathlib 全体の 5倍を超える分量で、Lean 史上最大の証明とされます。消費した出力トークンは約60億、使われたのは Claude Fable 5.1 相当の社内研究モデルでした。

FLT は 1637 年に Fermat が本の余白に書き残した主張で、1995 年に Andrew Wiles が 129 ページの証明を発表するまで 350 年以上未解決でした。その Wiles の証明を「計算機が一行ずつ検証できる形」に書き直す作業（形式化）は数年かかると見られていました。実際、Imperial College London の Kevin Buzzard が 2024 年に立ち上げたコミュニティ主導の形式化プロジェクトは、初期フェーズの設計図だけで 86 ページあり、資金は 2029 年まで確保されています。

そのプロジェクトを率いる Buzzard 自身が Claude の証明をレビューし、「数学の公理以外に前提を置かずにフェルマーの最終定理を証明している」「AI による自動形式化の成果物は、もはやその上に積み上げられるだけの頑健さを持つ」と評価しました。

ただし、この記事で押さえたいのは記録の大きさではありません。11日間・数十体のエージェントを協調させ続けた「やり方」が公開されたことです。ここは業務でエージェントを組む側にとって、そのまま設計の参考になります。

何が変わったか

1. 成果そのもの

• FLT の end-to-end で計算機検証済みの証明が初めて存在するようになった
• Lean 1,300万行 / 補助定理 29,500件（Mathlib の 5倍超、Lean 史上最大）
• 所要 11日間、出力トークン 約60億、モデルは Claude Fable 5.1 相当の社内研究モデル
• 証明は Wiles の証明を Darmon–Diamond–Taylor が簡略化した版に沿う。人間の数学的入力は「Jacobian をスキームとして扱うのを優先」程度の優先順位の助言に限られた

2. 成功の鍵は「共有された状態」だった

• 最初の試行は失敗している。 エージェント群は序盤こそ進んだが、プロジェクトの状態を見失って協調が崩れた。その失敗分は最終証明の非定型部分の約7%として残っている
• 成功したのは Prove2Me（Anthropic 研究者 Tianyi Peng と Columbia 大学のグループが作った、形式化のための共同プラットフォーム）に切り替えてからである
• Prove2Me が担ったのは3点。定理文の有向非巡回グラフ（DAG）を維持して各エージェントが「次に何を証明すべきか」を決められるようにしたこと（記憶劣化の緩和と並行作業の両立）、定理文と証明をファイル分離して Lean のコンパイルを高速化し資源消費を抑えたこと、各定理文に自然言語の説明を持たせて検索と再利用を可能にしたこと
• 実行基盤は Claude Code ベースのマルチエージェント・ハーネスである

3. 検証は多重化されている

• Lean の標準3公理のみに依存し、sorry（未証明の穴）なしで全体がビルドされることを確認
• comparator ツールが、証明された主張が Mathlib 側の FLT の主張と一致することを確認し、証明全体を Lean のカーネルで再生
• Rust による Lean カーネルの独立再実装 nanoda でも全宣言を受理
• 証明全文と Claude の思考過程の抜粋は GitHub と PDF で公開され、第三者が追試できる

業務インパクト（一般企業向け）

**「AI が数学の難問を解いた」というニュースとして消費すると、実務側が得られるものを取りこぼします。**この発表で企業側が持ち帰れるのは、長時間・多エージェントのタスクをどう成立させたかという設計の話です。

最も具体的なのは、エージェントの状態を会話履歴に置かなかった点です。最初の試行が崩れた原因は、公式の説明では「エージェントが急速にプロジェクトの状態を見失い、効果的な協調をやめてしまった」ことでした。これは社内でエージェントを試した組織が例外なくぶつかる壁と同じです。長いタスクをエージェントに投げると、途中から前提を忘れ、同じ作業を繰り返し、互いの成果を無視し始める。Anthropic の解は、モデルの記憶を強化することではなく、状態を外部の共有グラフ（DAG）へ追い出すことでした。「次に何をやるか」も「何が既に終わったか」も、会話の中ではなくプラットフォーム側にある。この構造は、数学以外のタスク——大規模なコード移行、仕様書からのテスト網羅、大量ドキュメントの正規化——にそのまま移植できます。

もう1つは検証の設計です。成果物が正しいことを、生成したのと同じ系で確認していません。Lean のカーネル、comparator、そして独立実装である nanoda という3系統で受理を確認しています。業務のエージェント運用でも、「エージェントが自己申告で完了と言っている」状態と、「独立した検査系が通した」状態は別物です。ここを分けていない自動化は、規模が大きくなるほど壊れます。検査系を先に用意できるタスクほど、エージェントに任せる効果が大きいという判断基準が、この事例から引けます。形式化がうまくいったのは、Lean という完璧な検査系が最初から存在していたからでもあります。

期待の置き方には注意が必要です。公式が明言しているとおり、ここで新しいのは検証であって、新しい数学ではありません。Claude は既存の証明を機械が検査できる形に翻訳したのであって、未解決問題を解いたわけではない。自社の業務に当てはめるときも、「答えのない問題を解く」ではなく「正しさの基準が定義済みの作業を、桁違いの量でこなす」方向に読み替えるのが妥当です。加えて、使われたのは公開モデルではなく社内研究モデルであり、出力トークン60億という規模も一般的な予算感とは異なります。手法は参考になるが、コスト構造は別途見積もる必要があります。

副業・個人活用視点

個人が真似できるのは、規模ではなく構造の方です。

長時間タスクをエージェントに任せて途中で崩壊した経験がある人には、この事例の失敗談がそのまま処方箋になります。進捗と残タスクを、会話の中ではなく外部のファイルやチケットに持たせる。Prove2Me がやっていたのは、突き詰めれば「依存関係つきの ToDo を全員で共有する」ことです。個人開発なら、Markdown のタスクファイルや issue でも同じ効果が出ます。各項目に自然言語の説明を必ず付ける（Prove2Me の3つ目の工夫）のも、検索と再利用が効くようになるので効果的です。

検査系を先に作るという順序も、個人規模ほど効きます。テストを先に書いてからエージェントに実装させる、スキーマを先に定義してから変換を書かせる、といった段取りは、要するに「Lean を先に用意する」ことです。検査系がある領域では、エージェントを長く走らせるほど成果が積み上がります。逆に検査系がない領域で長く走らせると、間違いも同じ速度で積み上がります。

そしてハーネスが Claude Code ベースだった点は、手が届く話として押さえておく価値があります。数十体のエージェントを協調させた仕組みが、特別な研究用フレームワークではなく、普段使っている CLI の上に組まれていたということです。受託や個人開発で「大量の似た作業」を抱えている場合——テストの追加、型付け、リファクタリング、コンテンツの構造化——共有状態と検査系の2つを用意するところから、同じ形を小さく試せます。