フェルマーの最終定理をClaudeが11日で形式化 — Lean1,300万行を機械検証

フェルマーの最終定理の証明が、コンピュータで最後まで確かめられる形になりました。Claudeが11日間ほぼ自律で書いたLeanのコードは1,300万行、最終的な証明で使われた定理は29,500件に及びます。新しい数学が生まれたわけではありません。動いたのは、すでにある証明を機械が確認できる状態にするまでにかかる時間のほうです。

要点

• 形式化に要した期間は11日: Anthropicの研究者Tianyi Pengが、Claudeにフェルマーの最終定理の形式化を試させたところ、11日で端から端まで通る機械検証済みの証明ができあがりました
• 規模は1,300万行・29,500定理: 最終的な証明で使われた定理は29,500件。途中で証明した分まで数えると30,300件になります。Leanの証明としては過去最大で、行数は依拠している数学ライブラリMathlibの5倍を超えます
• 主題は新定理ではなく検証: 証明そのものは1995年にAndrew Wilesが発表済みで、Claudeが担ったのは「その論証をLeanが1ステップずつ確認できる形に書き直す」作業です
• 証明はGitHubで公開: anthropics/fermats-last-theorem にApache-2.0で置かれ、2026年のカーネル健全性修正を含むLean 4.33.1とMathlib v4.33.0で誰でも再検証できます
• 消費した出力トークンは約60億: 使われたのは社内の汎用研究モデルで、性能はおおむねClaude Fable 5.1と同程度と説明されています

一言でいえば、数学の中身が前進した話ではなく、「証明が正しいと確かめる作業」にかかる時間が桁で縮んだ話です。

リーマン予想での新記録と今回は何が違うのか

違いは「新しい数学を作ったか、既存の数学を検証したか」の一点にあります。2026年8月に公開されたリーマン予想の関連問題での新記録では、臨界線上の零点の割合の下限が41.6%から67.2%へ更新されました。あちらは、それまで誰も証明していなかった主張が新たに証明された事例です。

今回のフェルマーの最終定理には、新しい主張がありません。証明は31年前に完成しています。作られたのは、その論証を機械が読める言語に翻訳した成果物のほうです。電卓で計算を検算するのと同じ感覚で、証明の論理を1行ずつ確かめられるようになった、と考えると近くなります。

この違いが効くのは、信頼の作られ方です。新しい定理は、誰かが読んで納得するまで信頼できません。形式化された証明は、Leanのカーネルが通した時点で論理の穴がないことが確定します。読む人の熟練度にも、費やせる時間にも依存しません。

フェルマーの最終定理の350年と、形式化に費やされた11日

フェルマーの最終定理は「3以上の指数nについて、aⁿ + bⁿ = cⁿ を満たす正の整数の組は存在しない」という主張です。1637年頃にPierre de Fermatが本の余白に書きつけてから、証明が出るまでに350年以上かかりました。

1993年の一件は、この分野で検証がどれだけ難しいかを示す例としてよく引かれます。Wilesは講義で証明を示したものの、2か月に及ぶ検証の途中で査読者の質問から穴が見つかりました。修復には1年を要し、いったんは断念寸前まで追い込まれています。完成にこぎ着けたのは、以前に捨てた方針が使えると気づいてからのことでした。

なお、Fermat自身が書き残した「真に驚くべき証明」については、初等的な証明が数世紀にわたって見つかっていないことから、誤りだったと考えるのが今の数学界の見方です。

11日の内訳 — 数十体のエージェントとProve2Me

フェルマーの最終定理の形式化には数年かかると見込まれていました。人間の証明が「自明」として飛ばす手順もLeanは1つずつ確認する必要があり、しかも形式化済みの数学は全体のごく一部しかないためです。実際にかかったのは11日でした。

作業を進めたのは、数十体のClaudeエージェントによる分業です。概念を定義する役、中間定理を証明する役、その定理を使ってより難しい主張に進む役が並行して動きました。人間からの数学的な指示は「スキームとしてのヤコビアンは優先度が高そう」「Mazurの定理を早めに片づけて」といった高レベルの声かけに限られています。

形式化の対象になったのは、Darmon・Diamond・Taylorによる解説に沿ったWilesの証明の簡略版です。論証の骨格そのものは、Frey、Serre、Ribet、Wiles、Taylor-Wilesの筋をたどります。なお1,300万行という行数は、必ずしも成果の大きさを表すものではありません。Mathlibが簡潔でよく吟味されているのに対し、この証明は必要以上に長くなっている可能性が高い、という但し書きが添えられています。

ただし最初からうまくいったわけではありません。初期の試みでは、エージェントが早い段階で成果を出したあとプロジェクト全体の状態を見失い、協調が崩れました。この失敗した作業が最終的な証明に残ったのは、定型部分を除いた行数の約7%です。

風向きが変わったのは、Prove2Meという形式化向けの共同プラットフォームに切り替えてからでした。Tianyi Pengとコロンビア大学の共同研究者が設計したもので、3つの仕組みが効いています。

1. 定理の依存関係を有向非巡回グラフ(DAG)で保持する: 次にどの証明へ進むかをエージェント自身が判断できるようになり、記憶の劣化を抑えながら複数のエージェントを並列に走らせられます
2. 定理の主張と証明を別ファイルに分ける: 両者のつながりは独立に管理されるため、Leanのコンパイルが速くなり資源の消費も減ります
3. 各定理に自然言語の説明を持たせる: 既存の定理を検索して再利用でき、証明の道筋が単純になります

この仕組みとClaude Codeベースのマルチエージェント構成を組み合わせ、2週間弱で完走しました。エージェントを増やすだけでは崩れる作業が、状態を共有する土台を挟むと通る——今回の実務上の学びは、数学よりもこちらに寄っているように読めます。

証明が正しいと言える根拠は3段構えになっている

公開リポジトリでは、3つの検査を通したことが示されています。

1つ目は、依存する公理の確認です。既定のビルドターゲット FinalCheck.lean は、証明が依存する公理をビルド時に確かめる仕組みです。対象は propext / Classical.choice / Quot.sound というLean標準の3公理だけに限られます。sorry(証明の保留)、独自公理、native_decide のいずれかが紛れ込んでいればビルドが失敗する設計です。あわせて unsafe / extern / implemented_by / partial def / #eval を加えた計8種の構文が、どのモジュールにも現れないことが確認されています。このビルドではリポジトリの60,475モジュールすべてが通り、各宣言がLeanのカーネルで検査されました。同ファイルは、Mathlibが持つフェルマーの最終定理の主張 FermatLastTheorem も、この定理から導出しています。

2つ目は、comparatorによる照合です。leanprover/comparator v4.33.0が、Mathlibの語彙だけで書かれた挑戦用の主張とビルド結果を突き合わせました。証明された主張とそこに現れる定数がすべて一致すること、余分な公理が使われていないこと、Mathlibを含む証明全体がLeanカーネルを再通過することを確認しています。なお主張そのものはLean組み込みの自然数と + ≤ < ≠ で書かれており、Mathlib由来の要素は自然数上の ^ だけです。この ^ もMathlibがLean組み込みの冪乗として定義したもので、comparatorが素のMathlibと同一であることを確かめています。Mathlibライブラリ全体を信頼する必要はない、という設計です。

3つ目は、別実装のカーネルによる再検査です。Rustで書かれた独立のLeanカーネルnanoda 0.4.13が、同じ環境のエクスポートを受け取り、1,052,234件の宣言をエラーなしで検査しています。速度改善などの小さなパッチが4つ当てられていますが、型付け規則を足したり取り除いたり緩めたりするものは含まれません。

手元で検証し直すには何が要るか

公開された証明は読むだけでなく、自分の環境で再検証できます。ただしリポジトリは研究成果物として置かれたもので、保守も外部からの貢献の受け付けも行わないと冒頭に明記されています。要求される資源もかなり大きく、手元のノートPCで気軽に回せる規模ではありません。リポジトリに記載された実測値を工程ごとに並べると、次のようになります。

表のメモリ値は実測のピークです。並列1本あたり約5GBという目安をそのまま96倍しても153GBには一致しません。スレッドごとの山が同時には立たないためと見られます。

ディスクは .lake/ 配下に約67GB、加えてビルド中に生成されるCファイルが約220GBです。後者はビルドの進行に合わせて削除できます。

ビルドが動くのはLinuxとmacOSで、Windowsはパスが長すぎる箇所があるため対象外です。ただしcomparatorとnanodaの検証スクリプト2本はLinux専用のため、macOSではビルドまでしか通せません。スクリプトが使うのはbash / git / python3 / GNU coreutilsで、nanodaはさらに patch と cargo、そしてcrates.ioへの接続を必要とします。Leanの導入には elan とネットワーク接続も要ります。

git clone https://github.com/anthropics/fermats-last-theorem flt && cd flt
LEAN_NUM_THREADS=96 lake build
verification/comparator/run.sh
verification/nanoda/run.sh

LEAN_NUM_THREADS を省くと、ハードウェアスレッド数と同じ本数で並列に走ります。並列1本あたり約5GBを目安に、手元のメモリに合わせて値を下げてください。nanodaはcomparatorのスクリプトが用意した道具を再利用するため、この順序で走らせます。

合否の読み方も決まっています。ビルドが成功していれば、出力の末尾に依存公理が3つである旨と Build completed successfully が並びます。comparatorの判定は .verify-work/wrapper/comparator.log の最終行に出て、合格なら Your solution is okay! です。nanodaの判定は .verify-work/nanoda/run-*/nanoda.stdout に書かれ、どちらのスクリプトも成功時は終了コード0で終わります。途中でLeanの非推奨警告やスタイル警告が大量に出ますが、結果には影響しません。

資源をかけずに中身を見たい場合は、リポジトリに同梱された html/ フォルダ(約390MB)が使えます。29,511件の定理それぞれにページがあり、正確なLeanの主張、引用元と引用先、展開できる依存グラフが載っています。定義モジュール1,450件分のページと、定理名・定義名を横断する検索窓も含まれます。html/index.html をブラウザで開くだけで動き、サーバーは要りません。動作確認が取られているのはChromium系のブラウザのみです。

Claude Maxプランでも形式化に参加できるのか

小規模な題材であれば、個人向けプランの枠内でも形式化は成立しています。Anthropicの研究者が、個人契約のClaude Maxプラン3つだけを使い、Hardy-Littlewoodの円周法の応用を形式化する実験を行いました。Prove2Meだけを介して協調させたエージェント群は、ヴィノグラードフの3素数定理の形式化を3日で完了しています。

フェルマーの最終定理のほうはトークンを大量に消費するプロジェクトでしたが、こちらは規模が違います。適切な仕組みさえあれば、消費者向けの契約でも主要な定理を共同で形式化するところまで届きうるというのがAnthropicの見立てです。研究者向けの支援としては、無償・割引の契約や研究クレジットの提供が科学者向けClaude Teamプランの開放などの形で広がっています。LeanやMathlibの改善を含む大型プロジェクト向けの助成枠も、別途用意されています。

形式化が普通になると数学の書き方はどう変わるか

証明を読んだKevin Buzzardは、今回の成果を「現代の数学文献を自動的に形式化することへ向けた大きな一歩」と評しています。既存の文献に残る誤りを洗い出す道具になり、査読者の負担を軽くする方向に働く、とBuzzardは見ています。LLMが生成した数学を厳密に確認する手段としても挙げられており、現状では人手で高いコストをかけている作業にあたります。

ここから先で起こりそうなのは、論文の提出物が2本立てになることです。人間向けの説明と、機械検証を通した形式化の両方を添える運用が広がっていく見通しです。形式化が人間向けの解説に取って代わるという話ではなく、AIが生成する結果の量に数学界が追いつくための現実的な手段は、そこにしかないかもしれないとAnthropicは位置づけています。

もう1つ興味深いのは、Claudeにとっては、Leanを書くこと自体が新しい結果を出す助けになっているようだ、という観察です。Anthropicの最近のClaudeによる成果の多くは証明と並行して形式化されており、Claudeはその部分的な証明を使って自分の仮説を独立に確かめていると見られています。数値シミュレーションを書いて見立てを確かめるのと同じ使い方です。ここから先は編集部の見立てですが、証明支援系の役割は「答え合わせの道具」から「思考の途中で使う道具」へ移りつつあるように見えます。ただし人間の書き手が同じ使い方をするには、Leanを読み書きできることが前提になります。その層がどこまで広がるかは、また別の問題です。

まとめ

• 数学の新結果ではなく、検証にかかる時間の話として読むのが正確です。証明自体は1995年に完成しており、動いたのは形式化にかかる時間のほうです
• 成果物は公開されており、主張の強さも追跡できます。Apache-2.0で公開され、PROOF-PATH.md が各ステップと対応するLean定理を明示しています。Imperial College LondonのFLTプロジェクトとflt-regularに由来する106ファイルは、上流のファイル・著作権者・著者とともに ATTRIBUTION.md に記載されています
• 再検証には大きな計算資源が要ります。ビルドからnanodaまで通すと計算は22時間ほど、comparatorのために300GBの確保が推奨されます。読むだけなら同梱の html/ から入るほうが手軽です
• 形式化を試したい研究者にとっては、規模の見積もりが変わります。3素数定理が個人向けプラン3つで3日という実測は、着手のハードルを判断する材料になります
• 数学以外の領域にも波及しそうな論点があります。数十体のエージェントが状態を見失って協調を崩し、共有グラフを挟んで初めて完走した経緯は、長時間のマルチエージェント運用に共通する課題です