はじめに

2026年9月4日、Anthropic が「フェルマーの最終定理の、完全に機械検証された証明」を公開しました。Claude が11日間ほぼ自律的に動き、証明を Lean というプログラミング言語で書き下した、という発表です。

ここで多くの人が同じ疑問を持つはずです。フェルマーの最終定理は1995年にアンドリュー・ワイルズが証明済みのはずでは？

そのとおりです。今回 Anthropic が主張しているのは「新しい数学を発見した」ことではありません。公式ページも、リーマン予想をめぐる別の成果と対比する形で「今回あたらしいのは検証のほうだ」と明記しています。証明そのものではなく、証明を機械が最後の一歩まで追いかけられる形に翻訳した、というのがこの発表の中身です。

そしてその「翻訳」は、エンジニアにとって決して他人事ではありません。書いたものが機械のチェックを通ることと、書いたものが正しいことは、別だからです。

📌 この記事の3行まとめ
  • Claude が11日間で Lean のコード約1,300万行を書き、29,511個の定理を積み上げてフェルマーの最終定理に到達した（いずれも Anthropic 発表値）。Lean のカーネルと外部の検査ツール2種が、公理3つだけに依存していることを確認している
  • 価値は「証明された」ことではなく、29,511個の定理が機械検証済みの部品として公開されたこと。ただし Anthropic 自身が「現状のままでは Mathlib に入る形ではない」と明言している
  • Kevin Buzzard 氏が2024年から積み上げてきた土台の上に乗った成果。氏本人がレビューし、自身のブログで祝意を示したうえで「私の仕事が無くなったわけではない」とも書いている

1. 🧩 フェルマーの最終定理とは何か

まずは主役の定理から。数学に馴染みがなくても、主張そのものは中学生でも読めます。

x^n + y^n = z^n

この式について、n が3以上のとき、正の整数 x, y, z の組は存在しない——これがフェルマーの最終定理です。

n が2のときは 3^2 + 4^2 = 5^2 のようにいくらでも見つかります（ピタゴラス数）。ところが指数を1つ上げて3にした瞬間、解が1つも無くなる。この落差が、この問題を350年以上のあいだ生かし続けました。

余白から始まった350年

1637年ごろ、フランスの法律家ピエール・ド・フェルマーが、ディオファントスの『算術』の余白にこの主張を書き込み、続けてこう記しました。「私はこの命題の真に驚くべき証明を見つけたが、余白が狭すぎて書けない」

その「驚くべき証明」は、ついに出てきませんでした。以後、数学者たちは指数を1つずつ潰していくことになります。オイラーが n=3 を、ソフィー・ジェルマンが多くの素数指数について部分的な結果を、クンマーが「正則素数」と呼ばれる素数のクラスについて証明する。そうやって少しずつ削られながら、全体は残り続けました。1908年には10万マルク（Anthropic の換算で現在の100〜200万ドル相当）の懸賞金がかけられ、最初の1年だけで621件の誤った証明が寄せられたと記録されています。

ただし、この戦い方には限界がありました。指数は無限にあるので、1つずつ潰していっても終わらないのです。

350年を動かした「橋」——谷山–志村予想

では、なぜ350年も動かなかった問題が、20世紀の後半になって突然決着したのか。答えは「フェルマーの最終定理そのものを、もっと強力に攻めた」ことではありません。まったく別の場所に架かった橋を渡ったからです。

その橋が 谷山–志村予想（谷山–志村–ヴェイユ予想。現在はモジュラリティ定理）です。主張はこうです。

💡 ワード解説：楕円曲線・モジュラー形式・谷山–志村予想

楕円曲線は y^2 = x^3 + ax + b の形で書ける曲線のことで、楕円とは関係ありません。暗号（ECDSA など）で使われるあの楕円曲線と同じものです。整数解を数える、つまり数論の対象です。

モジュラー形式は、ある種の対称性を持つ複素関数の一族。こちらは解析の対象で、出自も道具立てもまったく違います。

谷山–志村予想は、この2つが対応すると言います。すなわち「有理数体上のすべての楕円曲線は、モジュラーである」。数論の対象を数え上げて出てくる数列と、解析の対象の展開係数が一致する、という主張です。分野をまたいで辞書を1冊渡すようなもので、片側で難しい問題が、もう片側では易しくなることがある。これが「橋」と呼ばれるゆえんです。

この予想は、戦後の日本から出ています。1955年に東京と日光で開かれた「代数的整数論に関する国際シンポジウム」で、谷山豊が問題として提出したものが起点でした。同席していた志村五郎がのちにこれを精密化し、現在の形に整えます（André Weil もこのシンポジウムの基調講演者の一人で、予想の名にヴェイユが加わることがあるのはこの縁です）。谷山は1958年に31歳で世を去り、予想が証明される日を見ていません。350年の難問を落とした鍵は、戦後まもない日本で、まだ20代だった数学者が投げた問いから育ったものでした。

フェルマーとの橋渡し——フライ・セール・リベット

とはいえ、谷山–志村予想はフェルマーの最終定理とは何の関係もない主張に見えます。両者が繋がったのは1980年代でした。

1986年、ゲルハルト・フライが指摘します。もしフェルマーの最終定理に反例 a^p + b^p = c^p があったら、その解から次のような楕円曲線を作れる、と。

y^2 = x\,(x - a^p)\,(x + b^p)

これがフライ曲線です。フライ曲線は、あまりに性質が良すぎてモジュラーではあり得ない形をしている。ジャン゠ピエール・セールがこの見立てを精密な予想（ε予想）として定式化し、1990年にケン・リベットがそれを証明しました（レベル下げ）。

これで論理が閉じます。

  1. フェルマーの最終定理に反例があれば、フライ曲線が作れる
  2. リベットの定理により、フライ曲線はモジュラーではない
  3. ところが谷山–志村予想が正しければ、すべての楕円曲線はモジュラー
  4. 矛盾。よって反例は存在しない

つまり、谷山–志村予想を（フライ曲線が該当する範囲で）示せば、フェルマーの最終定理が従う。ここが決定的でした。

そしてワイルズが橋を渡った

1993年6月、アンドリュー・ワイルズがケンブリッジのニュートン研究所で3日連続の講演を行い、その橋を渡ってみせます。注意したいのは、ワイルズが直接証明したのはフェルマーの最終定理ではないということです。彼が示したのは半安定な楕円曲線についての谷山–志村予想であり、フェルマーの最終定理はそこから帰結として落ちてきます。

ところが検証開始から2か月後、査読者の質問が証明の致命的な穴を突きました。ワイルズは1年をかけて、最後は元教え子のリチャード・テイラーと組んでこれを埋めます。Gerd Faltings が米国数学会の会報に寄せた解説（1995年7月号）によれば、テイラーとワイルズの論文はその穴を塞いだのではなく迂回したもので、完成は1994年9月でした。論文は1995年5月に公表されます。

なお、半安定に限らない一般の楕円曲線についてのモジュラリティ定理は、その後2001年に Breuil・Conrad・Diamond・Taylor の4人が完成させました（米国数学会誌 JAMS 14巻4号、843〜939ページ）。

そして今回の Claude の証明は、この1990年代の道筋——フライ曲線、マズール、ラングランズ–タネル、リベットのレベル下げ、そして R = T——をそのまま Lean で辿っています。§4 に載せた依存関係の図に Level lowering (Ribet) や Modularity lifting, R = T といった枝が並んでいるのは、このセクションで説明した構造がそのまま形式化されたからです。

timeline title フェルマーの最終定理 350年の道のり 1637-1800年代 : 1637 フェルマーが余白に予想 : 1770 オイラーが n=3 を証明 : 1820年代 ジェルマンの成果 : 1850 クンマーの正則素数 1900-1994年 : 1908 賞金10万マルクの懸賞 : 1955 東京・日光で谷山が提出 : 1986 フライ曲線 : 1990 リベットの定理 : 1993 ワイルズ講演 穴が発覚 : 1994 テイラーと修復 1995-2026年 : 1995 ワイルズの論文が公表 : 2001 一般の場合が完成 : 2024 Buzzard の形式化計画 : 2026 Claude が Lean で完走

もっと知りたい人へ

この350年の物語そのものが、一冊のノンフィクションとして読めます。サイモン・シン『フェルマーの最終定理』（青木薫 訳・新潮文庫）は、フェルマーの書き込みからワイルズの証明までを、数学の予備知識がなくても追える形で描いた本です。ワイルズが7年間ほとんど一人でこの問題に取り組んだ経緯や、1993年に見つかった穴とその修復までが、当事者への取材をもとに語られます。上で「橋」と呼んだ谷山–志村予想がどう生まれたかも、同書が扱う中心的な話題のひとつです。この記事の §1 で駆け足に済ませたところが、まるごと一冊分の厚みで書かれていると思ってください。

サイモン・シン『フェルマーの最終定理』新潮文庫 表紙 ▶ サイモン・シン『フェルマーの最終定理』（新潮文庫）を Amazon で見る

※本記事にはアフィリエイトリンク（Amazon アソシエイト）が含まれます。

2. 🔍 「もう証明済み」なのに、なぜ形式化するのか

ここが今回の話の芯です。

人間の査読は、思ったより脆い

ワイルズの1993年の講演から、穴が見つかるまで2か月かかりました。世界最高峰の専門家たちが、2か月かけてやっと1か所の欠陥に気づいたわけです。これは例外ではありません。Anthropic の発表は、脚注で似た事例を並べています。

  • ケプラー予想（トマス・ヘイルズ、1998年）は査読に4年かかり、12人の審査団は最終的に「99%の確信」で決着させた。ヘイルズ氏はのちに20人規模のプロジェクト Flyspeck を率いて、証明そのものを形式化した
  • ポアンカレ予想（グリゴリー・ペレルマン、2002年）は、数学界が受け入れるまでにおよそ4年と、300ページ級の解説3本を要した
  • 弱いゴールドバッハ予想（ハラルド・ヘルフゴット、2013年）は、いまも査読中

つまり「査読を通った」は、「論理の全ステップが検査された」を意味しません。人間の証明は「自明である」「同様にして」といった省略で書かれていて、その省略がすべて埋まる保証はどこにもないからです。

Lean は省略を許さない

Lean（リーン）は、証明を書くためのプログラミング言語です。数学の公理と論理規則を最初から知っていて、書かれた証明が正しいかどうかをプログラムとして検査します。ソースコードをコンパイルするのと同じ操作で、この証明は通る／通らない、が返ってくる。

Lean が紙の証明と決定的に違うのは、「自明」「同様に」が書けないことです。人間の読者向けの証明は明らかな手順を飛ばしますが、Lean はどんなに些細なステップでも全部見せろと要求します。しかも人間の証明が何世紀ぶんもの既刊の結果に寄りかかれるのに対して、形式化はすでに形式化済みのごく一部からしか出発できません。

💡 ワード解説：Lean / Mathlib / 形式化 / autoformalization

Lean：証明支援系（proof assistant）と呼ばれるプログラミング言語。Leonardo de Moura 氏らが開発。証明を書くと、その論理をカーネル（中核の検査器）が機械的に検証します。

Mathlib：Lean のコミュニティが積み上げてきた数学ライブラリ。事実上の標準ライブラリで、数百人の数学者が貢献しています。Buzzard 氏（Mathlib のメンテナでもある）は自身のブログで、Mathlib は約230万行、書き上げるのに9年かかったと書いています。

形式化（formalization）：人間の言葉で書かれた数学を、Lean のような機械が検査できる言語へ書き下すこと。翻訳作業であって、新しい数学を作ることではありません。

autoformalization（自動形式化）：その翻訳を AI に任せること。今回の成果はこれにあたります。

だから「査読済み」と「機械検証済み」は別物

人間の査読 Lean による検証
検査する対象 論文に書かれた議論 公理まで遡った全ステップ
「自明」の扱い 読者が補って納得する 補えなければ通らない
所要時間 数か月〜数年 数時間の計算機時間
見落としの可能性 ある（実例が複数ある） カーネルとツール群を信頼する限り無い

Lean が保証してくれるのは「述べられた主張が、公理から確かに導かれている」ことです。裏返せば、それ以上は保証しません。この線引きは §5 でもう一度、今回の実物に即して見ます。

3. ⏱️ 11日間で何が起きたのか

Anthropic は発表と同時に、17ページの PDF で日ごとの経過を公開しています。以下は同社の発表値です。

項目 発表値
期間 2026年8月7日〜8月17日（11日）
最終定理が Proved になった時刻 8月17日 22:00（米東部時間）
証明した定理 30,300件（最終証明に使ったのは 29,511件）
Lean のコード量 約1,300万行（生成された定型部分を除くと約1,050万行）
出力トークン 約60億
モデル 「Claude Fable 5.1 とおおむね同等」の汎用内部研究モデル
人間が書いた数学・Lean ゴール定理の1行の宣言のみ

底本になったのは、ワイルズの原論文そのものではありません。アンリ・ダルモン、フレッド・ダイアモンド、リチャード・テイラーによる解説（1995年、154ページ）に沿った簡略版の道筋です。ちなみにワイルズの原論文は Annals of Mathematics 141巻3号の443〜551ページ（109ページ）、続けて載ったテイラーとの共著論文が553〜572ページ（20ページ）。Anthropic が発表で使っている「129ページ」は、この2本を合わせた分量にあたります。

複数の Claude が Prove2Me の上で分業した

最初の試みは失敗しています。Anthropic によれば、エージェントたちは序盤こそ成果を上げたものの、すぐにプロジェクトの状態を見失い、協調をやめてしまった。その失敗した作業は、最終的な証明の非定型行のうち約7%として残っているそうです。

うまくいったのは、Prove2Me というプラットフォームに切り替えてからでした。コロンビア大学の Tianyi Peng 氏（Anthropic の研究者でもある）のグループが設計した、数学の形式化のための公開協働プラットフォームです。arXiv の論文（2608.28433）によれば、利用者が形式化の「ミッション」を立ち上げ、そこに AI エージェントが証明を寄せていくという設計になっています。

💡 ワード解説：DAG（有向非巡回グラフ）で依存を管理するとは

定理 A を証明するには定理 B と C が要る、B には D が要る。この関係を矢印で結ぶと、枝分かれしながら一方向に流れる図になります。これが DAG（Directed Acyclic Graph）です。循環しない、つまり「A のために B が要り、B のために A が要る」という堂々巡りが起きないことが保証されています。

Prove2Me はこの DAG を全エージェントの共有盤面として持ちました。各エージェントは盤面を見て、次に手をつけるべき未証明のノードを選べます。効いたのは2点で、エージェントの記憶が劣化しても盤面が状態を覚えていること、そして複数エージェントが衝突せずに並列で進めることです。ソフトウェアのビルドシステムが依存関係を解いてから並列コンパイルするのと、発想は同じです。

人間からの数学的な入力は、高レベルな優先度の指示に限られました。Anthropic が実例として挙げているのは、たとえば「Jacobian as a scheme sounds high priority（スキームとしてのヤコビアンは優先度が高そうだ）」といった一言です。

エージェントが互いのレビューを通した

PDF には、11日目にこんな出来事が記録されています。Claude のあるエージェントが、レビュアーとして通した補題が実は偽だったと報告している場面です。

1件、お伝えすべき訂正があります。今朝わたしが（レビュアーとして）通した命題（Cartier 加群の列に関する “model domination” の補題）が、書かれたとおりでは偽だと判明しました。別のエージェントが、わたしのレビューが計算せずに議論で済ませたケースを実際に計算して、反例を見つけたのです。誰かがそれに対する証明を書く前に捕まりました。

——Claude の作業報告より（Anthropic 公開 PDF、筆者訳）

レビューは通ったが、間違っていた。それを捕まえたのは、体制ではなく「計算して確かめる」という行為でした。この構図は §5 でもう一度出てきます。

4. 🧱 本当の価値は「29,511個の部品」のほう

「AI がフェルマーの最終定理を証明した」という見出しは、この成果を正しく伝えていません。証明したのはワイルズとテイラーです。では何が新しいのか。

フェルマーの最終定理は、難しい定理を何段も積み重ねて初めて届く場所にあります。マズールの定理、ラングランズ–タネルの定理、リベットの定理、そして R = T（変形環とヘッケ代数の同型）。これらを全部 Lean に通したということは、その途中の 29,511個の定理が、機械検証済みの部品としてリポジトリに残ったということです。

公開された部品には、Mathlib がまだ持っていなかったものが含まれます。Claude 自身の整理によれば、ヘッケ代数、固有形式に伴うガロア表現、モジュラー曲線とそのヤコビアン、ネロンモデル、有限平坦群スキーム、テイト曲線、そしてテイラー–ワイルズ patching を伴う変形環。現代整数論の道具箱が、機械の検査を通った形で一式そろったわけです。

その積み上がり方は、Anthropic が公開した依存関係の図がそのまま示しています。

フェルマーの最終定理を中心に、モジュラリティ持ち上げ・レベル下げ・志村曲線・マズールの定理・ラングランズ–タネルなどの定理群が放射状に枝分かれして繋がっている依存関係グラフ

形式化された定理の依存関係。中心の Fermat’s Last Theorem に、モジュラリティ持ち上げ（R=T）・レベル下げ（リベット）・志村曲線・ネロンモデル・ラングランズ–タネルなどの枝が集まる（出典: Anthropic の研究記事より）

中心にあるのが最終目標の Fermat’s Last Theorem で、そこへ向かって枝が集まっています。枝の名前は §1 で説明した構造そのものです。Level lowering (Ribet) はフライ曲線をモジュラー形式の世界へ落とすリベットの定理、Modularity lifting, R = T はワイルズが橋を渡るのに使った変形環とヘッケ代数の同型、Langlands–Tunnell はその出発点になる定理。§1 で名前を出したものが、そのまま形式化の単位になっています。

そして注目したいのは中心ではなく、枝のほうです。Taylor–Wiles primes and Selmer groups、Hecke algebras and level raising、Integral models of modular curves、Galois representations at bad primes。これらはフェルマーの最終定理のためだけの道具ではありません。現代の整数論では、まったく別の問題を扱うときにも普通に出てくる対象です。今回それが1つ残らず Lean を通ったので、この図の枝は「証明の経路」であると同時に「使える部品の目録」でもあるという見方ができます。

「Mathlib の5倍」をどう読むか

Anthropic は「約1,300万行は Mathlib の5倍を超える規模」と書いています。数字としては正しい。ただしこれを「5倍の数学がある」と読むのは誤りで、それは Anthropic 自身が脚注で釘を刺しています。

これはひとつには、Mathlib が簡潔でよくレビューされているのに対し、我々の証明は必要よりずっと長い可能性が高いからである。

同じ PDF に収録された Claude 自身の自己評価は、さらに率直です。

それは Mathlib 全体の行数の6倍だが、作られ方の違うものの生の行数であって、「より多くの数学」ではない。

そのうえで Claude は、この証明が Mathlib に取り込まれない理由を自分で列挙しています。以下はいずれも Claude の自己申告値で、Anthropic は PDF の中で「抜粋に含まれる数学的主張を独立に検証してはいない」と断っています。

  • 人間に読めない。 コメントは付いておらず、名前は機械生成。Mathlib が1ファイル1,500行の上限を敷いているのに対し、900を超えるファイルがそれを超えている（Mathlib 側で超えているのは2ファイル）
  • 一般的でない。 ここでの「リベット」「ワイルズ」「マズール」「ラングランズ–タネル」は、いずれもこの議論に必要な強さだけで証明された制限版。Mathlib が欲しいのは一般の主張を一度だけ証明した形
  • 重複だらけ。 カードごとに孤立して証明したため、証明ファイル内の定理のおよそ5件に2件が、他のファイルにある文と一字一句同じ。ある基本補題は300を超えるファイルで再宣言されている
  • 脆く高価。 バイト数の31%が生成された前置き。Lean 4.30 から 4.33 へツールチェーンを上げただけで、29,511ファイル中 7,620件（26%）が変化し、5,672件（19%）は個別に直す必要があった

「では意味がないのか」というと逆です。リポジトリは Apache-2.0 で公開されており、誰でも参照できます。Claude 自身も「入るとすれば、これらの基盤部分を、我々のファイルをコピーではなく参考実装として使う形で、人間主導の Mathlib 開発として進めることだ」と書いています。完成品ではなく、参照できる作業記録として置かれた、というのが正確な位置づけです。

5. ⚖️ 何が確かめられ、何が確かめられていないのか

ここが、この記事でいちばん丁寧に書きたいところです。

flowchart TD A["ワイルズらの人間向け証明
1995年・129ページ"] --> B["解説論文
Darmon-Diamond-Taylor"] B --> C["blueprint
ICL FLT 計画・86ページ"] C --> D["Lean への書き下し
Claude エージェント群"] D --> E["Lean カーネルが検証
公理3つ・sorry なし"] E --> F["comparator
主張の一致を確認"] E --> G["nanoda
別実装のカーネルで再検査"]

確かめられたこと

プラットフォーム上で Proved と表示されることは、まだ端から端までの検査ではありません。Prove2Me は各カードの証明を、子ノードの主張だけを相手に個別コンパイルするからです。そこで Anthropic は最終カードが閉じた翌朝に 29,511 カードすべてをプラットフォームの外で再コンパイルし、さらに翌日、木全体を1つの Lean プロジェクトとしてビルドしました。

  • 公理は3つだけ。 propext / Classical.choice / Quot.sound の3つで、Mathlib 自身が依存しているのと同じものです。sorry（未証明の穴）はどこにも無い。リポジトリの FinalCheck.lean は、この条件が崩れるとビルドが失敗するように書かれています
  • 主張のすり替えが無い。 Lean FRO の comparator が、証明された文が Mathlib だけを import した参照ファイルの文と一字一句同一であること、他の公理が使われていないこと、そして Mathlib を含む証明全体が Lean のカーネルを再度通ることを確認。判定は Your solution is okay!
  • 別実装のカーネルも通った。 Rust で書かれた独立実装の Lean カーネル nanoda 0.4.13 が、同じ環境のエクスポートを受け入れた（Checked 1052234 declarations with no errors）。速度のための小さなパッチが当たっていますが、型付け規則を変えるものは含まれないと明記されています
  • 手順が公開されている。 README には再現手順と実測値が書かれています。ビルドは96並列で5時間32分・メモリのピーク153GB、comparator は約15時間・ピーク230GB。Windows は不可（パスが長すぎる）という但し書きまで付いています

確かめられていないこと

そして、リポジトリの README には次の一文があります。この記事でいちばん引用したかった箇所です。

どのツールにも確かめられないのは、それぞれの中間定理が、その名前の示すとおりの意味かどうかである。それは読者が判断することだ。

機械が保証するのは「最終的な主張が、公理から導かれている」ところまで。途中の29,511個の定理がそれぞれ何を言っているかは、人間が読むしかありません。そのために PROOF-PATH.md があり、そこには名前の付いた古典的定理が実際にはどの強さで証明されているかが、正直に列挙されています。たとえば次のように。

  • マズール：フライ曲線に対する既約性は証明済み。一般の曲線の有理同種写像やねじれに関するマズールの定理は証明していない
  • ラングランズ–タネル：八面体型の場合を明示的な持ち上げつきで証明。可解像を持つ一般の奇な2次元表現の保型性は証明していない
  • リベット：フライ表現に対するレベル下げをトレースの合同として証明。一般のモジュラー mod p 表現に対するリベットの定理は証明していない

さらに、第三者による独立した再実行についても線を引いておきます。comparator も nanoda も第三者が作ったツールですが、今回それらを走らせたのは Anthropic 自身です。Buzzard 氏がレビューして肯定的な評価を出していること、Freek Wiedijk 氏の「100 theorems」一覧が更新されたこと（§6）は確認できましたが、第三者が15時間の再検査を完走したという報告は、本記事の執筆時点では確認できていません。手順は公開されているので、誰でも実行できる状態にはあります。

6. 🤝 Buzzard 氏の5年計画と、この成果の関係

「AI が横から入って持っていった」という受け取り方をする人もいると思います。実際の構図は、もう少し面白い形をしています。

5年計画のほうが先にあった

Imperial College London の Kevin Buzzard 氏は、2024年10月から2029年9月まで、EPSRC の助成（EP/Y022904/1）を受けてフェルマーの最終定理の Lean 形式化を進めています。リポジトリは2023年11月に作られ、証明の道筋はリチャード・テイラー氏との議論で設計され、進捗を記述する blueprint（設計図）は86ページまで育っていました。今回 Claude が形式化フェーズの指針に使ったのは、この blueprint です。

流用はそれだけではありません。Anthropic のリポジトリの NOTICE と ATTRIBUTION.md によれば、106個のファイルが Imperial の FLT プロジェクトと flt-regular プロジェクトから、クレジット付きで取り込まれています（フライパッケージ、ガロア表現、変形理論、patching など）。Anthropic の謝辞も「我々の形式化は、フェルマーの定理の長い歴史と形式数学の発展の、小さな一片にすぎない」と書き、三世紀ぶんの数学者と Lean / Mathlib の数百人の貢献者を並べています。

もうひとつ、この対比は象徴的です。Buzzard 氏はプロジェクトの説明文書に、2023年12月時点でこう書いていました。

現時点（2023年12月）で人類が手にしている AI ツールは、この作業の形式化の部分については実際のところ役に立たない。したがって作業の大半は人間が行うことになる。助成が終わる2029年9月に、どれだけ状況が変わっているかを見るのは興味深いだろう。

答えは2029年ではなく、2026年に来ました。

Buzzard 氏本人は何と言ったか

氏は発表と同日、自身のブログ「Xena Project」に “FLT: Anthropic has beaten me to it”（FLT：Anthropic に先を越された）という記事を書いています。冒頭は「Anthropic、おめでとう！」。そして「私にはもう仕事が無いというのが素朴な反応だろうが、そうではない」と続けます。理由は3つ。

  1. 約束していたゴールが違う。 氏が EPSRC に約束したのは「FLT を1980年代までに知られていた結果に帰着させる」ことであり、全部を証明することではなかった。その意味で今回の成果は約束を超えている
  2. Mathlib への還元が残っている。 現代整数論の基本的な対象を Mathlib へプルリクエストとして送り込む作業は継続中
  3. 人間が読める形が残っている。 「人間が現代的な証明を探索できる動的な文書を作る」という約束があり、氏の見立てでは「Anthropic がそれをやるとは考えにくい。形式化で仕事は終わったと感じるだろうし、そもそも彼らが形式化したのは現代的な証明のほうではない」

3つめは §4 と地続きです。Anthropic が通したのは1990年代の古典的な道筋（ラングランズ–タネルとリベットを経由する道）で、Imperial のプロジェクトが目指しているのは Khare–Wintenberger らの発想を取り込んだより現代的で一般的な道筋です。同じ山に登山道が2本あると考えるのが正確です。

そして、これは読んでいて素直に良いなと思った箇所なのですが、氏は記事を個人的な思い出で締めています。1993年、大学院2年生だった氏はワイルズの3連続講演の1回目に出席し、まったく理解できなかったので残り2回をサボって恋人とアイルランドへ旅行に行った。歴史的瞬間を取り逃したわけです。そして今回も、Anthropic からのメールが届いたとき氏はウェールズの音楽フェスにいて電波が悪く、「End-to-end Lean formalization of Fermat’s Last Theorem」という件名のメールを見て、知らない人からの怪しいメールだと思って無視した。1週間後に約1,000通の未読を片付けていて、ようやく気づいたそうです。

20年越しのベンチマークが埋まった

Radboud University の Freek Wiedijk 氏が管理する「Formalizing 100 Theorems」という一覧があります。数学の有名な定理100個のうちどれが形式化されたかを追跡しているページで、20年以上続いてきました。最後の1つとして残っていたのが、フェルマーの最終定理です。

筆者が2026年9月6日更新のページを確認したところ、該当行は「Lean, not in Mathlib, Anthropic」になり、ページ冒頭の達成率は 100% と表示されています。Buzzard 氏もブログで「これでこの20年来のベンチマークが締めくくられた」と書いています。第三者の一覧に載ったという意味で、これは現時点でもっとも外形的な承認です。

📌 筆者の見方

筆者は数学の専門家ではありません。証明の中身の妥当性は、Buzzard 氏をはじめとする専門家の判断に委ねます。そのうえで、リポジトリの README を読んでいていちばん手が止まったのは、数字ではなく §5 で引いたあの一文でした。どのツールにも確かめられないのは、それぞれの中間定理が、その名前の示すとおりの意味かどうかである。

これは筆者が電子工作で毎回踏んでいる線と、まったく同じものだと感じました。ESP32 のファームがビルドを通っても、それは「書いたコードが文法的に正しい」ことしか意味しません。センサーの軸を1本取り違えていれば、コンパイラは何も言わずに通します。基板でも同じで、KiCad の DRC が緑になるのは「引いた配線がルールに違反していない」ことの保証であって、「その回路が意図どおり動く」ことの保証ではない。今回の Lean カーネルは、DRC よりはるかに強い保証を与えています。最終的な主張が Mathlib の FLT と一字一句同じであることまで機械が確かめている。それでも、29,511個の中間定理が何を言っているかは人間が読むしかない。保証の強さが上がっても、保証の外側そのものは消えない。そこは自分の作業と地続きだと受け止めました。

もうひとつ、これは意見ですが、公開資料でいちばん実感を持って読めたのは限界の側の数字でした。ツールチェーンを Lean 4.30 から 4.33 へ上げただけで26%のファイルが変化し、19%は個別に直す必要があった、というくだりです。筆者は ESP-IDF のバージョンを上げるたびに同じ目に遭っています。前の版で動いていたプロジェクトが、フレームワークを一段上げただけでビルドを通らなくなる。「一度動いた」と「これからも動く」の間には距離がある。それは350年の難問を機械検証で閉じたコードでも変わらないのだと分かったのが、今回いちばん腑に落ちた点でした。

そして率直に言えば、この件でいちばん気持ちが良かったのは Buzzard 氏のブログでした。先を越された当人が、まずおめでとうと書き、次に自分の残りの仕事を数え直し、最後に30年前に講演をサボった話で締める。技術が前に進んだ日の記録として、これ以上に健全な文章はなかなか無いと思いました。

まとめ

  • 2026年9月4日、Anthropic が Claude によるフェルマーの最終定理の Lean 形式化を公開した。期間11日・Lean 約1,300万行・29,511定理・出力トークン約60億（いずれも Anthropic 発表値）
  • 主張されているのは新しい数学ではなく、検証である。Anthropic 自身が「今回あたらしいのは検証のほうだ」と明記している
  • Lean のカーネルに加え、第三者製の comparator と nanoda（Rust による独立実装のカーネル）が通った。依存する公理は Mathlib と同じ3つのみ、sorry は無い。ただしこれらを走らせたのは Anthropic 自身であり、第三者による再実行の完走報告は執筆時点で確認できていない
  • 価値は「29,511個の定理が再利用可能な部品として Apache-2.0 で公開された」こと。ただし Anthropic も Claude 自身も、このコードは現状のままでは Mathlib に入らない（読めない・一般的でない・重複が多い・脆い）と明言している
  • 土台には Kevin Buzzard 氏が2024年から進めてきた Imperial College London の FLT プロジェクトがあり、86ページの blueprint が指針に、106ファイルがクレジット付きで流用された。氏本人がレビューし、ブログで祝意を示したうえで「自分の仕事は残っている」と3点を挙げている
  • Freek Wiedijk 氏の「Formalizing 100 Theorems」の最後の1問が埋まり、達成率が100%になった

よくある質問（FAQ）

Q1. AI がフェルマーの最終定理を証明したのですか？

いいえ。証明したのは1995年のアンドリュー・ワイルズ（とリチャード・テイラー）です。今回 Claude が行ったのは、その証明を Lean という言語に書き下し、機械が全ステップを検査できる形にしたことです。Anthropic 自身も、新しい数学が生まれたわけではないと明記しています。

Q2. すでに証明済みなら、形式化に意味はあるのですか？

あります。人間の査読は「自明」「同様に」といった省略を読者が補って成立しますが、Lean はそれを許さず、公理まで遡って全ステップを機械が検証します。実際、ワイルズの証明にも1993年に穴が見つかっています。加えて今回は副産物として、ヘッケ代数やガロア表現など現代整数論の道具が29,511個の検証済み部品として公開されました。

Q3. 「Mathlib の5倍の規模」はすごいことですか？

規模としては事実ですが、5倍の数学があるという意味ではありません。Anthropic は脚注で「Mathlib が簡潔でよくレビューされているのに対し、我々の証明は必要よりずっと長い可能性が高い」と断っています。Claude 自身も「作られ方の違うものの生の行数であって、より多くの数学ではない」と自己評価しています。

Q4. このコードは Mathlib に取り込まれるのですか？

現状のままでは取り込まれません。Claude 自身が理由を挙げています。コメントが無く名前が機械生成で人間に読めないこと、900を超えるファイルが Mathlib の1,500行上限を超えていること、定理の5件に2件が他ファイルと重複していること、そしてツールチェーンの更新に対して脆いこと。取り込まれるとすれば、基盤部分を人間主導で書き直すときの参考実装として、という位置づけです。

Q5. Buzzard 氏のプロジェクトは無駄になったのですか？

なっていません。Anthropic が通したのは1990年代の古典的な道筋で、Imperial のプロジェクトが目指しているのは Khare–Wintenberger らの発想を取り込んだより現代的で一般的な道筋です。さらに氏の助成の約束には「Mathlib へ現代整数論の対象を送り込むこと」「人間が証明を探索できる動的な文書を作ること」が含まれており、いずれも今回の成果では埋まりません。氏本人がブログでそう説明しています。

Q6. 第三者は検証したのですか？

部分的にです。Buzzard 氏が完成した証明をレビューし、肯定的な評価を出しています。また Freek Wiedijk 氏の「Formalizing 100 Theorems」がフェルマーの最終定理を「形式化済み（Anthropic）」として掲載し、達成率が100%になりました。一方、comparator と nanoda は第三者製のツールですが走らせたのは Anthropic 自身で、第三者が約15時間の再検査を完走したという報告は執筆時点では確認できていません。手順は README に公開されています。

Q7. 自分の環境で確かめられますか？

手順は公開されていますが、要求されるリソースが個人の環境の範囲を超えています。README の実測値では、ビルドが96並列で5時間32分・メモリのピーク153GB・ディスク約67GB（加えて中間の C ファイルが約220GB）、comparator が約15時間・ピーク230GB。Windows では動きません（パスが長すぎるため Linux か macOS が必要）。個人で試すなら、まず html/ フォルダ（約390MB）をブラウザで開いて、定理ごとのページと依存グラフを眺めるところからになります。

Q8. なぜ Lean だったのですか？ 他の証明支援系ではだめですか？

Rocq（旧 Coq）、Isabelle、Agda など他の証明支援系もあります。Lean が選ばれる理由は主に Mathlib の存在です。数百人の数学者が積み上げた現代数学のライブラリがあるので、ゼロから始めずに済みます。Buzzard 氏も、Liquid Tensor Experiment など先行プロジェクトの実績から Lean を選んだとプロジェクト文書に書いています。

関連記事

参考