本稿は、OpenAI が一週間で Navier–Stokes の結果を公開した出来事から始まり、Alpöge–Buckmaster の時間軸と共同声明の議論をたどったうえで、形式化された正しさ、知識の伝承、研究過程を分けて考えます。信頼できる検査を通った結論は、まず明確な利用範囲を持つことができます。理解、説明、伝承は同じように重要な貢献であり、並行して進められます。
ほとんど一夜で現れた答えから始まった
一次資料と関連文献 · 25 名のフィールズ賞受賞者による共同声明 · Terry Tao による Alpöge–Buckmaster の成果紹介 · OpenAI の Navier–Stokes に関する説明 · Tristan Buckmaster の公開文書
Navier–Stokes 方程式は、水や空気のような流体の運動を記述します。三次元非圧縮方程式の滑らかな解が滑らかさを保ち続けるかどうかは、七つのミレニアム懸賞問題の一つです。これは偏微分方程式の問題であると同時に、航空機設計、天気予報、血流の研究にも関わります。有限時間特異性とは、滑らかな初期データから始まった解が、有限時間内に速度の発散などによって正則性を失う現象です。粘性は不安定性を抑えようとしますが、非線形相互作用はエネルギーをますます小さな尺度へ集中させます。この緊張関係が問題を難しくしています。
2026 年 9 月の第一週、OpenAI はこの問題を AI の数学能力をめぐる公開競争の中へ持ち込みました。同社の説明によれば、8 月 28 日から訓練中の内部モデルが非常に強い数学能力を示しました。9 月 1 日、二つのミレニアム問題が解かれたかもしれないという報告を聞き、チームは未解決問題やその他の重要な問題でシステムを試し始めました。約 100 のエージェントが約 50 時間並行して作業し、最初の結果は外力のない Euler 方程式に関するものでした。これは粘性を無視した流体モデルであり、チームはその後 Navier–Stokes に資源を移しました。
OpenAI によれば、エージェントは 9 月 5 日、取り組みの開始から約 88 時間で Navier–Stokes の解析的な解答に到達しました。その後、Lean で形式化と検証に累計約 17 時間を使い、9 月 8 日に論文とコードを公開しました。Lean は対話型定理証明器です。形式証明は、命題、依存関係、検査規則を、信頼できるカーネルが再検査できる形で示します。OpenAI は、提示した定式化の範囲でミレニアム問題を解いたと説明し、この発表をモデルの能力と研究速度の公開記録として位置づけました。
この時間軸だけを見れば、ニュースの中心は明快です。長く未解決だった問題について、他者が検査を続けられる新しい結果が現れ、形式化資料も論文と同時に公開されました。論争が始まったのは、同じ週に別の研究の時間軸が公の記録へ入ったからです。
同じ週に、別の研究の時間軸が公の記録へ入った
Tristan Buckmaster と Antonin Alpöge は、以前から流体方程式を長く研究していました。Buckmaster の公開文書によれば、二人は 8 月 15 日、滑らかな外力を含む Boussinesq 方程式と Euler 方程式について進展を得ていました。また数か月分の研究上の対話、プロンプト、資料を Codex セッションに保存していました。読者にとって、それらのセッションは研究過程の作業台に近いものです。問いの立て方や試した道筋を記録する役割を担います。
9 月 3 日、大規模言語モデルが重大な未解決問題を解いたかもしれないという報告が広がりました。Buckmaster は OpenAI に連絡し、9 月 6 日の二度の通話で、過去二か月に Codex に残していた未公開研究が内部システムからアクセスされたのか、訓練に使われたのかを尋ねました。公開された文書には、その問いと通話の内容が記録されています。9 月 7 日、二人は非圧縮多孔質媒体方程式、二次元 Boussinesq 方程式、三次元非圧縮 Euler 方程式について三つの有限時間爆発結果と Lean 形式化を公開しました。これらは隣接する方程式を扱う、同じ流体特異性研究の線上の結果です。早い公開によって、二人の成果と時刻も同じ公共記録に入りました。
公開文書には、優先権と著者表示をめぐる争いも記録されています。そこには、Anthropic の職員 Levent Alpöge を共同発表の著者に含めるかどうかという問題もありました。9 月 10 日の更新で OpenAI は、Buckmaster が過去二か月に Codex に残したプロンプトが内部システムや訓練に影響することはあり得ず、相手の成果が公開される前に研究者やエージェントがそれを見ていなかったと説明しました。同社は、プロジェクトと Lean 検証を終えた後、並行公開を望んでいたこと、外力付き Euler の結果について相手の優先権を認めたことも述べました。
データ隔離、優先権、著者表示について、公開された説明は一致していません。判断には、アクセスログ、訓練データの来歴、通信、版の時刻、独立者が調べられる監査資料が必要です。争いの焦点は証明の正しさから、研究者が自分の仕事を公平な条件で保存し、説明し、発表できるかどうかへも広がっています。
Tao の紹介と共同声明が議論の背景を広げた
9 月 7 日、Terry Tao は Alpöge–Buckmaster の仕事を刺激的な進展として紹介し、三つの有限時間爆発結果と外力のない Navier–Stokes 問題との関係を説明しました。また、最初の証明文は非常に読みにくく、著者たちが専門的な論文へ書き直していることにも触れました。問題を解くこと、証明の構造を理解すること、他者が再利用できる方法を取り出すことは、同じ時間表で進む作業ではありません。
9 月 11 日、Tao は「A Severe Misalignment of AI in Mathematics」という共同声明を公表しました。最初の署名者には 25 名のフィールズ賞受賞者が含まれていました。声明は、概念的理解と数学的洞察を数学共同体が重視する中心に置き、問題を解くことをその目標へ至る道具または代理指標として説明します。また、著名な未解決問題を AI の benchmark にすることを批判し、競争が速い発表を、丁寧な執筆、方法の抽出、先行研究の引用、共同知識への統合より前へ押し出すことを懸念しています。
声明は OpenAI の論文公開から三日後に出され、自然に同じ公開議論の中へ入りました。本文が扱うのはより広い AI と数学の実践であり、特定の論文に対する数学的裁定ではありません。それでも、中心にある因果の問いは今回の出来事に直接触れています。答えがモデル能力の公開指標として示されるとき、速度や注目が、説明、帰属、共同体が理解するために必要な時間を追い越してしまわないか。後の分析では、数学、伝承、研究過程を分けて考える必要があります。
この出来事を三つの次元から見る
ここまでの時間軸は、出来事がどのように進んだかを示しました。ここで視点を変えます。数学の結果が公開の議論に入るとき、その結果には同時に三つの次元があります。これらを分けておくと、共同声明が何を論じているのか、そして今回の争いのどの部分に別の証拠が必要なのかが見えてきます。
第一は正しさです。AI が生み出した命題が、示された仮定と範囲の中で成立するのか、その証明や形式対象を他者が独立に検査できるのかを問います。ここには客観的な側面と、人間がその正しさを確かめる側面があります。命題がすでに成立していても、読者が論文を読み、依存関係を調べ、実験や形式コードを再現し、自分の判断を得るまでには時間がかかります。結果の成立と、それを共同体が確かめるまでの時間は、一つの仕事の異なる段階です。
第二は知識の伝承です。検査を通った結果は、他者が読み、引用し、教え、発展させられる知識へ書き直される必要があります。問題の背景、先行研究、証明を支える構造、適用範囲を示し、後の研究者が再利用できるようにする作業です。この次元は、結果が共同知識へ入るか、人間がそこから構造と方法を取り出せるかを問います。
第三は倫理です。結果がどのように作られ、どのように公開されたか、研究者と共同の規則が尊重されたかを問います。未公開資料がアクセスまたは訓練に使われたのか、貢献と著者表示は正確だったのか、優先権はどのように扱われたのか、関係する研究者に公平な発表の機会があったのか。これらには、アクセスログ、データの来歴、通信、時刻、独立監査が必要です。数学の命題を判断する証拠とは異なります。
共同声明が主に扱うのは、最初の二つの次元です。概念的理解と数学的洞察を中心に置き、著名な未解決問題を benchmark にすることが、答えの速さを知識の伝承より前へ押し出すのではないかと懸念しています。つまり、答えを得ることと、それを共同の数学知識へ変えることの関係を論じています。今回のデータ隔離、優先権、著者表示の争いは第三の次元に属し、理解を重視する声明だけで決着するものではありません。
この三つの次元を見据えて、次の分析を順に進めます。OpenAI が公開した論文と形式化資料が正しさの問いに何を与えるのか、知識の伝承に固有の時間と作業がなぜ必要なのか、そして価値ある結果と研究過程の適切さをどのように分けて考えるのか。
第一の問い：形式化された結果はどの範囲で正しいのか
形式化は、自然言語の命題、変数、仮定、依存関係、証明を、検査器が扱える対象へ変換します。論文の主張が形式命題と一つずつ対応し、依存関係が公開され、カーネルが証明項を受け入れ、他者が同じ条件で検査を再現できるなら、その結論は提示された範囲で明確な正しさの境界を持ちます。新しい構造を示すか、読みやすいか、教科書に入るかは別の証拠で判断します。
SAT は小さいながら強い比較を与えます。固定されたブール問題に対し、充足可能だと主張するなら割当を、充足不可能だと主張するなら独立の検査器が確認できる証明書を提示できます。証明書が通れば、工学システムはその範囲で設計を排除し、制約を確認し、次の計算へ進めます。利用者はソルバーが試した経路をすべて理解する必要がなく、証明書も優雅な理論へ整理されるまで役に立たないわけではありません。
形式化された AI の証明も、より豊かな対象について同じ論理をたどります。正確な命題、証明対象、依存関係、カーネル検査を与え、自然言語の主張が形式命題に忠実に対応し、隠れた依存がなく、公開された基礎から検査を再現できるなら、その結果は範囲内で利用可能な正しさを持ちます。人間が読むには長い時間が必要かもしれません。構造の説明、方法の発展、教科書化は後から来る可能性がありますが、その遅れが既に成立した形式的証拠を消すことはありません。
正しさと理解は、並行して育つ二つの貢献です。形式化された結果が数日で教科書にならなかったからといって、科学的価値を失わせるべきではありません。同じ範囲と形式状態の結果を人間が発表したなら、共同体は通常、検査と消化のために数か月、時には数年を認めます。AI が関わったという出所だけを理由に、数日で完全な概念説明まで求め、それがなければ認めないなら、作品より出所を上位に置く二重基準になります。形式化の不忠実さ、依存の欠落、読みにくい論文、不正確な帰属への批判は成立しますが、具体的な欠陥に向けるべきです。
形式化された結論を、境界の明確な呼び出し可能な数学的コンポーネントへ育てる方法については、別の文章で扱っています。ここでの要点は一つです。安定した再利用を考える前に、結果には検査可能な境界が必要です。
第二の問い：知識はどのように伝わるのか
共同声明が丁寧な執筆、説明、正確な帰属、教育、後続研究を重視する点には理由があります。結果が文献、教室、その後の研究へ入り、他者が理解して発展させられると、記録は共同知識へ変わっていきます。発表後も、著者はその道に責任を負います。
知識の伝承は独立した貢献であり、結果が共同知識へ入るための過程です。それを正しい結果を使うための許可証にする必要はありません。信頼できる検査を通った結論は、明確な範囲内で先に引用、再現、利用できます。その間に数学者は証明の構造を説明し、よりよい表現や一般化を探せます。数学には、人が理解し、教え、伝えられる知識として残す機能があります。同時に、境界が明確で、後続研究が信頼して再利用できるコンポーネントとして残す機能もあります。二つは互いを強め、成熟する速さも異なります。
ポアンカレ予想の歴史は、具体的な時間尺度を示します。Perelman の最初の関連プレプリントは 2002 年 11 月 11 日に公開され、続く二つの資料が 2003 年 3 月と 7 月に現れました。最初のプレプリントから初期資料がそろうまで約 8 か月です。その後も Hamilton、Kleiner、Lott、Tian らによる検証、解説、整理が続きました。2006 年には、最初のプレプリントから約 3 年半が経ち、証明は共同体が公に頼れる理解へ徐々に変わっていました。最初の数日で教科書にならなかったことは、その時点で生まれた数学的内容を消しません。
OpenAI が論文と形式化資料を公開したのは 9 月 8 日です。この記事の改訂日である 9 月 14 日まで、まだ 6 日しかありません。6 日あれば論文とコードを読む入口はできますが、すべての検証、説明、構造の抽出を終えるには短すぎます。文章の明瞭さや先行研究の扱いを問い、後続の論文に読みやすい説明を求めることはできます。途中にある伝承を、結論に価値がない証拠へ変えることはできません。
人間の著者が同じ形式化結果を提出したなら、理解と教科書化には時間がかかる後続作業だと考えるでしょう。AI が関わる成果にも同じ時間尺度を適用すべきです。命題が成立するか、説明が信頼できるか、より広い数学知識へどう入るかを、証拠の進みに合わせて評価していけばよいのです。
ポアンカレ予想の時間資料 · ポアンカレ予想の時間軸 · Perelman の最初のプレプリント
第三の問い：数学的価値と研究過程は同じなのか
結果の数学的価値と、それがどのように作られ公開されたかは別の問いです。モデル企業が商業的な目的を持っていても、科学的に有用な仕事をすることはあります。動機だけで価値が消えるわけではありません。正しい結論も、データ利用、著者表示、優先権の問題に免責を与えるわけではありません。
今回の出来事では、問いが具体的です。未公開の Codex 資料がアクセスまたは訓練に使われたのか。研究者のプロンプトとデータは内部システムから隔離されていたのか。貢献と著者表示は正確だったのか。関連研究の存在を知った後も、公平な並行公開の選択肢が示されたのか。公開の時期を決める力を誰が持っていたのか。Buckmaster の文書と OpenAI の更新は異なる説明を示します。公開記録は争いの存在を示しますが、すべての事実を独立に確定するものではありません。
未公開研究を使って先に発表したなら、あるいはデータの境界や著者表示で研究者を明らかに不利な立場に置いたなら、最終的な数学が正しくても研究ガバナンスの失敗です。ログ、データの来歴、時刻、通信、独立監査が隔離を示した場合でも、研究者が優先権や著者表示の扱いを問う権利は残ります。数学の証拠と過程の証拠は、異なる問いに答えます。
したがって、結果に価値があるかと、公開が適切だったかは分けて評価する必要があります。前者には論文、形式コード、依存関係、再現が必要です。後者にはアクセスログ、データの来歴、通信、著者表示の取り決め、独立者が検査できる監査が必要です。一方の証拠で他方を置き換えると、議論は本来の問題から離れてしまいます。
結果から共同知識へ：追跡可能な科学の過程
新しい機械支援の結果は、連続した科学の過程を進むことができます。各段階が別の信頼性を加え、後の読者が調べられる記録を残します。
これらの段階は、仕事の進行に合わせてそれぞれ開いていけます。形式結果は、伝承が続いている間も、検査でき引用できる記録になれます。説明と外部審査も公開後に改善できます。段階ごとに証拠があり、公開文は完了したことと進行中のことを明確に書けばよいのです。
- 命題、適用範囲、形式証明、依存関係、公理の状態、再現可能な検査手順を固定する。
- 背景、先行研究、例、証明の道筋を示し、形式対象を研究者が無理なく読める論文へ書き直す。
- 論文とコードを公開プレプリントとして出し、外部審査を受け、質問、修正、訂正を記録する。
- 論文、形式コード、版の時刻、引用、公開議論を一つの追跡可能な記録に保つ。
- サーベイ、授業、教科書、後続研究が構造を取り出し、理解できる結果と信頼して再利用できる結果を育てる。
発見、検査、伝承にそれぞれの時間を与える
この出来事は、しばしば一つにまとめられる判断を分けて見せました。結論が正しいか、共同体が理解したか、研究過程が参加者と公共の規則を尊重したか。互いに関係していますが、それぞれに固有の証拠と時間があります。
私たちは今後も、命題と形式的な境界を固定し、再現可能なカーネル検査を行い、証明を人が読める論文にし、公開プレプリントと外部審査へ進め、修正、説明、後続利用を追跡可能な版の記録に残します。知識の最初の形を保存しながら、共同体の理解と信頼できる再利用へ進む道を保ちます。
数学の仕事は二つの形で長く残り得ます。人が理解し、教え、伝えられる知識として残ること。そして、境界が明確で、後続の仕事が信頼して呼び出せるコンポーネントとして残ることです。科学には二つの時間尺度が必要であり、それらを一つの誠実な記録で結びつける必要があります。新しい技術は発見と検査の速度を変えます。科学共同体の仕事は、その速度を、検査でき、説明でき、後の人へ渡せる成果へ変えることです。