Anthropic が公開したのは、Fermat の最終定理について「新しい数学の発見」ではなく、「既にある証明を Lean で最後まで機械検証できる形に落とし込んだ」成果だ。しかもその作業は、人間が細かく手を動かして積み上げたというより、Claude が 11 日間かなり自律的に進めたものだという。数学の世界では、証明が正しいかどうかを読む人間が何週間も何か月もかけて確かめることがある。そこに AI と proof assistant の組み合わせがどこまで食い込めるのか、Anthropic はかなり強い実演を見せた格好だと思う。
Anthropic の発表によると、Claude は Fermat の最終定理の proof を Lean という programming language に書き直し、computer-checked な形で最後まで通した。Fermat の最終定理とは、正の整数 a, b, c について aⁿ + bⁿ = cⁿ を満たす解は n > 2 では存在しない、という有名な命題だ。17世紀に Pierre de Fermat が書き残したもので、長く未解決だったが、1995年に Sir Andrew Wiles が最初の正しい proof を完成させた。Anthropic はその Wiles の proof を、人間が読む文章としてではなく、コンピュータが逐一チェックできる形に変換した。
ここで重要なのは、Claude が新しい数学をひねり出したという話ではない点だ。Anthropic 自身も、今回の新しさは「verification」、つまり proof の検証にあると説明している。Lean のような proof assistant は、数学的な推論をアルゴリズムとして確認する。人間向けの証明なら「自明な一歩」は飛ばせるが、Lean にはそういう飛ばしが通じない。すべての段差を埋める必要がある。今回 Claude は、その作業を 11 日間でやりきった。途中で 13 million lines の Lean を書き、29,500 の中間 theorem を証明したという。別の箇所では、30,300 の theorem を computer-verifiable にしたとも書かれている。最終的な proof では 29,500 を使ったということだ。
作業は単独のモデルが一気に解いたわけではなく、複数の Claude agents が協力する形だった。初期の試みは、状態管理がうまくいかず失敗したらしい。そこで Anthropic は Prove2Me という collaborative platform に切り替えた。これは theorem の依存関係を DAG として管理し、自然言語の説明も残し、Lean の compile を分割して軽くする仕組みを持つ。Claude の人間側の入力は、Tianyi Peng が時々投げた高レベルの指示だけに限られていた。たとえば「Jacobian as a scheme sounds high priority」「push Mazur theorem to be done soon」といった具合だ。最終的には、Claude Code ベースの multi-agent harness と Prove2Me を使い、約 6 billion output tokens を消費して proof を完成させたとされる。
Anthropic はこの結果を、将来の数学研究のあり方に関係するものとして位置づけている。もし大きな theorem をこうして formalize できるなら、数学論文の誤りを見つけたり、新しい主張を査読する負担を軽くしたりできる。Kevin Buzzard のコメントでも、AI による formalization が現代数学の文献全体を機械的に検証する方向に進む可能性が語られている。Anthropic は、将来は human-readable な説明と formalized proof をセットで出すのが当たり前になるかもしれない、と見ている。
この発表で面白いのは、Fermat の最終定理そのものよりも、「証明を読む」から「証明を機械に通す」へと重心がずれていることだと思う。数学の世界では、正しさは昔から重要だったが、実際の運用では人間の読解力にかなり依存してきた。長い証明は、専門家が時間をかけて眺め、穴がないか確認する。ところが AI が大量の theorem を積み上げていく時代になると、そのやり方は追いつかなくなる。Anthropic の主張は、そこに formalization を差し込めば、検証のコストを下げられる、というものだろう。
私は、この方向性はかなり現実的だと思う。なぜなら、AI が出すものの量が増えるほど、「人間が全部読む」モデルは破綻するからだ。数学に限らず、コード、仕様書、法務文書、研究メモでも似た話が起きる。人間向けの説明は必要だが、それだけでは信頼の裏取りにならない。機械がチェックできる裏帳簿があるかどうかが効いてくる。Fermat の最終定理は象徴的に見えるが、本当に変わるのは、その周辺にある“検証の作法”ではないかと思う。
一方で、ここをそのまま「Claude が数学を解いた」と受け取るのは少し雑だ。元記事を読む限り、Claude がやったのは強力な formalization であって、既存の大定理を Lean に写し込むことだった。もちろん、それ自体が簡単な仕事ではない。13 million lines、29,500 の theorem、11 日という数字は異様だ。ただ、数学者が本当に知りたいのは、証明の骨格をどう新しく発見するかであって、整形だけではない。Anthropic もそこは分かっていて、formalized proof は human-understandable exposition を置き換えるべきではないと書いている。
ここで大事なのは、AI が「発見」と「検証」の両方を同じ速度でできるわけではない、という現実だと思う。今回の成果は検証の側に大きく寄っている。だからこそ価値がある一方で、これをもって AI がすぐに数学の中心部を乗っ取る、とは言いにくい。むしろ逆で、人間が発見した proof をどれだけ早く堅牢に固められるか、その補助輪として強い。数学者にとっては助かるが、同時に「本当に面白い部分」はまだ人間に残る。そこは冷静に見たほうがいい。
もう一つ引っかかるのは、Claude 単体の賢さより、周辺の scaffold の設計が勝負を決めている点だ。初期の agents は状態を見失い、うまく協働できなかったという。そこで DAG で theorem の関係を管理し、ファイルを分け、自然言語の説明を残し、検索と再利用をしやすくした。つまり、長大な数学 proof では、モデルが賢いだけでは足りず、作業空間の設計がそのまま成果を左右する。これは研究のやり方としてかなり示唆的だと思う。
私はここに、AI 研究の次の競争点が見える気がする。モデル本体の性能差だけでなく、複数 agent をどう編成するか、どの情報をどこまで構造化するか、どこに人間の高レベル指示を残すか。今回の発表は、そうした「周辺設計」が大きな theorem の formalization を現実にすることを見せた。逆に言えば、AI を使った研究は、ますますソフトウェア工学とタスク分割の問題になるのではないか。数学の話に見えて、実は運用設計の話でもある。
Anthropic は、formalization が査読の負担を減らすと言っている。これは楽観的に聞こえるが、私はかなり本音に近い見立てだと思う。論文が増え、AI が生成した proof まで混ざると、読む側は「面白いか」だけでなく「本当に通っているか」を見る必要がある。そのとき、formalized proof が一緒に出てくれば、少なくとも検証の入口はかなり変わる。査読者は文章の説得力だけでなく、機械検証可能な証拠を見られるからだ。
ただ、これがそのまま学術の民主化になるかというと、そこはまだ分からない。Lean や Mathlib を使いこなせる人は限られているし、大規模な formalization は依然として専門的だ。AI がその敷居を下げる可能性はあるが、逆に「formalization できる人だけが通る」世界になる危険もある。だから私は、この発表を単なる成功談としてではなく、学術コミュニティに新しい技能を強いる出来事として見ている。証明を書く力に加えて、証明を機械に渡す力が必要になる。Fermat の最終定理は、350 年越しの大定理であると同時に、その変化の象徴として使われたのだろう。
