Claude がフェルマーの最終定理を11日で形式化 — 1300万行 Lean と「検証器がある領域」の意味

はじめに

Anthropic が 9 月 4 日、Claude のエージェント群が フェルマーの最終定理（FLT）を Lean 4 で完全に形式化した と発表した。11 日間、ほぼ自律で、約 1300 万行の Lean コードと 30,300 個の中間定理を生成し、sorry（未証明のプレースホルダ）ゼロで Lean カーネルを通した。人間の数学的入力は「ヤコビアンをスキームとして扱うのを優先しろ」といった断片的な指示に限られている。

この手のニュースは「AI がついに数学を解いた」という見出しで消費されがちだが、実際に起きたことはもう少し具体的で、そしてエンジニアにとって示唆的だ。FLT 形式化プロジェクトを 2024 年から率いてきた Imperial College London の Kevin Buzzard は、この成果を「並外れた自動形式化の達成」と評価しつつ、同時に 「数学については何も教えてくれない」 とも言っている。この両方が同時に正しい、というのがこの件の面白いところだ。

この記事では、(1) 実際に何が生成され、どう検証されたのか、(2) 数十体のエージェントを 11 日間協調させた Prove2Me という仕組み、(3) Buzzard の批判が指し示すボトルネックの移動、を順に見ていく。数学の話ではなく、「機械検証器のある領域で AI に物量を投げると何が起きるか」 の話として読んでほしい。

何が生成され、どう検証されたのか

まず数字を並べる。出典は Anthropic の発表と、公開されている GitHub リポジトリの README だ。

項目	値
生成された Lean コード	約 1300 万行（Buzzard の実測では 13.4M 行）
証明された定理	30,300 個（最終証明で使用されたのは 29,500 個）
モジュール数	60,475
定義モジュール	1,450
所要時間	11 日
出力トークン	約 60 億
使用モデル	「Claude Fable 5.1 に概ね相当する」社内の汎用研究モデル
Lean バージョン	4.33.1
ライセンス	Apache-2.0

比較対象として、Lean の標準数学ライブラリである Mathlib は約 260 万行。今回の証明単体で Mathlib の 5 倍以上という規模になっている。

検証は三重に行われている。ここが「AI が証明したと主張している」との決定的な違いなので、丁寧に見ておく価値がある。

Lean カーネルによるビルド: 60,475 モジュールすべてが Lean 4.33.1 でコンパイル・型検査を通る。デフォルトのビルドターゲット FinalCheck.lean が、sorry も追加公理も存在しないことを保証する。使われている公理は Lean 標準の 3 つ（propext、Classical.choice、Quot.sound）のみで、これは #guard_msgs で機械的に強制されている。native_decide、unsafe、extern、partial def といった逃げ道も禁止されている。
コンパレータ: 証明した命題が本当に FLT なのかを確認する工程。Mathlib の FLT の記述と突き合わせ、Challenge.lean に対して再度カーネルを通す。約 15 時間かかる。
nanoda: Lean とは独立に Rust で書かれた第三者製のカーネル実装。1,052,234 個の宣言をエラーなく検査した。Lean 本体にバグがあった場合の保険になる。

つまり「AI の出力を人間が読んで納得した」のではなく、AI の出力を機械が独立に 2 系統で検査した。手元で再現することもできて、96 並列で lake build に約 5.5 時間、ディスク 67GB、ジョブあたり 5GB のメモリが要る。実際 Buzzard は自分でコンパイルし、標準のチェックツールを走らせた上で上記の評価を出している。

なお、正直な注意書きも README に載っている。定理名は機械生成されたもので、数学的な意味を反映していない。また Mathlib との照合が行われたのは「命題文そのもの」だけで、その下位にある定義群は Mathlib 内部との一致ではなくカーネルを信頼する形になっている。

Prove2Me — 数十体のエージェントを 11 日間協調させた仕組み

エンジニアとして一番持ち帰りやすいのはここだと思う。Anthropic は最初、素朴にエージェントを投入して失敗している。発表にはこう書かれている。エージェントは「プロジェクトの状態をすぐに見失い、効果的に協調しなくなった」。

長時間のマルチエージェント運用をやったことがあれば、この失敗モードには見覚えがあるはずだ。コンテキストウィンドウは有限で、数日単位のタスクでは「今どこまで進んだか」がコンテキストから溢れる。溢れた瞬間、エージェントは既に終わった仕事をやり直したり、他のエージェントが担当している箇所に重複して着手したりする。

これを解いたのが、Tianyi Peng と Columbia 大の共同研究者が設計した Prove2Me というプラットフォームだ。仕組みは三点に整理できる。

1. DAG による状態の外部化

定理の言明を有向非巡回グラフ（DAG）として保持する。定理 A の証明に定理 B と C が必要なら、それが辺として表現される。エージェントは「次に何を証明すべきか」をこのグラフから読む。プロジェクトの状態がエージェントのコンテキストではなくグラフという外部ストアに載っているので、コンテキストが飛んでも進捗は失われない。Anthropic はこれを「メモリ劣化を緩和し、複数エージェントの並列作業を可能にした」と説明している。

依存関係のグラフを持つのは、そもそも数学の証明が持つ構造をそのまま写しただけとも言える。だが同じことは、ソフトウェアのタスク分解でも成立する。「この関数を実装するには先にこの型定義が要る」という関係は DAG だ。エージェントに渡すべきは TODO リストではなく依存グラフだ、というのがこの設計の主張になっている。

2. 言明と証明のファイル分離

定理の言明と証明を別ファイルに分け、リンクを独立に維持する。Lean のコンパイル時間とリソース消費を減らすためだ。あるエージェントが定理 B の証明を書き換えても、定理 A の側は B の言明にしか依存していないので再コンパイルが要らない。

これはインターフェースと実装の分離そのもので、目的も同じ——再ビルドの伝播を止めること。1300 万行という規模で、しかも数十体が並行で書き換える環境では、これがないとフィードバックループが回らなくなる。

3. 自然言語での検索と再利用

各定理に自然言語の説明を付与し、「こういう性質を示す補題はもうあるか」を検索できるようにした。29,500 個の定理を抱えるプロジェクトで、既存の補題を見つけられないエージェントは同じものを何度も証明することになる。名前が機械生成で数学的意味を持たない以上、名前で引くことはできない。だから説明文で引く。

この 3 点は、要するに 「数十体の LLM エージェントを長期間走らせるためのインフラ」 であって、数学固有のものはほとんどない。Anthropic 側の記述でも「Prove2Me と Claude Code ベースのマルチエージェントハーネス」で完走した、とされている。

ついでに書いておくと、Prove2Me 導入前の失敗した試行も無駄にはなっていない。発表によれば、それらの失敗が最終証明の非ボイラープレート行の約 7% に寄与している。

Buzzard の評価 — 「数学については何も教えてくれない」

ここからが本題かもしれない。Kevin Buzzard は 2024 年から EPSRC の助成を受けて FLT 形式化を進めてきた当事者で、当初の計画文書は 86 ページ、完了までに数年かかると見込まれていた。その彼が、Anthropic のコードを自分でコンパイルした上で述べた評価は、賞賛と留保が明確に分かれている。

賞賛の側はこうだ。「AI の群れが、数千ページの文献をエンドツーエンドで 11 日で形式化した」。そして FLT の自動形式化が可能なら「現代数学の文献の自動形式化に向けて大きな一歩を踏み出したことになる」——既存の数学的コーパスの誤りを洗い出し、査読者の負担を軽くするツールにつながる、と。

留保の側は三点ある。

第一に、数学的な新規性はない。 この形式化は Darmon・Diamond・Taylor による 1995 年の Wiles 証明の解説を忠実に追っており、Buzzard 自身が形式化してきた現代的な経路ではない。彼の言葉では「初期の文献を忠実に追っているだけで、何も足していない」。Wiles の証明が正しい確率を彼は 99.9%、整数論コミュニティは 100% と見ていた。つまり 形式化は「知らなかったこと」を明らかにしたわけではない。Anthropic 自身も、新しい数学を生んだ Riemann 予想周りの AI 研究とは違い「今回新しいのは検証の側だ」と位置づけている。

第二に、コードの質。 13.4M 行は Mathlib の 2.6M 行に対して 5 倍以上で、96 コアのマシンでコンパイルに Mathlib の約 20 倍かかる。Anthropic 自身も「必要以上にずっと長い可能性が高い」と認めている。動くが、保守可能な形ではない。

第三に、そしてこれが一番効く指摘だが、ボトルネックが移動しただけかもしれない。 Buzzard は、この 1300 万行は現状 Mathlib には一行も入れられない、と指摘している。Mathlib は AI 生成コードのレビューを受け付けていないからだ。証明を書くコストは劇的に下がったが、それが読まれて共有資産に取り込まれるプロセスは詰まったままになる。形式化はまさにその「読む負担」を減らすための技術だったはずなのに、である。

彼は金銭面の観察も残している。自分は 5 年間で 100 万ポンドの助成を得て取り組んでいるが、Anthropic は 11 日で終えた——「向こうがもっと使ったのかどうかは分からないが」。60 億出力トークンという数字がその答えの一部だろう。

エンジニアにとって何が変わるか

この事例から実務に持ち帰れる論点は、少なくとも三つある。

1. 「検証器があるか」が AI の物量が効くかどうかの分水嶺になった

Lean が特殊なのは、生成物の正しさを 人間のレビューなしに機械が判定できる ことだ。エージェントは間違った証明を書いてもいい。カーネルが弾くので、次の試行に進むだけだ。誤りが出力の外に漏れない領域では、失敗コストがほぼゼロになり、そこに 60 億トークンを注ぐ戦略が成立する。

裏返すと、検証器のない領域では同じ戦略は成立しない。通常の業務コードで機械が判定できるのは型検査とテストが通ることまでで、「仕様通りか」は判定できない。この非対称性が、今回の成果がそのまま一般のソフトウェア開発に転写できない理由になっている。

実務的な問いはこうなる——自分のプロジェクトで、AI の出力に対する「カーネル」の役割を果たすものは何か。型システムか、プロパティベーステストか、契約か、本番相当データでのゴールデンテストか。それが弱いほど、AI に物量を投げる戦略の期待値は下がる。エージェントを速くすることより、判定器を強くすることに投資したほうが効く局面は多い。

2. 長期マルチエージェントの設計は「状態の外部化」に尽きる

Prove2Me が解いた問題——エージェントがプロジェクトの状態を見失う——は、規模を問わず起きる。対策も規模を問わず同じで、進捗をコンテキストではなく外部の構造に置く。DAG でなくてもいい。依存関係を明示したタスクファイル、ステータス付きの Issue、ロック付きの作業台帳。要は次にやるべきことがコンテキストの記憶ではなく読み取りで決まる形にする。

そして再利用のための検索を用意する。生成物が増えるほど、既にあるものを見つけられないエージェントは重複を作る。名前規約が効かない場面では、説明文による検索が現実的な代替になる。

3. レビューがボトルネックになる未来はもう来ている

Mathlib が AI 生成コードを受け入れないのは、頑迷だからではない。レビューできない量が届くからだ。同じ構造は普通のリポジトリでも起きる。エージェントが 1 日に出す差分の量が、チームが読める量を超えた瞬間、ボトルネックは生成から取り込みに移る。

このとき効くのは「読まなくても信頼できる根拠」を積むことで、それはテスト・型・静的検査・独立した第二の検証系といった、今回 Anthropic が三重に積み上げたものと同じ系統の話になる。1300 万行を誰も通読していないのに信頼できるのは、nanoda という独立実装が別経路で同じ結論に達したからだ。

まとめ

Claude のエージェント群が Lean 4 で FLT を形式化。11 日・約 1300 万行・29,500 定理・約 60 億出力トークン。sorry なし、Lean 標準の 3 公理のみ
検証は三重（Lean カーネルビルド / Mathlib 命題との照合 / 独立実装 nanoda による 105 万宣言の検査）。コードは Apache-2.0 で公開され、手元で再現できる
成功の鍵は Prove2Me — DAG による状態の外部化、言明と証明のファイル分離、自然言語検索による再利用。素朴なエージェント投入は「状態を見失って」失敗している
Buzzard の評価は二面的。「並外れた自動形式化」である一方、数学的新規性はなく、Mathlib の 5 倍の行数・20 倍のコンパイル時間で、AI 生成ゆえ Mathlib には取り込めない
効いたのは 機械検証器の存在。失敗コストがゼロの領域だから物量が通った

新技術の導入判断でいつも問われるのは「うちで同じことができるか」だが、この件に関しては問いを一段ずらしたほうがいい。うちのコードベースにおける Lean カーネルは何か。それが答えられる領域から、AI に物量を投げる戦略は現実的になる。