代数幾何の7500ページを、AIの群れが機械で確かめ直した。見つけた直しは、本家には送らない

「AIが数学をやる話、もう何回目？証明できました、また証明できました、でしょ？」そう思ってる？今日のは、証明の話から始まって、別のところに着く。誤りを見つけたあと、誰がそれを直すのか、という話だ。

前回の記事まで、3回続けてAnthropicの話をした。今日は別の会社。ただ、話の芯は9月に書いた『20年埋まらなかった最後の1行を、AIが11日で埋めた』の続きになる。あのとき私は、機械が保証してくれるのは論理だけで、何を言おうとしていたのかを読むのは、まだ人間の仕事だ、と書いた。今日は、その「人間の仕事」の側が、自分から線を引いた話でもある。

20年かけて書かれた参考書を、まるごと機械にかけた

主役は、Stacks Projectという数学の参考書だ。代数幾何という、方程式と図形の関係を調べる分野の土台を書いたもので、約7500ページある。コロンビア大学の数学者Johan de Jongが2005年に始めて、20年のあいだに何百人もの数学者が証明や例や手直しを持ち寄って育ててきた。定義や定理の一つひとつに、4文字の決まった番号（タグ）が付いている（Axiom）。

11月4日、Axiom Mathという会社が、このStacks Projectを丸ごと、Leanという証明を機械で確かめる言語に書き移して公開した。約1600万行。Axiomは、これまでに作られた中でいちばん大きい、つながった形で使い回せる、機械で確かめた数学の道具箱だと言っている（Axiom）。

9月の記事で、Claudeがフェルマーの最終定理の証明を1300万行のLeanにした話をした。あれは1つの定理を確かめる仕事だった。Axiomも、10月27日に有限単純群の分類という1つの大きな定理を形式化して出している。でも今回のStacksは性格が違う、とAxiomは書く。何千もの定義と補題が絡み合っていて、価値は、この先の無数の証明に部品として使われるところにある（Axiom）。辞書を作った、に近い。

なぜ要るのか。AIが人間の手では見きれない速さで数学の議論を書き出すようになると、機械で確かめることが欠かせなくなる。ところが代数幾何は、ひとつの現代の証明が、本題に入る前に長い定理の鎖を引っぱってくる分野で、それに見合うLeanの土台が無かった（Axiom）。Axiomの技術スタッフのAshvin Swaminathanは、形式化された数学の地図を見ると代数幾何のところがぽっかり抜けていた、とTechCrunchに話している。

やり方は、AIのエージェントの群れだ。役割を分けた階層を作って、依存のつながりをたどりながら、文を訳す、Mathlib（世界中の数学者が積み上げてきたLeanの証明の土台）に同じものがないか探す、証明を組む、前提を片付ける、を並行して回した（Axiom）。全部をきっちり指図したわけじゃなく、エージェントが自分で仕事を見つけていた、とSwaminathanは言う（TechCrunch）。

CEOのCarina Hongの一言がいい。「人生では、大きいものと繊細なものは、どうにも両立しない」（TechCrunch、原文は英語）。1600万行にわたって、つながりを1つも切らさず、定義どうしが食い違わないように保たないといけなかった（TechCrunch）。

書いてある通りには成り立たない文が、出てきた

で、ここからが面白い。

機械にかけたら、Stacks Projectの中に、直しが要る文が数十個見つかった、とAxiomは書いている。仮定が足りないもの、正の標数という特殊な場合で例外が出るもの、書かれた一般性のままでは成り立たないもの。エージェントは証明に失敗したところで止まらずに、どこで成り立たなくなるかを示す反例まで作った。仮定が抜けているだけなら、足りない仮定を特定して、直した定理と反例を並べて形式化した。深い定理を支える補題がまちがっていたところでは、文献の中から別の道を探して、元の仮定のままで本題の定理を示した（Axiom）。

1つ、中身を見てみた。Stacksの第98章「Artinの公理」にある補題、タグ0GHB（Stacks Project）。Axiomのリポジトリのファイルには、書かれたままではこの補題は偽で、いまオンラインにある版（コメントも訂正も付いていない）も同じだ、とある（AxiomのGitHub）。

反例の作り方が、ちょっと笑える。出発点の材料をぜんぶ空っぽにする。すると、補題が「1対1に対応する」と言っている2つのもののうち、片方は何も無いのに、もう片方には少なくとも1つある。対応しようがない。原因は、条件のひとつが、どこかに開いた部分があればいい、としか言っていなくて、どの部分かを縛っていないことだった。そのうえでファイルは、本当に言いたかったことは証明の書き方から読み取れる、と続けて、その意図どおりに条件を絞った版を証明している（AxiomのGitHub）。

11月6日に本家のタグ0GHBのページを開くと、コメントは0件だった。

本家は、当面は手で直すつもりだ

ここで、本家の側の話をする。

10月21日、de Jongは自分のブログに「No AI for now」という短い文を出した。当面は、AIにコメントやプルリクエスト（変更の提案）を出させないでほしい。AIが書いた中身を含むコメントやプルリクエストも、出さないでほしい。少なくとも近いうちは、Stacks Projectの更新と修正は手で続けるつもりだ、と（Johan de Jong）。

突き放してはいない。読んでいて気づいたことを、自分で欄に打ち込んだコメントは大歓迎。直しを見つけて、そのLaTeXを自分で打ち込んだなら、メールでもプルリクエストでも送ってほしい、と書いている（de Jong）。

で、最後の一文がこれ。

「あなたがAIで見つけるものは何でも、私もAIで見つけられる（もう見つけているかもしれない）！」（de Jong、原文は英語）

うまいな。怒ってもいないし、AIを否定してもいない。私にはこう聞こえる。見つけるだけなら、もう誰でもできる。だから見つけたものを持ち込まれても、それだけでは助けにならない。直すかどうか、どう直すかは、この本を20年預かってきた自分が決める。

ちなみに本家のコメント欄には、ボットよけに、いま見ているタグの名前を打ち込んで人間だと示す欄がある（Stacks Project）。

Axiomは、この線を守ると書いた。de Jongの頼みを全面的に尊重して、形式化も、反例も、直しも、自分たちのリポジトリに置いておく。数学者が自分のやり方で見て、使えるように、と（Axiom）。

つまりこうだ。AIの群れが、本の中に直しの要る文を数十個見つけた。その直しは、本の持ち主のところには持っていかない。別の倉庫に並べて、扉を開けてある。

人が見直した棚と、AIが書いたままの棚

もう1つ、割り引かないといけないところがある。

Axiomのライブラリは2段になっている。StacksCoreは、人がStacks Projectと突き合わせて、Mathlibの基準まで整えた部分。StacksFrontierは、AIのエージェントが書いて、まだ人が見直していない部分だ。どちらの証明もLeanが全部確かめていて、証明を後回しにする印（sorry）は1つも無い（AxiomのGitHub）。

数えてみた。StacksCoreのLeanのファイルは445個。ライブラリ全体は約6万3000のモジュールでできている、とREADMEにある。残りのほとんどは、StacksFrontierのほうだ。さっきのタグ0GHBの反例のファイルも、StacksFrontierに入っている。リポジトリに置かれた説明の書類には、StacksFrontierの文は一つひとつタグと照らし合わせたけど、まだ人の見直しは受けていない、とはっきり書いてある。プロジェクト全体の見直しの状態も、自己評価となっている（AxiomのGitHub）。

Axiom自身も、機械で確かめた証明より、定理の文が元の数学の意味を正しく写しているかのほうが大事だと書いている。そこは、複数のエージェントによる点検と、元の文との意味の照合と、後ろの定理にちゃんとつながるかどうかで、自動で守っているという。土台になる定義と大きな定理には、狙いを絞った点検も足している（Axiom）。

9月に私が引っかかったのも、まさにここだった。機械は「AからBが出る」は確かめられる。「このBが、言いたかったBなのか」を確かめるのは難しい。Axiomはそこを自動の点検で埋めにいった。でも、人の見直しを済ませたStacksCoreは、445ファイルだ。参加の案内にも、StacksFrontierのコードを見直してStacksCoreに移す仕事が並んでいる（AxiomのGitHub）。

答え合わせの方法を、先に作る

同じ週、別の分野から、ちょうど反対側の話が出ていた。

Y Combinatorの2026年春の組に入っていた材料のスタートアップ、Discovered Materialsが、材料科学の未解決問題5つに、総額100万ドルの賞金をかけた。ごく低い温度で電気抵抗がゼロになる、銅の酸化物の超伝導を説明する理論、ほぼすべての半導体に入っているシリコンと二酸化シリコンの境目の構造を予測する計算の方法、などだ（TechCrunch）。

発表の前に、最先端の研究所のモデルにネットにつないだまま何日も自分で取り組ませたけど、どの問題もあまり進まなかったという。共同創業者のAdvaith Sridharは、材料科学は数学と違って、はっきりした定義があって正しいか間違いかに行き着く、という形で問題を書きにくい、と話している。だから先に確かめ方と課題を決めて、そのあとで誰かに説明を考えてもらう、新しいやり方を試す、と（TechCrunch）。

並べると、よく分かる。数学には、Leanという、正しいか間違いかを機械が言ってくれる仕組みがある。だから7500ページを丸ごと機械にかけられた。材料科学は、その仕組みから作らないといけない。でも数学の側でも、答え合わせの機械があるからといって、問いの文そのものが言いたいことを言えているかまでは、機械だけでは決まらない。

割り引いて読むところ

まず、ここまでの多くはAxiomの自己申告だ。Stacksの中で直しが要った文が数十個、という数も、Axiomのブログが書いているだけで、外の人が数えた数字じゃない。いちばん大きい道具箱だ、というのもAxiomの言い方だ。

次に、リポジトリは11月4日に公開されたばかりで、作業はAxiomの社内のリポジトリで進められた（AxiomのGitHub）。ほかの数学者が中身を見るのは、これからだ。

それと、de Jongがこの公開をどう見ているかは、まだ分からない。本家のブログの最新の投稿は、10月21日の「No AI for now」のままだ（de Jong）。

今日の本音

AIの群れが、20年かけて人が書いた7500ページを機械で確かめ直して、書かれたままでは成り立たない文まで掘り出した。それ自体、まずワクワクする。

でも今日いちばん面白かったのは、見つけた側が直しを本家に持ち込まず、本家の持ち主は、AIで見つけられるものは自分もAIで見つけられると書いて、少なくとも当面は手で直していくつもりだと言ったところだ。見つけるのは、もう速い。次の問いは、誰がそれを引き受けて直すのか、だ。