検証されたが読まれない証明 — フェルマーの最終定理の形式化が残した問い
検証されたが読まれない証明 — フェルマーの最終定理の形式化が残した問い
機械が証明を機械の検証できる形で書き切れるとしたら、数学において「理解」とは何として残るのか。Lean のカーネルが通した1,300万行は知識なのか、知識の影なのか。
導入
2026年9月4日、Anthropic がフェルマーの最終定理（Fermat’s Last Theorem、以下 FLT）の初のエンドツーエンドな計算機検証済み証明を公開した。主張は簡潔である。Claude が11日間おおむね自律的に作業し、Lean で証明を書き上げた。その過程で1,300万行の Lean コードを書き、30,300個の定理を証明し、うち29,500個が最終的な証明に使われた。a^n + b^n = c^n を満たす正の整数解が n > 2 では存在しない、という1637年の余白の走り書きに始まり、1995年のアンドリュー・ワイルズの129ページの論文で閉じた問題である。
Hacker News ではこの発表が490点を超え、その日の首位になった。ところがスレッド上部で最も強く薦められたリンクは Anthropic の発表文ではなかった。あるユーザーは、インペリアル・カレッジ・ロンドンで FLT 形式化プロジェクトを率いるケビン・バザード（Kevin Buzzard）のブログを併読するよう勧め、その記事が「この達成が何を意味し、何を意味しないか」の文脈を与えてくれると書いた（@lalitmaganti）。HN の運営者はそのリンクを投稿上部の注記に加え、いっそそちらを代表リンクにしたいとまで述べている（@dang）。
この反応の構造が事件の性格を語っている。発表文だけを読めば何が証明されたかは分かるが、何が証明されていないか、その証明がどういう種類の知なのかは分からない。
11日と1,300万行、そして当事者自身が確かめたこと
まず事実関係を整理する。Anthropic によれば、証明はワイルズの議論を簡略化したダルモン・ダイアモンド・テイラー（Darmon–Diamond–Taylor）の1995年の解説に沿っている。実行はコロンビア大学の Tianyi Peng らが設計した Prove2Me という公開協働プラットフォーム上で行われた。このプラットフォームは定理の命題を有向非巡回グラフ（DAG）として保持し、エージェントが次に何を証明すべきか判断できるようにする。さらに命題と証明を別ファイルに分離して Lean のコンパイルを高速化し、各命題に自然言語の説明を付けて検索と再利用を可能にする。その上に Claude Code ベースのマルチエージェント・ハーネスが載り、数十のエージェントが協働した。消費した出力トークンは約60億、使われたのは「Claude Fable 5.1 におおむね相当する社内の汎用研究モデル」である。
注目すべきは失敗の記録も残っていることだ。初期の試行は失敗した。エージェントがプロジェクトの状態を見失い、協働が崩れたからである。その失敗した作業が最終的な証明の非ボイラープレート行のおよそ7%を占めている。人間による数学的介入は「時折の高レベルな指示」にとどまったと発表文は記す。加えて、コミュニティが用意した86ページのブループリント、共有ライブラリ Mathlib、そしてバザードのインペリアル・プロジェクトと flt-regular プロジェクトの断片が出発点として使われた。Anthropic は謝辞でこれを明記している。
決定的なのはバザード本人による検証である。彼はブログで、コードベースを自分でコンパイルし comparator を走らせたうえで「問題なく通る」と書いた。規模は1,340万行を超え、96コアのマシンで Lean の数学ライブラリの20倍近いコンパイル時間を要する。500GB のメモリを積んだマシンでもファイル間の移動がもたつくため、実際の探索は Anthropic が併せて提供した HTML 文書で行ったという。
同時に彼は範囲を正確に切り分けている。このリポジトリが展開するのはフォンテーヌ理論と、マズールのアイゼンシュタイン・イデアルに関する仕事であり、その結果として直接扱われるのは素数指数 p ≥ 17 である。では残りはどうなるのか。奇数の正則素数に対する FLT は Best–Birkbeck–Brasca–Rodriguez によってすでに形式化されており、最小の非正則素数は37である。したがって17未満の奇素数はすべて正則素数であり、先行研究が覆う。バザードの言葉では「so it’s all good」、すなわち隙間はない。Anthropic の「FLT 全体が証明された」という主張は、この二つの筋を合わせて初めて成立する。機械が新たに書いたのは p ≥ 17 の経路であり、小さい指数は人間が数年前に形式化しておいた結果に依っている。
そしてバザードは、この仕事の数学的な意味を自ら削ぎ落とす。「数学的には、Anthropic のこの仕事は本質的に何も教えてくれない」と彼は書いた。自分は FLT の証明が正しいと99.9%確信していたし、数論コミュニティの大半は100%確信している。形式化は初期の文献を忠実になぞっただけで、何も付け加えていない。HN では「バザードのグループが先を越された」という反応がトップのコメントに上がったが（@kdavis）、当の本人はその枠組みを退ける。彼は EPSRC の助成でほかに二つを約束していると述べる。一つは現代数論の基本的な対象を Mathlib へプルリクエストとして入れること、もう一つは「人間が現代的な証明を探索できる動的な文書」を作ることである。後者を Anthropic がやるとは思えない、と彼は見る。そもそも彼らが形式化したのは現代的な証明ですらない。
信頼の根はカーネルではなく命題の記述にある
この一件が突きつける認識論上の問いは「1,300万行を信じられるのか」である。HN のあるユーザーはまさにそう問うた。AI が生成した1,300万行の Lean コードが正しいと確信する根拠はあるのか、我々は一つの検証問題を別の検証問題に置き換えただけではないのか（@skobes）。
答えの半分は形式証明の構造にある。Lean のカーネルが証明を通したということは、「この証明項がこの命題という型を持つ」という確認である。すなわちその命題が、与えられた定義と公理から導かれるという保証だ。途中の1,300万行がどれほど冗長でも、どれほど奇妙な迂回をしていても、カーネルを通ったのなら論理の連結は切れていない。別のユーザーがまとめたとおりである。定理証明支援系の利点は途中の行を読まなくてよいことであり、人間が確かめるべきは、ゴールの命題が自分の考えているその命題と実際に一致するかどうか、その一点だけだ（@fwip）。
だから信頼の根はカーネルではなく命題の記述部にある。形式的な文は定義の組み合わせであり、定義が微妙にずれていれば、真の文を証明しながら意図した定理とは別のものを証明したことになる。スレッドでいわゆる「ジャンク定理（junk theorem）」が話題に上ったのはそのためだ（@stratos123）。あるユーザーはその性格を正確に要約している。ジャンク定理は偽ではなく真である。ただし数学をどう符号化したかに敏感であり、真でありながら概念的には無意味になりうる。フォン・ノイマン順序数で自然数を定義すると自然数同士の共通部分が最小値と一致するが、この文は真であっても自然数の考え方としては完全に誤っている（@mswphd）。
FLT の場合、この軸は実際に閉じている。Anthropic は証明が Lean の標準的な三つの公理しか使わず、comparator によって定理の命題が Mathlib 自身の FLT の命題と一致することを確認したと述べた。そしてバザードが自らの手で同じ検査を再実行した。命題の忠実性は、発表者の自己申告ではなく外部の専門家による再実行で確かめられている。ここははっきりさせておく価値がある。「AI がもっともらしい何かを証明したと言い張っている」という懐疑は、この事例には当てはまらない。
閉じていない軸はその下にある。カーネル自体の健全性である。スレッドでは、Lean にもバグがあったし他の証明支援系も同様であること、そして証明支援系がうまく機能する理由の一つは、それが人間の意図を込めた入力を前提に作られていることが指摘された。1,300万行の中に何が入っていて、それが Lean のバグに触れないかどうかを我々は知らない、というわけである（@Jaxan）。より鋭い整理も出た。人間の数学者が Lean の証明を書くとき、カーネルのバグを使ってごまかす動機も能力もほとんどない。だが AI は過去に目標達成に対して「野心的」であったし、Lean のバグを見つけて悪用する術も知っている。同じカーネルを通っていても、著者が誰かによって信頼の増減の向きが変わる（@3192987）。実際にフロンティアモデルを動員して Lean のカーネルとランタイムの健全性の問題を洗い出し、修正してきた作業があるという反論も併せて上がった（@kingstnap）。さらに、この証明のかなりの部分が Mathlib にない新しいコードだという指摘もあった。既存の資産の上に積んだのではなく相当量を新たに合成したということであり、それだけ未レビューの表面が広い（@throw567643u8）。この懸念は抽象論ではない。一か月ほど前に Lean カーネルのバグが AI によって悪用され偽の命題が証明された事例があったという指摘があり、同じユーザーは、人間がレビューしていない1,300万行が FLT についての我々の理解に決着をつけるわけではないとまとめている。その中のどこかでカーネルのバグが使われた可能性は明確に残るからだ（@mswphd）。
反対側の整理も同じスレッドにあった。単純なチェッカーがあり、それが正しいと多くの人が同意し、定理の形式化がその定理を正確に定義していることにも多くの人が同意するなら、誰も読んでいない1,300万行はそれで十分だという。検証すべきは定理の形式化とチェッカーの健全性の二つだけで、証明の本文を読む必要はない（@stabbles）。二つの立場の差は事実判断というより、どこまでリスクを引き受けるかの問題に近い。確かなのは、形式証明が動かすのは信頼の総量ではなく信頼のかかる地点だということである。129ページの論文を読み切った少数の専門家にかかっていた信頼が、いまやカーネルのコードと命題一行にかかる。
最後に残るのが理解可能性だ。検証可能性と理解可能性は別の目標である。あるユーザーは、幾何代数やリー理論を長く学んできたにもかかわらず自分の脳が Lean を読めないと打ち明けた。Lean 4 以前から何度も入門を試みたが、Lean の証明の書かれ方が自分の証明の考え方と噛み合わず、Isabelle のほうが自然に感じられたという。証明の未来が Lean 一色になるのは惜しい、と彼は付け加えた（@rao-v）。別のコメントでは「人間が1,300万行を検査したのか、この種の作業の品質保証はどうするのか」という問いが出て（@prometheus1992）、また別のユーザーはすかさず「では /simplify を走らせよう、半分にできるのか」と応じた（@stabbles）。Anthropic 自身も脚注で、この証明が「必要よりずっと長いだろう」と認めている。
ワイルズの証明を理解していると言える人はいま世界に25人から50人しかいないだろう、という推定もスレッドに上がった（@bjourne）。そのリストに1,300万行の Lean リポジトリを加えることはできない。それは理解ではなく確認だからだ。バザードが自分のプロジェクトの残務として「人間が探索できる動的な文書」を挙げたのは、この隙間への正確な応答である。形式化は命題が真であることを確定させるが、なぜ真なのかを人間に伝える仕事は依然として別の労働である。
検証器がある場所でだけ効く魔法
HN で最も多く引用された数字には、こんな解釈が添えられていた。1,300万行と29,500個の中間定理という規模は、「正しいと示せることであればモデルは何でもやれる」という考えに信憑性を与える、というものだ（@m_w_）。この推論はどこまで妥当か。線を引いておく必要がある。
この問題が特別なのは、五つの条件が同時に成り立っていたからである。第一に、目標の命題がすでに形式的に存在していた。Mathlib に FLT の命題があったため、「何を証明するのか」を定義し直す必要がなかった。第二に、人間のコミュニティが作った86ページのブループリントという分解計画があった。第三に、ほぼ無謬の判定者が事実上いくらでも安く判定してくれる。第四に、部分的な進捗が再利用可能な部品として蓄積される。定理を一つ証明すればそれは永続的に残り、次の定理の材料になる。第五に、失敗が無害である。誤った証明はデプロイされて事故を起こす代わりに、単にコンパイルに失敗する。あるユーザーはこの構造を経験的に指摘した。検証器があれば、エージェントの思考がかなり混沌としていても意味のある解に収束する、というのである（@fspeech）。
実務上の問題の大半はこの条件を満たさない。命題そのものが曖昧であり（「ユーザーにとって使いやすい画面」）、判定者は人間であり、その人間は高くつき、遅く、日によって一貫しない。形式化の成功をそのまま一般化すると、条件ではなく結論だけを持ち込むことになる。
ソフトウェア工学への含意はむしろ明快だ。我々の業界にはすでに安価な判定者が揃っている。型チェッカー、テストスイート、コンパイラ、プロパティベーステスト、静的解析器、契約と不変条件がそれである。生成モデルの限界生産性は、これらの判定者が密なコードベースで際立って高い。裏返せば、判定者を増やして鋭くする仕事のほうが、コードを直接書く仕事よりレバレッジが大きいという結論になる。ただし同じ罠がここでも繰り返されることを忘れてはならない。テストが通ったということは、テストに書いた内容が真だという意味であって、我々が意図したものが真だという意味ではない。信頼の根がカーネルではなく命題の記述にあるという原則は、そのまま「信頼の根はテストランナーではなくアサーションにある」と翻訳される。ゲートを増やすほど、そのゲートが何を問うているのかを人間が読まねばならなくなる。
コストも併せて見るべきだ。60億の出力トークンについて、HN では公開レートで見積もって30万ドル前後という計算が出た（@davmre）。バザードは5年のプロジェクトに100万ポンドを受け取ったと記し、Anthropic は11日で済ませたがカネはもっと使ったのではないかと付け加えている。この比較を額面どおり受け取ってはいけない理由は明らかだ。失敗した試行のコストが計算に入っておらず、Mathlib とブループリントと先行する形式化という、ただで与えられたインフラが値札に載っていない。
今後のシナリオは三つに分かれる。楽観的には、バザードの期待どおり現代の研究文献の形式化が日常の作業となり、論文査読の負担が減り、「専門家には知られている」結果を暗黙に仮定してきた論文があぶり出される。悲観的には、検証はされたが誰も読まない巨大な生成物が積み上がり、カーネルのバグ一件がその全体を揺るがす。現実にはその中間のどこかだろう。形式化のボトルネックが労働から判断へ移り、人間の仕事は証明を書くことから、命題を選び検査することへ移っていく。
結論
冒頭の問いに戻る。Lean のカーネルが通した1,300万行は知識なのか。知識である。ただし、正確に一行についての知識だ。最終的な命題が真であることを我々はいまや機械的に知っている。しかし、なぜ真なのかはその中に入っていない。バザードが「数学的には本質的に何も教えてくれない」と書いたのは貶しではなく、この区別を正確に守った一文である。彼は同じ記事で高揚を隠していない。数千ページの文献が11日でエンドツーエンドに形式化できるのなら、遠からず現代の研究が進行中に形式化され始めるし、機械が不完全な論証を容赦なく指摘するようになるからだ。
だからこの出来事の意味は FLT にはない。FLT が真であることは、すでに誰もが信じていた。意味は、自動形式化が実用的な規模に達したという事実、そしてその瞬間に「検証された」と「理解された」が初めてはっきり分離したという事実にある。20年来の100定理リストの最後の項目は、こうして閉じられた。
残る問いは我々の側にある。形式的には検証されたが誰も読まない生成物が増え続けるとき、共同体は何を信頼の単位とするのか。そして、通過するテストと緑色の CI を根拠にすでに同じことをやっている我々のコードベースで、最後にアサーションを自分の目で読んだのはいつだったか。
出典: