証明が正しいかどうかを人間が確かめるのに、何年もかかることがある。9 月 4 日、Anthropic は Claude が 11 日でフェルマーの最終定理の証明を Lean で形式化し、機械検証を通したと発表した。13,000,000 行のコード、証明された定理は 30,300 件。
ここで起きたのは「AI が難問を解いた」ではない。証明の筋道は 1990 年代に人間が作り、その後に簡略化されている。機械に回ったのは、それを一行の隙もない形に書き下ろし、正しさを確かめる側の作業だ。
そして確かめる作業のコストが崩れると、私たちが何かを「確かめられた」と言うときの根拠の置き場所も動く。この記事では、確かめられる範囲を先に敷いたうえで、その線がどこまで手元に降りてきて、どこから先は降りてこないのかを見ていく。
まず、確かめられることから
公開されたのは論文ではなく、動かせる成果物だ。GitHub の anthropics/fermats-last-theorem に、Lean 4 (v4.33.1) のコードが Apache License 2.0 で置かれている。
定理の記述そのものは短い。自然数 n が 3 以上のとき、正の自然数 a, b, c について a の n 乗と b の n 乗を足したものが c の n 乗に等しくなることはない——これが Lean の言葉で数行に書かれ、その数行が証明されている。
大事なのは、その証明が何に依存しているかが機械的に確定していることだ。リポジトリによれば、依存する公理は Lean 標準の 3 つ (propext / Classical.choice / Quot.sound) だけで、sorry (未証明の穴を許す記法) も追加の公理も、実行時に外部へ逃がすような記法も使われていない。規模は 60,475 モジュール、定理 29,511 件。
しかも検証は Lean 本体だけで終わっていない。別実装の検証器が 2 つ通されている。ひとつは leanprover/comparator で、証明された文が意図した定理の記述と本当に一致しているかを独立に確認する。もうひとつは nanoda 0.4.13 という Rust 製の独立したカーネルで、リポジトリには 1,052,234 個の宣言をエラーなく検査した、と記録されている。
ここまでが、誰が読んでも同じ手順で追える範囲だ。
11 日の中身
発表によれば、作業は Claude のエージェントが複数協調する形で進み、人間の関与は「ときどきの高レベルな指示」にとどまった。出力は約 60 億トークン。証明された定理 30,300 件のうち、最終的な証明に使われたのが 29,500 件 (リポジトリ側の集計は 29,511 件)。
数字のなかで、いちばん誠実なのは失敗の扱いだと思う。最終的な証明に残った定型外の行のうち、約 7% は失敗した試行から来ている。うまくいかなかった経路が丸ごと捨てられず、部品として残ったということだ。初期のエージェントは「プロジェクトの状態をすぐに見失い、うまく協調しなくなった」とも書かれている。転機になったのは、Prove2Me という共同作業用のオープンな基盤を与えたことだった。
完成は 8 月 17〜18 日、公開は 9 月 4 日。
ゼロから出てきたわけではない
ここは範囲を絞っておきたい。
フェルマーの最終定理の形式化は、2024 年 4 月から Imperial College London の Kevin Buzzard 氏が率いるコミュニティプロジェクトとして進んでいる。英 EPSRC による最初の 5 年間の資金がついた企画で、その期間内の目標は完全な形式化ではなく、「FLT を、1980 年代末までに数学者に知られていた主張に還元する」ことだった。Buzzard 氏自身、開始時に「このプロジェクトがどれだけかかるか、まったく見当がつかない」と書いている。
今回の証明は、Wiles の原証明ではなく、Darmon・Diamond・Taylor による簡略化された解説の筋道に沿っている。そしてリポジトリのうち 106 ファイルは Imperial のプロジェクトと flt-regular 由来の素材を含み、23 ファイルは Mathlib の補題を再現したものだ。
だから「AI が単独で 11 日でフェルマーを片づけた」という要約は、少し広すぎる。正確には、数年がかりで積まれてきた形式化の土台と、人間が先に簡略化し終えていた証明の筋道の上で、書き下ろしの作業が 11 日で終わった。それでも十分に大きな出来事だが、大きさの中身が違う。
「機械が確かめた」の範囲は、思ったより狭い
カーネルが保証しているのは「この記述が、この公理から導ける」という一点だ。それ以上でも以下でもない。
人間に読めるかどうかは、別の問題として残っている。リポジトリは名前が機械生成であることを明示していて、ソースは可読性より検査可能性を優先している、と書かれている。13,000,000 行は Mathlib の 5 倍を超える大きさで、発表自身が「必要よりずっと長い」と認めている。形式化された証明は、人間が読んで理解できる説明の代わりになるものではない——その線も発表のなかで引かれている。
Buzzard 氏のコメントも、称賛と限定が同居している。「数学の公理以外に何の仮定も置かずにフェルマーの最終定理を証明している」と評価したうえで、現代数学の文献を自動で形式化することへ向けた一歩、という位置づけをしている。証明が読めるようになった、とは言っていない。
そしてこれは検証であって、発見ではない。新しい数学が生まれたわけではない。
確かめる側に回るコスト
ライセンスの上では、誰でも確かめられる。Apache 2.0 で、手順もリポジトリに書いてある。ただし手元の計算資源の話になると、様子が変わる。
リポジトリが挙げているビルド要件はこうだ。並列ジョブ 1 本あたり約 5GB、フルビルドのピークで 153GB のメモリ。ディスクは作業領域に約 67GB、生成される C ファイルに約 220GB。96 並列で約 5.5 時間かかる。comparator による独立検証はさらに約 15 時間、nanoda は約 30 分 (エクスポートの時間を除く)。OS は Linux か macOS で、Windows はパスが長すぎて通らない。
つまり「自分で全部を再現する」は、普通のノート PC の外側にある。
一方で、手元でできることが何もないわけでもない。リポジトリには証明の道筋を Lean の定理名で追える PROOF-PATH.md があり、ネットにつながっていなくても開ける HTML 版 (約 390MB) も同梱されている。読むことと、全部を走らせ直すことでは、必要なものが桁でちがう。
このギャップは、これから何度も出会う形だと思う。検証可能であることと、自分が検証できることは、同じではない。
私たちは、どう向き合うか
「機械が確かめた」と言われたとき、手元で確認できることは意外にある。今回の件は、その項目がきれいに揃っている例として使いやすい。
【1】何を仮定しているか。今回なら「Lean 標準の 3 公理だけ」「未証明の穴なし」。何を前提にしたのかが書かれていない主張は、確かめられたと呼びにくい。
【2】誰が独立に確かめたか。同じ実装で 2 回通しても、独立ではない。今回は別実装のカーネルが通されていて、そこが効いている。
【3】自分が再現するには何が要るか。ライセンス、手順、計算資源。この 3 つのうちどれかが欠けていれば、「再現できます」は言葉だけになる。今回は 3 つとも揃っているが、3 つ目の値段が高い。
そのうえで、確かめないという選択肢も同じ卓の上にある。全部を自分で検証しながら生きるのは、時間の側から見て不可能だ。だからこの 3 項目は「必ずやること」ではなく、どこを信じてどこを保留するかを自分で決めるための目盛りとして持っておくほうが、実用に耐えると思う。
目盛りは数学の外でも使える。「測った」「検査を通った」「監査済み」と言われる場面はいくらでもある。そのたびに、仮定は書かれているか・確かめたのは何者か・自分が追試するには何が要るか、と並べてみる。答えが出ないこともあるが、答えが出ないと分かること自体が判断材料になる。
見ておきたい点
【1】Imperial College のコミュニティプロジェクトが、この成果物をどう扱うか。取り込むのか、別の道を進むのか
【2】自動形式化が、検証の側から発見の側へ動くか。今回は既に知られた証明の書き下ろしで、新しい数学は出ていない
【3】この規模の成果物が、153GB のメモリを持たない環境でも検査できるようになるか。独立カーネルの軽さ (nanoda で約 30 分) は、その方向のヒントに見える
【4】数学の外で、同じ厳しさの検証成果物が出てくるか。出てこないなら、その分野の「確かめた」は当分ラベルのままだ
あなたが「確かめた」と言われて信じるとき、確かめているのは中身のほうだろうか、それとも確かめたと言った誰かのほうだろうか？
