AI が出す数学の結果に、人間の査読が追いつかなくなっている。その状況への答えとして、数学者の側から新しい学術誌の案が出た。Terence Tao のブログに10月17日に載った『Starting a new journal』で、掲載するすべての証明に、証明支援系 Lean での形式検証を求める。掲げる標語は『先取りより理解』である。翌10月18日には『Will it be a golden age or a dark age for mathematics and science?』が載った。AI 時代の数学と科学が黄金期になるか暗黒期になるかは、8つの選択で分かれると論じている。
この1か月で、数学の共同体は AI の結果を受け止める仕組みを2つ作っていた。Erdős 問題のサイトの規則の改定と、リポジトリの Hexagon である。今回の学術誌の案は、その流れをもう一歩進め、検証を投稿の条件そのものにした。
機械による検証を、査読の前の関門にする
この学術誌が既存の誌と最も違うのは、証明が正しいかどうかの判定を、まず機械に任せる点である。投稿される証明はどれも Lean で形式化してあることが前提になる。人間の査読者は、論理の細部を一行ずつ追う仕事から離れられる。代わりに、その結果が何を明らかにし、なぜ大事で、先行研究とどうつながるかを見ることに時間を使える。
『先取りより理解』という標語は、論文の価値をどこに置くかを示している。誰が先に結果を出したかではなく、結果を読んだ人が何を理解できるかである。AI が証明を大量に出せるようになった今、『最初に解いた』ことの重みは急に軽くなった。この標語は、その変化を誌の方針として書き込んだものと読める。
なぜ『先取り』が問題になったのか
この1か月の数学の共同体の動きを振り返ると、標語の背景がよく分かる。
OpenAI は10月6日、名前を明かさない社内モデルの原稿722本を GitHub に公開した（その後の撤回などを経て719本）。翌日には、Weil 類の代数性を扱う原稿で符号の誤りが見つかり、それに依拠する2本と合わせて3本を取り下げた。Lean で形式化してあるのは約42%だという。Sophie Huiberts は Tao のブログへのゲスト投稿（10月12日付）で、この公開を『普通に出来の悪い仕事』と呼んだ。考えの出どころの扱いが不適切で、細かく切り分けられ、証明は解読が途方もなく難しいという。
先取りをめぐる圧力は、人間の研究者の行動も変えている。Antonio Auffinger は9月22日のゲスト投稿で、自分の構想を誰かが AI に食わせることを恐れて、若手が論文を急いで出し、同僚が arXiv への投稿を控えるようになったと書いた。AI があふれさせたのは結果だけではない。『誰が先か』をめぐる焦りもあふれた。新しい誌の標語は、ここに直接答えている。
Erdős サイト、Hexagon、そして検証を条件にした学術誌
受け皿の仕組みは、少しずつ違う方向から作られてきた。
Thomas Bloom は10月6日、Erdős 問題のサイトの規則を改めた。AI が作った説明のない証明が、先取権を主張するために投稿される場になっていたからである。『解決／未解決』の表示と解決数の集計をやめ、結果を解いた人（人間か AI か）の手柄にしないことにした。代わりに、人間が読める解説と、リンクした Lean の証明を重んじる。手柄を数える仕組みをなくし、理解と検証を重んじるという方向は、今回の学術誌の標語とそのまま重なる。
同じ10月6日に、Ben Antieau が Hexagon を立ち上げた。LLM の助けを借りて得た結果を集める非営利のリポジトリで、全部を LLM が書いた仕事も受け付け、形式検証は求めない。その代わり、投稿者1人につき1日1本に絞る。10月12〜13日には投稿が入り始め、大半に『主に AI が生成』の札が付いていた。
3つを並べると、役割の分担が見えてくる。Hexagon は、検証の済んでいない AI の結果を、ひとまず置いておく場所である。Erdős サイトは、手柄の集計をやめて、検証と解説を重んじる方向へ規則を変えた。新しい学術誌は、検証を通ったものだけを載せる。検証を前提にした仕組みが、段階をつけて積み上がっている。
Lean を条件にする意味と、残る弱点
AI の証明は Lean で検証して公開すべきだという主張は、前から出ていた。Kevin Buzzard は10月1日の『To grieve, or not to grieve?』でそう論じている。10月16日に Tao が紹介した Avigad、Buzzard、Commelin らの『How to Formalize All of Mathematics』も、大規模な自動形式化での速さと理解の釣り合いを扱った。今回の案は、こうした議論を、投稿の規定という具体的な形にした。
ただし、Lean による検証も絶対ではない。Thomas Hales は10月9日のゲスト投稿で、7〜8月に Lean のカーネルで健全性の不具合が相次いだことを振り返った（『Summer of Soundness Bugs』）。そのうえで、約25の独立した Lean のカーネルで証明を突き合わせること、カーネルそのものを形式検証すること、土台の理論を固めることを提案している。Lean の型理論には、相対的な無矛盾性の完全な証明が今も公開されていないとも指摘した。検証を条件にする誌は、この土台の信頼性も引き受けることになる。
もう1つの課題は、形式化の及ぶ範囲である。分野によって、Lean のライブラリの厚みは大きく違う。全証明に検証を求めれば、形式化の進んだ分野の結果ほど載せやすくなる。どの分野をどう受け入れるかは、誌の設計の大きな論点になる。
『黄金期か暗黒期か』を決めるのは選択
10月18日の投稿は、AI 時代の数学と科学の行き先を、技術の性能ではなく、共同体が何を選ぶかの問題として示した。題名どおり、黄金期になるか暗黒期になるかを分けるのは8つの選択だという。
この見方は、Tao が10月10日の『Math 2.0』で示した立場と同じ筋にある。そこでは、AI に未解決問題を自動で解かせることを強調しすぎる流れを批判した。そして、人間が中心にいて、AI が人間の理解と数学の共同体を支える形を求めていた。前日の学術誌の案は、こうした選択のうち少なくとも1つ、つまり『先に出すこと』と『理解されること』のどちらを評価の軸にするかに、制度の形で答えようとするものと位置づけられる。
残る問い
案を実際の学術誌にするまでには、まだ決めることが多い。誰が編集し、誰が費用を出すのか。Lean での形式化の手間を誰が負うのか。AI が形式化まで担った投稿を、著者の仕事としてどう扱うのか。
資金の面では、Simons 財団、Anthropic、OpenAI が10月15日に始めた1,500万ドルの事業がある。AI の助けを借りた結果を評価する仕組みや、共同体の基準づくりを公募で支えるもので、受け皿の候補になりうる。Simons 財団の Spergel 財団長は『これらの道具をどう評価し、採り入れ、使うかの議論を主導するのは共同体であるべきで、どれか1つの会社や機関ではない』と述べた。新しい学術誌の案は、その議論の場を、数学者自身が検証を前提にして作ろうとする試みである。
