フェルマーの最終定理が11日で機械検証された — 移せるのは足場であって検証者ではない

Anthropic が9月4日、フェルマーの最終定理(FLT)の、計算機で検証された初の完全な証明を公開した。 Claude が11日間ほぼ自律的に Lean で書き、1,300万行のコードと29,500件の中間定理を積み上げたという^[1]。 ただし新しい数学が生まれたわけではない。発表本文自身が、新しいのは数学ではなく検証のほうだと 書いている^[1]。本紙が読むべきはそこではなく、最初の試行がなぜ失敗したかという記録である。 エージェントはプロジェクトの状態を見失い、協調しなくなって止まった^[1]。 直したのはモデルではなく、外に置いた依存関係グラフだった。

公開されたのは「証明」ではなく「検証済みの証明」である

フェルマーの最終定理そのものは1995年にアンドリュー・ワイルズが証明している。129ページ、 検証には数か月の労力を要した^[1]。1993年6月の講演から2か月後、査読者の質問で決定的な穴が 見つかり、ワイルズは1年かけて元教え子のリチャード・テイラーと塞いだ^[1]。 今回 Anthropic が出したのは新しい定理ではなく、そのワイルズの証明(ダーモン・ダイアモンド・テイラーによる 簡略版に沿う)を Lean が機械的に検査できる形に翻訳しきったもの、いわゆる形式化である^[1]。

この区別は本紙の関心にとって重要なので、発表本文の言い方をそのまま引く。リーマン予想に関する 近年のAI研究が新しい数学を生んだのに対し、今回新しいのは検証である、と^[1]。 証明を電卓の計算のように検査できるようにした、という話であって、Claude が未解決問題を解いたのではない。

形式化は難しい。人間向けの証明は自明な段を飛ばして書かれるが、Lean はどれほど些細でも全段を要求する。 しかも人間の証明は数世紀ぶんの既刊研究の上に立つのに対し、形式化はすでに形式化されたごく一部の数学からしか 出発できない^[1]。FLT の形式化には年単位がかかると見られていた。2024年にインペリアル・カレッジ・ロンドンの Kevin Buzzard が始めた共同プロジェクトが、その初期フェーズを記述するために作った設計図(blueprint)だけで 86ページある^[1]。

公表された数字

最後から2行目を軽く見ないほうがいい。公理の欄である。形式化の失敗の典型は、通ったように見えて 実は少し違う命題を証明していた、という取り違えだが、今回は Lean の標準3公理以外を仮定せず、 証明した命題が Mathlib 自身の FLT の記述と一致することを比較器で確かめている^[1]。 Buzzard も、数学の公理以外に何の仮定も置かずに証明していると評した^[1]。

効いたのはモデルではなく足場だった

本紙が最も重要だと考えるのは、この発表が失敗を書いていることである。Claude の初期の試行は いくつも失敗した。エージェントは序盤こそ成果を出したが、プロジェクトの状態をすぐに見失い、 効果的に協調しなくなった^[1]。長時間・多エージェントの自律実行で起きる失敗として、 これ以上ないほど典型的な形である。

通ったのは、Peng らが Columbia University で作った公開プラットフォーム Prove2Me に切り替えてからだった^[1,2]。発表本文が挙げる効き目は3つある^[1]。

(1) 定理の主張を有向非巡回グラフ(DAG)として保持し、エージェントが次にどれを証明しにいくかをそこから 決める。記憶の劣化を緩和し、複数エージェントの並列作業を可能にしたのはこれだと書かれている^[1]。 (2) 定理の主張と証明を別ファイルに分け、その対応を独立に管理することで、Lean のコンパイルを速くし 資源消費を抑えた^[1]。(3) 各定理の主張に自然言語の説明を持たせ、検索と再利用を可能にした^[1]。

発表側が書いた不都合

1,300万行が Mathlib の5倍超という数字は、規模の誇示のように読める。だが脚注3は自らこう断っている。 Mathlib が簡潔でよく査読されているのに対し、今回の証明は必要よりかなり長い可能性が高い^[1]。 つまり行数は成果というより、まだ圧縮されていないことの指標でもある。

達成の瞬間として引用された Claude 自身の思考の抜粋も、素直に読むと慎重である。最初の一行は 「FLT の根が Proved と表示されている。歴史的瞬間(再検査を留保すれば)」だった^[1]。 発表本文は、この留保が付いたままの文言を消さずに載せている。

コストの側も明示されている。約60億トークンを使った、トークン集約的なプロジェクトである^[1]。 しかも使われたのは製品として売られているモデルではなく、汎用の社内研究モデル(Claude Fable 5.1 に概ね相当) だった^[1]。この規模をそのまま外部が再現できるという話ではない。 一方で Anthropic は、個人向け Claude Max の3契約だけを使い Prove2Me 経由で協調させた実験で、 ヴィノグラードフの三素数定理の形式化が3日で終わったことを挙げ、適切な足場があれば消費者向けの 契約でも主要な結果の共同形式化は達成可能だとしている^[1]。これは同社の主張であって、 第三者による再現は本稿の時点で確認できていない。

フィジカルAIに移せるもの、移せないもの

移せるのは足場である。外部に依存関係のグラフを置き、エージェントは自分の記憶ではなくそのグラフを見て 次の一手を決める——この構造は、長時間タスクを分解して回す身体性エージェントにそのまま対応する。 今回の実測は、11日間の自律実行を止めていたのが推論能力ではなく状態管理だったことを示している。

移せないのは検証者のほうだ。Lean のカーネルは、証明が正しいかどうかを完全に・自動で・ほぼ無コストで 判定する。だからこそ30,300件の試行がすべて機械採点され、失敗した試行の産物さえ約7%が最終成果に回収された。 ロボットの側にこれに相当するものは無い。試行1回に実時間がかかり、ハードウェアは摩耗し、 そもそも「成功したか」の判定自体が曖昧である。60億トークンは11日で使い切れるが、 60億回の試行を実機の腕にさせることはできない。

シミュレータはその代用にならない。Sim2Realギャップという言葉は、 言い換えれば「シミュレータは健全な検証者ではない」という事実の別名である。Lean は通れば正しいが、 シミュレータは通っても現実で落ちる。本紙が繰り返し書いてきた、デモの成功率と工場が求める歩留まりの桁の違いも、 突き詰めれば検証者が無いことに帰着する。

したがって「11日でフェルマーの最終定理」という数字を身体性の話に持ち込むときは、 検証者の有無で割り引く必要がある。数学で先に起きたのは、数学が易しいからではなく、 数学だけが安価で健全な採点機を持っていたからだ。

本紙の見立て

自律機械の側にも形式検証の入口はある。制御ソフトウェアの正しさは、原理的には Lean と同種の道具で 検査できる領域だからだ。今回示されたのは、その翻訳作業——人間には年単位だった作業——を エージェントが日単位でこなしうるという実測である。ただし断っておくと、今回の発表は自律機械の安全性検証について何も主張していない。 Buzzard の評価も、数学の文献をめぐる査読負荷の話に限られている^[1]。ここから先は本紙の推測であり、 裏付けとなる実測はまだ無い。

本紙が8月に扱ったModel Hardware Standardの構図と、 今回は同じ形をしている。足場が解いたのは配線であり、状態管理であって、身体性そのものではない。 エージェントを長時間走らせるための土木工事は着実に進んでいる。物理世界に採点機が無いという条件だけは、 まだ一つも動いていない。