9 月 1 日から 5 日にかけて、OpenAI は約 1 万体のエージェントを同時に走らせ、88 時間で強制項つき 3 次元 Navier-Stokes 方程式の有限時間爆発を証明したと発表した。追加で 17 時間、別のモデルが証明支援系の Lean で形式化と検査を行ったという。投じられたのは 270 万件のやりとりと、この問題だけで約 1,300 億の出力トークン、金額にして数百万ドル規模とされる。
その証明を、まだ誰も見ていない。約 100 ページあるとされるが公開されておらず、当事者として説明を受けた数学者本人も「見ていない」と書いている。
同じ週に、もう一つ別のことが起きていた。ニューヨーク大学の Tristan Buckmaster と Levent Alpöge が、3 つの結果を Lean での形式化つきで公開した。こちらは誰でも機械にかけて確かめられる。そして Buckmaster は、その公開と同時に 4 ページの声明を出した。
これは数学のニュースであると同時に、自分の未完成の仕事を道具に預けて進める人間全員に向いた記録でもある。なお本記事の中心にある証明は公式一次ソース未確認のままで、OpenAI 側の説明については複数報道が伝えた発言に依っている。
まず、確かめられることから
公開されているものと、されていないものを分けておきたい。
公開されているのは、Buckmaster と Alpöge の 3 つの結果だ。非圧縮多孔質媒体方程式、Boussinesq 系、3 次元非圧縮 Euler 方程式について、なめらかな強制項つきの有限時間爆発。いずれも Lean の形式化が添えられている。
公開されていないのは、OpenAI の Navier-Stokes の証明そのものだ。主張の中身は「R³ と T³ における強制爆発の存在」で、強制項はなめらか、Fefferman による問題設定の選択肢 c と d に相当する、と説明されたという。ミレニアム懸賞問題としての賞金は、査読つきの出版と 2 年の待機期間を経て初めて対象になる。OpenAI は賞金を請求する意思はないとしている。
もう一つ確かめられることがある。Buckmaster と Alpöge も、hypo-dissipative Navier-Stokes については爆発を得たと考えているが、Lean の検証が終わっていないため公開していない。出さない理由が、明示されている。
手柄の話は、二者間では終わらない
声明で目を引くのは、Buckmaster が自分たちの功績を主張していないところだ。
彼は、この研究計画は自分たちが始めたものでも、大規模言語モデルが提案したものでもないと書く。基本アイディアの功績は Diego Córdoba と Luis Martínez-Zoroa にあり、二人は強制爆発の構成を何年も探ってきた。自分と Alpöge がやったのは、粗い強制項での結果を、モデルの助けを大量に借りてなめらかな強制項と Euler 方程式まで押し進めたことだ、と。そのうえで「Luis Martínez-Zoroa はフィールズ賞に値すると思う」と書いている。
誰の手柄かという問いは、ここで少なくとも四つの層に割れる。道を開いた先行研究者。その道を歩いた人間。使われた道具。道具を作って持っている会社。この四層はふだん重ならないが、道具が結果の大部分を生むようになると、真ん中の二層が近づいて見える。
個人の机の上で起きていたこと
ここが、この一件で最も見落とされやすい部分だ。
Buckmaster は、Alpöge との共同研究は完全に個人的なもので、双方の雇用主の institutional な合意も公式の関与もない、と書いている。研究グループが使うツール代は自分の研究費から払っており、そこには OpenAI への大きな請求書も含まれる。使ったモデルは一社ではない。Anthropic の Claude、OpenAI の Codex、とりわけ GPT-5.6 Sol、そして最近になって Astra。最後のものは文章化と論証の監査にだけ使ったという。
進み方も書かれている。1 年近く進捗は遅く、8 月 15 日になってなめらかな強制項での爆発結果が Boussinesq と Euler の両方で出た。Alpöge から送られてきた最初のモデル生成の証明について、彼は「これまで読んだ中で最もひどいものだった」と書く。それを 8 月 22 日に Lean で検証した。以後は、その証明を理解して読める形に直す作業を続けていた。
自費でツールを買い、複数社のモデルを併用し、未完成の下書きを入れて進める。それは今、個人が新しい技術基盤を使って仕事をするときの、ごく普通の形だ。
何が言えて、何が言えないか
9 月 3 日、Anthropic が大きな未解決問題を解いたという噂が流れているのを知り、Buckmaster は OpenAI の著名な数学者に電子メールを書いた。声明にはその全文が引用されている。要旨は、噂の出どころは自分たちかもしれないこと、これは機関の取り組みではなく個人の共同研究であること、そして未完成の Lean 証明書だけを急いで出すことは意図的に避け、まず通常の数学的な論証として提示したい、というものだ。
9 月 6 日、複数回の通話が持たれた。Alpöge は通話に入っていない。そこで内部モデルによる証明の存在を伝えられ、その後の説明が変わっていった経緯が書かれている。当初は「人間の入力はごくわずか」と伝えられていたが、実際にはチームが問題に取り組んでおり、これは試された複数の方針の一つで、最初は易しい問題から始めていた、と。示されたプロンプト自体も Codex に書かせたものだったという。
そして提案が二つ出された。声明によれば、そのうち一方には Alpöge を著者から外すという条件が含まれ、その理由として彼が Anthropic に所属していることが挙げられたという。Buckmaster は両方を断った。
OpenAI 側の説明も出ている。同社の研究責任者は、ユーザーデータを人間も AI システムも検索していないと述べ、こうした申し立てには落胆したとしている。別の幹部は、Euler の問題は内部モデルが「まったく異なる手段で」解いたと述べた。同社はその後、両者の製品利用から派生した de-identified なデータが自社モデルの改善に寄与した可能性は排除できない、とも述べている。公開されている説明はデータの扱いに向けられており、著者名の条件についての反論は確認できていない。
そして Buckmaster 自身が、自分が主張していないことを 4 つ挙げている。OpenAI の証明を見ていない。そのモデルが何をどうやったのかを知らない。自分たちのデータが使われたかどうかを知らない。誰かを非難してはいない。彼が述べているのは、いつ何を伝えられ、何を提案されたか、それだけだ。
機械が確かめた証明と、誰も見ていない証明
形式化された証明には、一つはっきりした性質がある。正しく見えるように話し込むことができない、という性質だ。Lean を通ったものは、誰の権威にも依存せず、機械にかければ同じ答えが返る。
OpenAI 側も 17 時間かけて Lean で形式化したとされている。だがそれが外に出ていない以上、この性質は働かない。数学の世界では、確かめられるようになるまで、主張は結果にならない。
この非対称は、規模の差とは逆を向いている。1 万体と 88 時間と数百万ドルの側にあるのは、まだ主張だ。個人の研究費と 2 人の側にあるのは、すでに確かめられる形になったものだ。
私たちは、どう向き合うか
読者の多くはミレニアム懸賞問題を解かない。それでも、この一件で起きたことの形は、規模を落としても同じように起こる。
預ける前に決めておけることがある。未公開の仕事のうち、どの段階のものを、どの道具に入れるか。学習に使われる設定がどうなっているか。そして、その道具を持っている相手が、同じ領域で自分の競合になりうるかどうか。Buckmaster は複数社のモデルを併用していたが、下書きを入れていた先の一つが、後に同じ問題を発表した側だった。
記録を自分の側に残す方法もある。日付の入る形で先に出す。機械が検査できる形にしておく。声明を読むかぎり、彼らがやっていたのはまさにそれだ。8 月 22 日に Lean を通したという事実は、後からの議論を「言った・言わない」から引き離す。
ただし代償がある。読める形にするには時間がかかる。Buckmaster は、理想を言えば生成された証明を読み物にするのに最初のページから何週も費やしたかったと書き、急いで出した Euler の文章について自ら厳しい評価を書いている。丁寧にやれば遅れ、急げば形が崩れる。この二択は、道具を使う側に必ず戻ってくる。
そして、記録を残しても防げないことも残る。時系列を証拠として持っていても、相手が先に発表してしまえば、外から見える順番は変わる。個人にできるのは、順番を確定させることまでで、その先の解釈までは持てない。
見ておきたい点
この先、確かめられるようになるかもしれない点が三つある。OpenAI が約 100 ページの証明、あるいは Lean の形式化を公開するかどうか。Buckmaster と Alpöge の hypo-dissipative Navier-Stokes の検証が終わって公開されるかどうか。そして、Córdoba と Martínez-Zoroa の先行研究が、今後の発表でどう扱われるか。
Buckmaster は声明の終わりに、これが Deep Blue とカスパロフの局面に当たるものだと書き、もし本当に OpenAI のモデルが最後の隙間を埋めたのなら、それは素晴らしいことであり、経緯を残したまま、彼ら自身の口から大きな声で語られるべきだ、と書いている。
道具は速くなった。速さは、誰が何をしたかの記録を勝手には作ってくれない。あなたは自分の未完成の仕事を、どの段階で、どこに置くだろうか？
