AIが書いた数学原稿722本が一度に出てから2週間、よく読まれた記事のいくつかが同じ問題を指摘しました。確かめて理解する速さが、生み出す速さに追いつかないという問題です。OpenAIが10月6日に公開リポジトリopenai/mathに置いた原稿のうち、3本は翌日に撤回されています。あるフィールズ賞受賞者は泣いたと打ち明けましたが、「数学を始めるなら今ほどいい時期はない」という題の動画も話題になりました。この件を扱った記事のうち、10月19日までにHacker News（HN）の上位に入ったものをまとめて読みました。
原稿722本、問題4,000問
OpenAIは原稿とLeanの証明を、GitHubの公開リポジトリopenai/mathに置きました。最初のREADMEによると原稿は722本で、関連する原稿どうしが372のファミリーにまとめられています。大半は未公開の社内モデルを使い、同じ手順で得た結果です。結果1つあたりChatGPT Pro並みの推論に平均3時間をかけ、モデルに出した問題はおよそ4,000問でした。
Scott Aaronsonはブログで、長年解けなかった問題をこのモデルに任せると、3時間の試行1回でおよそ10問に1問は解ける計算になると書いています。公開された結果には、Subhash Khotのユニークゲーム予想の証明も含まれています。ただしREADMEを見ると、結果ごとに検証の段階が違います。すべての結果がLeanで形式化されているわけではなく、「形式化されていない結果には問題があるかもしれない」という一文も添えられています。
OpenAIが最初に公開した原稿は722本です。点1つが原稿1本です。
関連する原稿どうしが372のファミリーにまとめられています。点の位置は原稿の順番とは関係ありません。
翌日の10月7日、このうち3本が撤回されました。残る原稿は719本です。
ある原稿の符号の誤り1つが、同じ構成を使っていた原稿2本まで崩しました。
同じ日の時点で、残る719本のうち主要な結果300件、約42%がLeanで形式化されました。
残りは、まだコンピュータが証明を1ステップずつ確かめていない原稿です。
翌日に撤回された3本
10月7日、リポジトリの変更履歴（history.md）に、ホッジ予想に関わる原稿3本を撤回するという記載が加わりました。理由は短いものです。ある原稿に符号の誤りが1つあって打ち消し合いの議論が成り立たず、同じ構成を使っていた原稿2本も一緒に取り下げた、というのです。撤回の告知には「撤回は証明についてのもので、命題が偽だと主張するものではない」とも書かれています。同じ日、OpenAIはほかの原稿14本で証明を補ったり命題を修正したりし、Leanの形式化を6本追加しました。これで、残る719本のうち主要な結果300件、約42%が形式化されたことになります。
OpenAIのDan RobertsがXでこの更新を伝えると、いいねが1,804件付き、表示は54万回を超えました。HNでは381ポイント、コメントは612件です。READMEには「一部の結果は、モデルが先に出した結果を土台にしている」という一文もあります。誤り1つが原稿3本に広がったのはそのためです。
Leanが確かめること、確かめないこと
証明支援系Leanで形式化した結果では、コンピュータが証明を1ステップずつ検査します。Thomas HalesはTerence Taoのブログに寄せたゲスト記事で、その保証がどこまで及ぶかを整理しました。カーネルを通った証明でも、カーネル自体にバグがあれば誤っている可能性があります。この夏には、Leanのバグが原因でコラッツ予想を「反証」する誤った証明が出てきたこともありました（いまは修正済みです）。もっとよくある落とし穴は命題のほうです。Leanが確かめるのは証明が命題に合っているかどうかだけで、その命題や定義が私たちの意図どおりかまでは確かめません。
Leanの証明であっても、命題が意図どおりかを人間が確認するまでは受け入れるべきではない。
Thomas Hales、Terence Taoのブログへのゲスト記事
Halesは、この確認はふつう証明そのものを確かめるよりずっと簡単だと付け加えています。私の見方では、42%という数字は出発点です。形式化されていない原稿には形式化が、形式化された原稿には命題の確認が残っています。
泣く人も、歓迎する人も
Derek Thompsonはコラム「I know why the mathematicians weep」（数学者たちがなぜ泣くのか、私にはわかる）で数学者たちの反応を集めました。HNで397ポイントを得た記事です。2022年にフィールズ賞を受けたHugo Duminil-Copinは、10月の公開のあとにこう語っています。
火曜の夜、泣いていたら娘が起きてしまった。あの人たちが、私の研究分野を消し去ってしまった。
Hugo Duminil-Copin、Derek Thompsonの記事より
Terence Taoは公開当日、Mathstodonに4回に分けて投稿しました（HN 614ポイント）。Taoが「Math 1.0」と呼ぶこれまでの数学では、長年の予想が解かれると、証明した人があちこちで講演し、ワークショップが開かれます。共同研究や次の問題が生まれ、新しい人がその分野に入ってきます。そのあいだに証明は磨かれ、次の世代の教科書に載ります。Taoは、いまはその逆がよく起きていると書いています。AIで問題を解いた人が、結果を説明できるほど理解しないまま次へ移り、続くセミナーや共同研究もずっと少ないというのです。先を越されるのを恐れて、有望な研究の方向を公開しないことまで起きているそうです。
未解決問題の答えをいまのように大量に刈り取るやり方は、長くは続かない。
Terence Tao, Mathstodon, 2026-10-06
Taoのいう「Math 2.0」は、問題を解くことだけでなく、解説を書くこと、コミュニティを育てること、新しい研究の方向を開くことまで、数学の進歩として認めようという提案です。Taoは、AIはそのすべてに貢献できると考えています。ただし、お気に入りのAIエージェントに未解決問題を投げて答えを受け取るだけの発想より、もっと大きな想像力と野心が要るとしています。
Aaronsonは記事（HN 409ポイント）で、少し違う角度から論じています。公開された結果の一部はLeanで検証されているものの、これらの証明をきちんと理解した人はまだほとんどいないといいます。それでも、「AIで私たちの未解決問題を解いて楽しみを奪うな」という主張はまったく受け入れられないと言い切っています。こうした能力は、どのみちGPTやClaudeを契約していれば誰でも使えるようになるからです。
今回の証明をきちんと理解した人は、まだほとんどいない。理解しようとする競争は始まったばかりだ。
Scott Aaronson, The Mathocalypse
Aaronsonによると、AIによる数学の成果を発表するやり方は2つに分かれつつあります。1つはOpenAIのように、AIが書いた証明をそのまま公開するやり方です。もう1つはAnthropicのやり方です。Virginia WilliamsとJosh Almanは、Anthropicのモデルが出した核となるアイデアをもとに、3SUM問題と全点対最短経路問題のアルゴリズムを改良しました。Anthropicは生の結果をすぐには出さず、2人に報酬を払って、内容を咀嚼して書き直した論文として発表してもらいました。Aaronsonは、どちらにも長所と短所があるといいます。OpenAI方式では入り組んだ証明を誰が先に読み解くかの競争が起き、Anthropic方式ではAIの成果を伝える数学者を企業が選ぶことになります。
同じころ、3Blue1Brownの動画「There’s never been a better time to go into math」（数学を始めるなら今ほどいい時期はない）もHNで541ポイントを得ました。題を見るだけでも空気は正反対です。動画の中身はこの記事では扱っていません。
コードにも同じ問いが残る
私の見方では、この話はAIがコードを書くいまの開発とよく似ています。Leanのカーネルによる検査は、テストや型検査にあたります。命題が意図どおりかを見る確認は、人が仕様を読むコードレビューです。Taoが挙げた証明の後に続く活動は、コードでいえば、そのコードを理解している人がチームに残っていることです。
機械が回せる検査をまず用意します。テスト、型、形式検証のように、人がいなくても回る検査です。
その検査が何を確かめているかは人が見ます。テストが的外れな仕様を守っていたら、緑のチェックに意味はありません。
説明できる人を残します。結果を説明できる人がいなければ、次の人はその上に積み上げられません。
原稿722本が一度に出てきたことで、数学の世界では確かめて理解する速さが、生み出す速さに追いつかなくなりました。数学でもコードでも、これからその差を埋めていく必要があります。