Anthropic、フェルマーの最終定理のLean形式化をClaudeが11日で完了と発表

Anthropicが2026年9月4日、フェルマーの最終定理の機械検証済み証明を公開した。Leanで1,300万行、中間定理29,500件。数十体のエージェントが最初は失敗し、Prove2Meの依存グラフで立て直した経緯と、どこまでが第三者に確認されているかを整理する。

Anthropic Claude Lean mathematics AI-agent formal-verification

Anthropicが2026年9月4日、フェルマーの最終定理（FLT）の機械検証済み証明を公開した¹。同社の説明では、Claudeが11日間、大部分は自律的に作業して証明をLeanで書き上げ、その過程で1,300万行のLeanコードと29,500件の中間定理を生み出したという。

数学の側で新しいものが得られたわけではない。証明そのものは1995年のAndrew Wilesのものであり、今回作られたのは「その証明が正しいことを計算機が確かめられる形」である。Anthropicはこの点を明示していて、リーマン予想をめぐる最近のAI主導の研究が新しい数学を生んだのに対し、今回新しいのは検証の側だと述べている。

129ページの証明に、2か月後に見つかったギャップ

なぜ検証がそれほどの手間なのかは、この定理自体の来歴がよく示している。Wilesの証明は129ページあり、検証には数か月の骨の折れる作業を要した¹。1993年6月に3日間の連続講演で発表されたとき、複数の数学者が2か月かけて検証した途中で、あるレビュアーの質問が致命的なギャップを露呈させている。Wilesは1年かけて修正に取り組み、当初は単独で、その後は元学生のRichard Taylorと組んだ。正しい証明が公表されたのは1995年5月だった。

証明支援系に読ませれば、この種の見落としは原理的に起きない。ただし人間向けの証明は「明らかな手順」を大量に省略して書かれているうえ、何世紀もの既刊研究に依拠している。形式化はその全部を、すでに形式化されているごく一部の数学から積み上げ直す作業になる。FLTの形式化には数年かかると見込まれており、コミュニティがプロジェクトの初期フェーズを記述するために使ってきたblueprintだけで86ページある。

数十体のエージェントは、最初つまずいた

今回の作業で本サイトの読者に近いのは、証明の中身よりも回し方のほうだろう。

Anthropicによれば、数十体のClaudeエージェントが協働して概念を定義し、中間定理を証明し、それらを使ってより難しい主張を証明していった¹。ただし最初からうまくいったわけではない。初期の試みは失敗しており、エージェントは早い段階では成果を出したものの、プロジェクトの状態をすぐに見失って効果的に協働しなくなったと同社は書いている。それらの失敗した試行は、最終的な証明の非ボイラープレート行の約7%に痕跡を残している。

転機になったのは、Anthropicの研究者Tianyi PengとColumbia Universityの共同研究者が設計した、形式化のためのオープンな協働プラットフォーム Prove2Me への切り替えだった。同社が挙げる寄与は3点ある。定理の主張を有向非巡回グラフ（DAG）として保持し、エージェントが次に何を証明すべきかを決められるようにしたこと。これが記憶の劣化を抑え、複数エージェントの並行作業を可能にしたとされる。定理の主張と証明を別ファイルに分け、その間のリンクを独立に管理することでLeanのコンパイルを速め資源消費を抑えたこと。そして各定理に自然言語の説明を持たせ、検索と再利用を可能にしたことである。

つまり、状態を共有する外部の構造をエージェント群の外側に置くことで、長時間の並行作業が成立するようになった、という設計上の話になっている。エージェントを並べれば仕事が進むわけではないという点は、AIエージェントを業務に組み込む場面でもそのまま当てはまる。

最終的に、Claude Codeベースのマルチエージェントハーネスとこの組み合わせで、2週間弱で証明が完成した。消費した出力トークンは約60億で、使われたのはClaude Fable 5.1に概ね匹敵する汎用の社内研究モデルだとされている。製品として提供されているモデルそのものではない点は、読むうえで押さえておきたい。

人間からの数学的な入力は、Tianyiによる時折の高レベルな指示に限られたという。Anthropicが例として挙げているのは「Jacobianをスキームとして扱うのが優先度が高そうだ」「Mazurの定理を早めに終わらせろ」といった短い指示である。

何が確かめられていて、何が自己申告か

数字が大きいだけに、どこまでが第三者の確認を経ているかは分けて読む必要がある。

計算機による検証の部分は具体的だ。完成した証明はLeanで検証され、Leanの標準3公理のみを使っている¹。さらにcomparatorによって、証明された定理の主張がMathlib自身のFLTの主張と一致することが確認されている。形式化の対象としたのはWilesの証明そのものではなく、Darmon・Diamond・TaylorによるWiles証明の簡略版である。

外部の目としては、Imperial College Londonの Kevin Buzzard が完成した証明をレビューしている。Buzzardは2024年にLeanでのFLT形式化を目指す複数年のコミュニティ活動を始めた人物で、Anthropicの証明も彼のプロジェクトとflt-regularプロジェクトから部品を取り入れている。Buzzardは、この形式化が代数・調和解析・幾何・数論にわたること、そしてAIによる自動形式化の成果物が「その上に積み上げられる程度には頑健になった」ことを評価している。

一方で、Buzzard自身の言葉は「Anthropicの研究者が11日しかかからなかったと言っている」という伝聞の形になっている¹。所要日数と自律性の度合いは、いまのところ同社の申告であって独立に検証されたものではない。

規模の数字にも注意がいる。1,300万行はMathlibの5倍を超えるが、Anthropic自身が脚注で、これは一部にはMathlibが簡潔でよくレビューされているのに対し、自分たちの証明は必要よりずっと長い可能性が高いためだと書いている。行数は成果の大きさというより、いまの自動形式化がどれだけ冗長かの指標に近い。

検証を安くする話として読む

この発表の含意は、数学の外にもある。

Buzzardは、自動形式化の技術が現在の数学の体系から誤りを洗い出し、査読者の負担を軽くするだろうとしたうえで、LLMが生成した数学を厳密に検証できるようにもなると述べている¹。彼によれば、それは現状きわめてコストの高い人力の作業である。Anthropicも、人間向けの記述と並べて形式化された証明を出すことが一般的になると予想している。ただし形式証明が人間に理解できる説明を置き換えるべきだとは考えていない、という留保を付けている。

「AIの出力を、人間が全部読まずに信頼してよいか」という問いは、ハルシネーションを抱えたモデルを実務に入れるときの中心的な論点でもある。数学の形式化はその極端な形で、検証を機械に肩代わりさせられる領域がどこまで広がるかを示している。同じ発想の動きとして、OpenAIは2026年8月に数学・理論計算機科学の未解決問題10件の結果を、Lean 4の証明書つきでGitHubに公開している。主張と一緒に検証の材料を置く、という点で今回の発表と同じ方向を向いている。

裾野の話も添えられている。Anthropicの研究者は、個人のClaude Maxプラン3つだけを使い、Prove2Meを通じてのみ協働する形で、Vinogradovの3素数定理の形式化を3日で完了させたという¹。同社は「適切なスキャフォールドがあれば、消費者向けAIサブスクリプションでの主要結果の協働形式化は達成可能だと考える」と書いている。

なお同社は、純粋数学や形式化に取り組む数学者を含む外部研究者への支援を、自社と他のラボがともに拡大したことにも触れている。Anthropic自身の直近の動きとしては、8月27日に研究者向けのClaude 1万席の開放とAI for Scienceの分野拡大を発表していた。今回の発表は、その支援の対象として想定される研究の一例を、自社の手で示した形になっている。

証明そのものは、ウォークスルーとあわせてGitHubで公開されているとされている。11日という数字を確かめる術はいまのところないが、出力されたLeanコードのほうは、誰でもLeanに読ませることができる。