Terence Tao が10月10日、自分のブログに『Math 2.0』を載せた（一次情報）。この数週間、Tao のブログには AI と数学をめぐる他の数学者のゲスト投稿が続いていた。今回は、ブログの主である Tao 本人がまとまった見解を出した。Tao によれば、『最近の出来事』を受けて、予定していた講演の中身を大きく変えたという。批判の対象は、AI に未解決問題を自動で解かせることを強調しすぎる流れである。代わりに Tao が求めるのは、人間の理解と数学の共同体を支える『Math 2.0』だ。
結論を先に言えば、Tao の問いは『AI はどれだけの問題を解けるか』ではない。『AI の結果が増えるなかで、数学を人間が理解する営みとして保てるか』である。これは、OpenAI が10月6日に始めた大量公開と、その直後の撤回への答えとして読める。
講演を変えさせた『最近の出来事』
Tao は『最近の出来事』としか書いていないが、時期から見て、中心にあるのは OpenAI の数学の成果の公開だと考えられる。OpenAI は10月6日、名前を出していない社内のフロンティアモデルに約4,000問を解かせ、原稿722本（結果のまとまりで372）を GitHub に公開した。翌10月7日には、そのうち3本を取り下げた。きっかけは『Algebraicity of Weil classes on split abelian eightfolds』の符号の誤りで、自分で決めた約束では−1になるはずのところが+1になっていた。これに依拠していた2本、つまり Kuga–Satake 対応の代数性と、K3 曲面の積に対する有理ホッジ予想の原稿も一緒に取り下げた。ほかに14本の証明を手直しし、Lean で形式化してある割合は約42%になった。公開は719本となり、撤回はその後増えていない。どのモデルが出した成果なのかは、今も示されていない。
公開の直後には、Tao がこのペースを『常軌を逸している』と言ったと報じられていた（Scientific American などの報道による二次情報）。今回のブログは、そうした断片的な反応ではなく、Tao 自身がまとまった形で立場を示したものである。
批判の的は『自動で解く』を成果の物差しにすること
Tao が批判したのは、AI を数学に使うこと自体ではない。未解決問題を AI に自動で解かせることばかりを強調する流れである。解いた数を成果として数え、ベンチマークのように示すやり方では、証明の中身を人間が理解し、検証し、次の研究に生かす部分が抜け落ちる。Tao が掲げる Math 2.0 は、AI をその部分を支える側に置く考え方である。
この懸念は、Tao だけのものではない。ナビエ・ストークスの件では、James Maynard が『この新しい AI の証明から人間の理解を引き出すのは、これまでのところ非常に難しい』と述べていた（NPR）。Tapio Schneider は Tao のブログで、正しくても理解できない証明は『見出し』を与えるだけで、『内幕の物語』は与えないと書いた。Tao の Math 2.0 は、こうした指摘を、数学という営み全体の設計の話に広げたものといえる。
このブログが共同体の議論の場になっていた
この見解が重いのは、Tao のブログ自体が、AI の結果があふれることに数学の共同体がどう応じるかを話し合う場になってきたからである。10月だけでも、次のような寄稿があった。
受け皿の仕組みを作る寄稿
Thomas Bloom は10月6日、Erdős 問題のサイトの規則を変えると書いた。AI が作った説明のない証明が、先取権を主張するために投稿されていたためで、コメントを止め、『解決／未解決』の表示と解決数の集計をやめた。代わりに、人間が読める解説とリンクした Lean の証明を重んじる。同じ日に Ben Antieau は、LLM の助けを借りた結果を集める非営利のリポジトリ『Hexagon』を紹介した。投稿の数は制限し、最初は1日1本から始める。
見方を変える寄稿
10月7日の Raghu Meka は、AI がほったらかされていた問題を解いたことで、数学の『壁』の多くは思い込みだったと分かったと論じた。10月9日には Thomas Hales が、Lean の信頼性を正面から取り上げた。7〜8月に Lean のカーネルで健全性の不具合が相次いだ『Summer of Soundness Bugs』を振り返り、独立したカーネルで証明を突き合わせること、カーネルそのものを形式検証することなどを提案した。OpenAI の『約42%は Lean で形式化済み』という部分をどこまで信じてよいかに直結する話である。
どの寄稿も、何問解けたかではなく、結果を人間の側がどう受け止め、確かめ、手柄を誰に帰すかを扱っている。Tao の Math 2.0 は、ブログの主として、この流れに方向を与えたものと読める。
OpenAI の『数で示す』方式との対比
OpenAI が10月6日に示したのは、規模と速さだった。1つの結果に使った計算は ChatGPT Pro 並みで約3時間とされ、プロンプトは出さず、平均の計算量だけを示すとしている。公開の進め方には、IAS が受け入れている数学と AI の諮問グループ（AGMAI）の助言を受けたという。ただし AGMAI は、OpenAI が『社内の進捗のペース配分』を助言の対象から外したまま作られた組織である。
大量に出し、誤りが見つかれば取り下げ、どのモデルの成果かは示さない。この進め方では、検証の負担は外部の数学者に回ってくる。Andrew Sutherland が、モデルが公開されるまで単一のエージェントの主張は『未検証』として扱うべきだと述べたのも、同じ問題を指している。Tao の主張は、この負担の偏りを、数学の共同体の側から問い直すものである。
今後の焦点
Tao の見解が実際の仕組みにどう反映されるかが、次の焦点になる。具体的には、AGMAI が公開の進め方について公式の勧告を出すか、OpenAI が成果を出したモデルを明かし、撤回の基準を示すか、Gowers や Buzzard などがこの見解にどう応じるか、である。数学は、AI の成果をどう評価するかについて、他の分野より早く規範づくりを迫られている。その中心にいる人物が、解いた問題の数より人間の理解と共同体を軸にすると明言したことは、ほかの研究分野が AI の結果の受け皿を作るときにも参考になる。
