Claudeが11日間ひとりで働けた理由｜フェルマーの最終定理の形式証明が中小企業に教えること

2026年9月4日、Anthropicが「Claudeが11日間、大部分を自律的に働いて、フェルマーの最終定理の形式証明を完成させた」と発表しました。数学の話に見えますが、この記事で扱いたいのは数学ではありません。なぜ11日間も、人がほとんど手を入れずに走り続けられたのかという、段取りの話です。

結論を先に書きます。走り続けられたのは、AIが賢かったからではありません。一歩ごとに機械が答え合わせをする仕事だったからです。そしてこの構図は、中小企業がAIに何を任せ、何を任せないかを決めるときの、そのまま使える物差しになります。

発表文と、あわせて公開された技術資料を、数式を出さずに読み解きます。

何が起きたのか｜数字で押さえる

フェルマーの最終定理は、1637年ごろに書き残された「aⁿ＋bⁿ＝cⁿ を満たす正の整数は、nが2より大きいとき存在しない」という主張です。証明されるまでに350年以上かかり、1995年にアンドリュー・ワイルズが完成させました。Anthropicの発表文によれば、その証明は129ページあり、正しさを確かめるだけで数か月の作業が要りました。同じ発表文には、1908年に懸賞が設けられた初年度だけで621件の誤った証明が届いた、ともあります。証明が正しいかどうかを確かめる難しさは、AIが登場するはるか前からの問題でした。

今回Claudeが行ったのは、この証明を「形式化」することです。人が読むために書かれた証明を、Leanという証明支援ツールが一歩ずつ機械的に検査できる形に書き直す作業です。数学者の共同プロジェクトが2024年から取り組んでいて、公式の説明では設計図だけで86ページ、完成まで年単位を見込んでいました。

結果を数字で並べます。期間は11日。技術資料によれば、8月7日に開始し、8月17日（米東部時間）に最終の定理が「証明済み」になりました。書かれたLeanのコードは約1,300万行。数学の証明を集めた既存の共同ライブラリ（Mathlib）の5倍を超える量です。証明した定理は、途中のものを含めて29,511（発表文では約29,500と表記）。使った公理はLeanの標準的な3つだけで、証明した定理の文が既存ライブラリのフェルマーの最終定理の文と一致することも、外部の独立した検査ツールで確かめられています。

数十のClaudeのエージェントが並行して働き、概念を定義し、途中の定理を証明し、それを使ってさらに難しい主張を証明する、という積み上げ方でした。そして人が書いたのは、目標となる定理の一行だけです。

この最後の一点が、この記事の出発点です。

なぜClaudeは11日間ひとりで走れたのか｜答え合わせを機械がした

あわせて公開された技術資料には、人の関与について次のように書かれています。

人は、優先順位についてときどきコメントしたり励ましを送ったりしたが、目標となる定理の一行の文以外には、数学もLeanのコードも一切書いていない。

発表文には、その「ときどきのコメント」の実例も載っています。「Jacobianをスキームとして扱うのが優先度が高そうだ」「Mazurの定理を早めに終わらせて」。中身は本題ではないので、読み飛ばして大丈夫です。大事なのは、これが方針の一言であって、作業の指示ではないことです。たとえるなら、社長が「来期の予算表を作って」と一言だけ言って部屋を出る依頼の仕方のようなものです。

普通なら、それで11日間放っておけば、どこかで道を外れます。AIが自信満々に間違えることも、同じ質問に毎回違う答えを返すことも、業務でAIを使った人なら知っています。では、なぜ今回は外れなかったのか。発表文は、この出来事の新しさをこう説明しています。

ここで新しいのは検証のほうである。数学の証明を、電卓で計算を確かめるのと同じように確かめること。

Leanという道具は、証明の一歩一歩を機械的に検査します。発表文の言葉を借りれば、人が読む証明は当たり前の手順を飛ばしますが、Leanは些細な一歩まで全部を見せる必要があります。そのぶん、間違った一歩は通りません。いわば、切符に不備があれば絶対に開かない自動改札です。

この構図が、11日間の自律を成り立たせました。人が途中を見ていなくても、間違いは先に進めない。AIが道を外れたとしても、外れた一歩は検査で止まり、そこから先が積み上がることはない。だから人は、目標の一行を渡して、あとは優先順位を時々つぶやくだけで済んだのです。

言い換えると、AIに長く任せられるかどうかは、AIの賢さではなく、答え合わせの仕組みで決まります。これがこの記事でいちばん伝えたいことです。

最初の試みは失敗していた｜分かれ目は「仕事の地図」

ただし、答え合わせの仕組みだけでは足りませんでした。発表文には、あまり見出しにならない一節があります。

Claudeの初期の試みのいくつかは失敗した。エージェントたちは早い段階では成果を出したものの、すぐにプロジェクトの状態を見失い、効果的に協働できなくなった。失敗した試みは、最終的な証明の（自動生成部分を除く）行数の約7%に寄与している。

賢いAIを数十体並べても、最初はうまくいかなかったのです。原因は能力ではなく、「いま全体のどこまで進んでいて、次に何をすべきか」を共有できなかったこと。たとえるなら、地図を持たずに大人数で山を登ろうとして、互いの位置が分からなくなった状態です。

成功に変えたのは、Prove2Meという共有の台帳でした。コロンビア大学のグループが開発した、数学の形式化を協働で進めるための公開の仕組みです。発表文は、これが役に立った点を3つ挙げています。

1つ目は、次に何をすべきかの地図。定理どうしの依存関係を図にして共有し、各エージェントはそれを見て次に取り組む証明を決めました。公式はこれが「記憶の劣化を和らげ、複数のエージェントが並行して働くのに特に役立った」と書いています。2つ目は、検査を速くすること。定理の文と証明を別のファイルに分けて、答え合わせの待ち時間と計算資源を減らしました。3つ目は、探して再利用できること。各定理に自然な言葉の説明文を付け、すでに証明したものを探して使い回せるようにしました。

この3つは、どれもAIの能力を上げるものではありません。Prove2Meは、いわば工程表と部品棚を兼ねた台帳のようなもので、人間の組織で言えば、進行管理と部品の共有管理にあたります。数十人が同時に働く現場で、それが無ければ崩れるのは人間でも同じです。

自律を支えた3つの仕組み

ここまでを整理すると、11日間の自律を支えた仕組みは3つあります。

①機械の答え合わせ。Leanが一歩ごとに正しさを判定し、間違いは先に進めない。これが最も重要で、人が途中を見なくてよい理由そのものです。

②仕事の地図。共有の台帳で、次に何をするかと、どこまで進んだかを全員が見る。これが無いときには、実際に協働が崩れました。

③相互チェック。技術資料には「ある主張に取り組む前に、通常は別のエージェントがそれが書かれたとおり正しいかを確かめた。これにより、誤った主張がいくつか早い段階で見つかった」とあります。3日目の記録には、あるエージェントの主張の誤りを別のエージェントが指摘し、指摘された側が確認して同意し、予定していた進め方を捨てた場面が残っています。

3つとも、AIの賢さを上げる話ではありません。間違いが残らないように段取りを組んだという話です。AIエージェントとは何かで「指示待ちAIから自走するAIへ」と書きましたが、自走を成り立たせるのは、走る力ではなく、外れたときに止まる仕組みのほうでした。

自社の業務に置き換える｜「答え合わせが機械でできる仕事」はどれか

ここからが本題です。この構図を自社の業務に当てると、AIに長く任せられる仕事と、短く区切るべき仕事の線引きが見えてきます。物差しはひとつ、「その仕事の答え合わせは、機械でできるか、人しかできないか」です。

左側の仕事には共通点があります。正しいかどうかを、事前に決めたルールで機械が判定できることです。金額が一致するか、必須欄が埋まっているか、形式が合っているか。これらは今回のLeanと同じ役割を果たします。AIが間違えても、判定で止まり、外れた分だけが人に上がってくる。だから長く任せられます。

右側の仕事は、正しさを人しか判定できません。謝罪文が相手にどう受け取られるか、この応募者を採るべきか。ここに機械の答え合わせは置けないので、AIに任せるなら短く区切って、一つずつ人が見ることになります。任せる範囲は下書きや材料の整理までです。

注意したいのは、この線引きがAIの得意・不得意とは別だということです。謝罪文の下書きは、AIはかなり上手に書きます。それでも長く任せられないのは、上手いか下手かではなく、正しいかどうかを機械が判定できないからです。逆に、照合作業はAIでなくてもできますが、AIに任せて長く走らせられるのは、判定が機械でできるからです。「賢いから任せる」ではなく「答え合わせができるから任せる」。順序を入れ替えるだけで、任せ方の迷いがかなり減ります。

では、機械の答え合わせは、どう用意すればよいのでしょうか。今回の証明ではLeanという既製の道具がありましたが、業務にはそんな道具は転がっていません。代わりになるのは、「合格の条件を、先に文章で書き出す」という作業です。請求書の照合なら「請求書の金額と入金額が一致し、入金日が支払期日から5営業日以内なら合格。それ以外は人に上げる」。記入漏れの確認なら「必須欄の一覧はこれで、すべて埋まっていれば合格。空欄があれば、どの欄かを添えて人に上げる」。この一文があれば、AIが判定したあとに、その判定が正しかったかを機械的に照らせます。Leanが証明の一歩ごとにしていたことを、業務の一件ごとにするわけです。

この条件を書き出してみると、思ったより書けない業務が多いことに気づきます。「いい感じにまとめて」「失礼のないように」といった、人なら通じる指示は、合格の条件として書き下せません。それは悪いことではなく、その業務が右側、つまり人しか判定できない仕事であると分かった、ということです。線引きは、業務を眺めて考えるより、合格の条件を書こうとしてみるほうが早く決まります。

もうひとつ、今回の発表から持ち帰れるのは「外れた分だけが人に上がる」という形です。Leanが通した証明は人が見ていません。見るのは、通らなかったところと、最後の結果だけです。業務でも同じで、AIが判定して合格になった案件を人が全部見直すなら、任せた意味がありません。合格は流し、不合格と判定不能だけを人が見る。人の時間を、機械が判定できなかったところにだけ使う。これが、答え合わせを機械に置く本当の効果です。

そして、機械で答え合わせできる仕事であっても、今回の失敗が教えるとおり、複数の作業を並行で走らせるなら仕事の地図が要ります。どこまで進んだか、次に何をするか、できたものはどこにあるか。それを共有する台帳が無いと、AIでも人でも協働は崩れます。この設計の考え方はAIエージェント導入を成功させる実務設計で、最初に決めるべき5つの点として整理しています。

限界と費用｜そのまま真似する話ではない

ここまで読むと「では自社でも」となりますが、発表文と技術資料は限界も正直に書いています。3点にまとめます。

1つ目は費用の規模です。発表文によれば、Claude Codeを土台にした複数エージェントの仕組みで、約60億の出力トークンを使い、モデルは公開されていない内部の研究用モデル（Claude Fable 5.1におおむね相当すると説明されています）でした。「トークンを多く使う案件だった」と公式自身が書いています。60億トークンがいくらに相当するかは、内部モデルのため単価が公表されておらず、計算できません。中小企業がこの規模の計算をそのまま回す話ではない、とだけ押さえておくのが正確です。Fable 5.1そのものについてはClaude Fable 5.1登場で扱っています。

2つ目は証明の品質です。技術資料は「大半は機械が書いたもので、Mathlibが受け入れる形にはまだなっていない」と書き、発表文の注釈は「われわれの証明は必要以上に長い可能性が高い」と認めています。正しいことと、きれいであることは別です。人間の職場でも、動くが読みにくいマニュアルはあります。

3つ目は途中の記録です。技術資料に載っている思考の抜き書きについて、「Claudeがそこで述べている数学的な主張を、われわれは独立に検証していない」と明記されています。保証されているのは、最終的な証明がLeanの検査を通ったという一点です。その証明そのものはGitHubで公開されていて、誰でも検査をやり直せます。途中の言葉を額面どおりに受け取らない、という姿勢は、AIの出力全般に当てはまります。

なお発表文は、より小さな実験にも触れています。Anthropicの研究者が、同社の個人向けプランであるClaude Maxを3つ使って、別の定理を3日で形式化したというものです。公式はこれを「適切な足場があれば、消費者向けの契約でも主要な結果の共同形式化は達成可能だと考えている」と説明しています。今回の記事の主張と重なるのは「足場があれば」の部分です。持ち帰るべきは規模ではなく、構図です。

私たちの見解｜賢さではなく、答え合わせの仕組み

「AIが11日間ひとりで働いた」という見出しは、AIの能力の話として読まれがちです。しかし発表文と技術資料を読み終えて残ったのは、むしろ逆の印象でした。能力の高いAIを数十体並べても、最初は失敗した。成功に変えたのは、機械の答え合わせと、仕事の地図と、相互チェックという、どれも段取りの側の仕組みでした。

これは中小企業にとって、むしろ良い知らせだと考えています。最先端のモデルを持っているかどうかより、自社の業務のどこに機械の答え合わせを置けるかを見つける力のほうが、任せられる範囲を決めるからです。それは技術の話ではなく、業務を知っている人にしかできない仕事です。

実務での順番は3つです。第一に、自社の業務を「答え合わせの相手」で分ける。機械で判定できる仕事から、AIに長く任せる候補を選ぶ。第二に、その判定基準を先に書き出す。「金額と日付が一致していれば合格」のように、Leanにあたるものを人間の言葉で用意する。第三に、複数の作業を並行させるなら、進捗と次の作業を共有する台帳を置く。90日で成果を出す導入の実行設計で書いた「小さく始めて、測って、広げる」順序は、ここでもそのまま使えます。

この記事の考え方をもとに、業務のどこにAIエージェントを置けるかを一緒に整理する支援も行っています。詳しくはAIエージェント導入支援をご覧ください。

まとめ

AIに何を任せるかを考えるとき、「このAIはどこまで賢いか」から入ると、答えは毎月変わります。「この仕事の答え合わせは誰ができるか」から入れば、答えは業務のほうに固定されます。今回の発表は、その物差しの正しさを、いちばん極端な例で示してくれたのだと受け止めています。

よくある質問

AIが数学の大定理を「発見」したということですか？

違います。Anthropicの発表文は、新しいのは発見ではなく検証のほうだと明記しています。フェルマーの最終定理は1995年にアンドリュー・ワイルズが証明を完成させており、今回Claudeが行ったのは、その証明の筋道をLeanという証明支援ツールが機械的に検査できる形に書き直すことでした。人が読むための証明は当たり前の手順を飛ばしますが、Leanは些細な一歩まで全部を見せる必要があります。その書き直しに、数学者たちは年単位の時間を見込んでいました。それを11日間で終えた、というのが今回の出来事です。

「ひとりで働いた」というのは、人が何もしなかったということですか？

公式の記述では、人が書いたのは目標となる定理の一行の文だけで、数学もLeanのコードも一切書いていません。ときどき優先順位についてのコメントや励ましを送った程度で、発表文には「Jacobianをスキームとして扱うのが優先度が高そうだ」「Mazurの定理を早めに終わらせて」といった短い指示の例が載っています。ただし、ひとりのAIが働いたわけではなく、数十のClaudeのエージェントが並行して概念を定義し、途中の定理を証明し、それを積み上げて協働しました。また最初の試みは失敗しており、成功したのは仕事の地図を共有する仕組みを入れてからです。

うちの会社でも、AIに11日間任せられますか？

そのまま同じことができる、という話ではありません。今回の証明は約60億の出力トークンを使った大規模なもので、Anthropic自身が「トークンを多く使う案件だった」と書いています。ただし読み取れる原則はあります。長く任せられたのは、AIの賢さのおかげというより、一歩ごとに機械が正しさを確かめる仕組みがあったからです。自社の業務で言えば、金額の一致や記入漏れのように、正しいかどうかを機械が判定できる仕事は長く任せやすく、顧客への謝罪文の言い回しや採用の判断のように、正しさを人しか判定できない仕事は短く区切って人が確認する、という分け方になります。

証明は完全に正しいと確認されたのですか？

証明そのものはLeanが検査し、Leanの標準的な3つの公理だけを使っていること、証明した定理の文が数学ライブラリMathlibにあるフェルマーの最終定理の文と一致することが、外部の独立した検査ツールで確認されています。数学者ケビン・バザード氏も、数学の公理以外の仮定を使っていないと評しています。一方で限界も公式に書かれています。証明は機械が書いた部分が大半で、Mathlibが受け入れる形にはまだなっていないこと、必要以上に長い可能性が高いこと、そして途中の思考の抜き書きについては数学的な主張を独立に検証していないことです。正しさの保証は、あくまで最終的な証明がLeanを通ったという点にあります。

参照元・出典

• Anthropic「Formalizing Fermat’s Last Theorem」（2026年9月4日公開・9月6日確認）— 11日間の自律、13,000,000行、約29,500の定理、人の入力が高水準の指示に限られた旨、最初の試みの失敗と約7%、Prove2Meの3つの役割、約60億出力トークン、3つの公理と外部検査、限界の注釈、個人向け契約3つでの実験
• Anthropic「Formalizing Fermat’s Last Theorem in Lean — A timeline and selected excerpts」（PDF）（2026年9月6日確認）— 29,511の定理、約1,300万行（自動生成分を除くと約1,050万行）、標準の3公理、独立した外部検査ツール2つ、8月7日開始・8月17日完了、人は目標の一行以外に数学もLeanも書いていない旨、相互チェックの記述、思考の抜き書きは独立検証していない旨、Mathlibが受け入れる形ではない旨
• GitHub「anthropics/fermats-last-theorem」（2026年9月6日確認）— 証明の公開先
• Chen, Marwaha, Lu, Yuen, Peng（2026）「Prove2Me: An open collaborative platform for scaling math formalization」（arXiv）（2026年9月6日確認）— 共有の台帳（Prove2Me）の論文