OpenAIが「ナビエ–ストークスを解いた」。6時間前に告発文が出ていた

みなづちです。

OpenAIが9月8日、こう発表しました。

Our system produced an analytical proof and a Lean formalization that an initially smooth fluid at rest can develop a singularity in a finite time.

静止した滑らかな流体が、有限時間で特異点を発生しうる。その解析的な証明とLean形式化を、自社システムが生成した、という内容です。

ナビエ–ストークス方程式の問題は、クレイ数学研究所が100万ドルの賞金をかけたミレニアム懸賞問題の1つです。それをAIが解いたという主張が、企業から出ました。

ところが、その6時間前に別の文書が公開されていました。ニューヨーク大学の教授が、自分のサーバーに置いた4ページの署名入り声明です。そこにはこう書かれています。

Sebastien twice asserted that he wanted Levent removed from authorship of his own work

OpenAIのセバスチャン・ブベック氏が、共著者のレヴェント・アルポゲ氏を著者から外すよう2度求めた、という主張です。アルポゲ氏はAnthropicの社員です。

ブベック氏はこれを全面的に否定しました。

I never ever asked for Levent to be removed from authorship of his own work

同じ出来事について、当事者の言うことが正面から食い違っています。そして第三者による事実認定は、私が確認できた範囲ではまだありません。

本記事では、以下のポイントから解説します。

• 何が発表され、どの数字が確定しているか
• 告発文と反論のどこが対立し、どこが一致しているか
• この共同研究が、実は1年前に始まっていたこと
• 「Leanで検証済み」が何を保証し、何を保証しないか
• 賞金を請求しないという一行の意味

結論：食い違っているのは「著者から外せと言ったか」の1点

先に結論を3つ置きます。順番に本文で確かめます。

1つ目。OpenAIは公式定式化の主張「C」と「D」を確立したと述べています。これは解の存在と滑らかさを示す側ではなく、破綻を示す側の選択肢です。約1万のエージェントが88時間、Leanの形式化と検証にGPT-6 Astraがさらに17時間を要したと書かれています。

2つ目。当事者の主張は「著者から外すよう求めたか」という1点で正面から食い違っています。そしてこの点について、第三者が事実を認定した記録は確認できませんでした。両者の言い分をそのまま並べる以上のことは、現時点では書けません。

3つ目。「Leanで検証済み」は、証明が正しいと確認されたことを意味しません。OpenAI自身がリポジトリの設定ファイルに「self-assessed（自己評価）」と記載しています。機械検証の公的なレジストリには、9月9日朝の時点でまだ登録されていません。

ただし公平のために先に書いておきます。この件を「OpenAI対Anthropicの企業戦争」として読むのは、事実に合いません。後述するとおり、この共同研究はAnthropic社員個人の動機で1年前に始まっています。

筆者の視点：「企業の争い」で書こうとして、1年前のメールで崩れた

この記事も、最初に立てた見立てが検証で崩れました。

「AI企業2社の代理戦争」から始めた

構図は分かりやすく見えました。OpenAIが未解決問題を解いたと発表し、Anthropic社員を共著者に持つ研究者が同じ日に告発文を出す。「競合2社の争いが学術界に持ち込まれた」という軸で書こうとしました。

アルポゲ氏本人が出した1年前のメールで崩れた

崩れました。アルポゲ氏が9月8日15時14分に投稿し、自分が1年前にバックマスター氏へ送った勧誘メールのスクリーンショットを添えていたからです。

日付は2025年9月19日。件名は「Normal pure math collaboration with ai」。動機としてこう書かれています。

Basically for ideological reasons I fear a world in which corporations are the ones with claim to the deepest pure math work

「企業が最も深い純粋数学の仕事を所有する世界を、イデオロギー的な理由から恐れている」。会社の指示ではなく、個人の動機でした。

「Leanで検証済みだから正しい」も書けなかった

次に「形式検証が付いているのだから証明は正しい」という前提で書こうとしました。これも崩れました。

Leanの公式ドキュメントが、証明の妥当性と定理文の意味は別問題だと明記しています。そしてOpenAI自身が、レビュー状態を「self-assessed」と記載していました。

残ったのは「誰も認定していない」という事実だった

残ったのは、地味な確認作業でした。両者の発言を時刻順に並べ、一致点と対立点を分け、第三者の認定があるかを探すことです。

認定は見つかりませんでした。この記事はそこから組み直しています。

発表は9月8日19時。告発文はその6時間前に出ていた

まず時刻を確定します。

OpenAIの発表は日本時間9月8日19時00分

OpenAIの公式RSSに、こう記載されています。

pubDate: Tue, 08 Sep 2026 10:00:00 GMT

日本時間では9月8日19時00分です。

ただし注意が要ります。発表ページ本体には構造化データの公開日時がありません。私が取得した生HTMLを検索しましたが、JSON-LDもdatePublishedもarticle:published_timeも0件でした。ページ上の表示は「OpenAI September 8, 2026」という日付のみで、時刻はありません。時刻の根拠はRSSだけです。

告発文は日本時間9月8日12時58分

バックマスター氏の声明PDFは、ニューヨーク大学クーラント数理科学研究所のサーバーに置かれています。HTTPヘッダのLast-Modifiedはこうでした。

Tue, 08 Sep 2026 03:58:30 GMT

日本時間では9月8日12時58分30秒。OpenAIの発表より約6時間早いことになります。

応酬は9月9日の朝まで途切れなく続いた

その後の発信を日本時間で並べます。

• 9月8日15時14分：アルポゲ氏の投稿（1年前の勧誘メールのスクリーンショット付き）
• 9月8日15時43分：ブベック氏の投稿
• 9月8日19時00分：OpenAIの発表
• 9月9日2時39分：ブベック氏の詳細な反論（4項目）
• 9月9日2時57分：アルポゲ氏の投稿
• 9月9日1時56分ごろ／6時32分ごろ：バックマスター氏の再反論

ブベック氏の反論の一部は、OpenAIの発表より前に出ています。

解いたと主張しているのは(C)と(D)。外力は公式に認められている

何を解いたと言っているのかを、原文で確かめます。

公式定式化には4つの選択肢がある

クレイ数学研究所が公開している公式問題文には、(A)から(D)まで4つの主張が並んでいます。

(A)と(B)は「解の存在と滑らかさ」を示す側で、外力について「Take f(x, t) to be identically zero」と、恒等的にゼロであることを課しています。

(C)と(D)は「破綻（Breakdown）」を示す側です。(C)の原文にはこうあります。

there exist a smooth, divergence-free vector field u◦(x) on R3 and a smooth f(x, t) on R3 × [0, ∞), satisfying (4), (5), for which there exist no solutions

滑らかな外力fの存在が明示的に許されています。

OpenAIが主張しているのは(C)と(D)

発表ページにはこう書かれています。

This resolves the Navier–Stokes Millennium Prize problem by establishing statement “C” (and also “D”) in the official Millennium Prize formulation

したがって「外力を加えているから本物のミレニアム問題ではない」とは書けません。公式定式化の(C)(D)は外力を認めています。

ただし世間が想像するのは(A)(B)のほうが多い

同時に、押さえておくべきこともあります。一般に語られてきた「ナビエ–ストークス問題」は、外力なしの(A)(B)であることが多いという点です。

規則には、ナビエ–ストークスについては「どちらの方向の解決も」標準的な評価手続の対象になると書かれています。4つのうちどれを示しても対象になる建て付けです。この事実と、世間の受け止めとの差は、両方書かないと読者を誤誘導します。

使ったのはAstraではなく、8月28日から訓練中の社内モデル

ここが本連載の読者にとっていちばん引っかかる点かもしれません。

完全な一文は「To solve」から始まる

To solve the Navier–Stokes problem, we used an internal model that is significantly more capable than GPT-6 Astra.

「ナビエ–ストークス問題を解くために、私たちはGPT-6 Astraより大幅に高性能な内部モデルを使用した」。

訓練は現在も続いていると書かれている

続く記述はこうです。

Since August 28 we have been training a new internal model that has exhibited unprecedented performance in our benchmarks, including mathematics.

This model’s training is ongoing and its performance continues to improve.

8月28日から訓練を続けており、訓練は現在も進行中で、性能は向上し続けている。そう書かれています。

公開最上位のAstraとの非対称が残る

本連載は9月5日に、GPT-6 Astraの展開状況を扱いました。そのとき確認したヘルプの記述は「Astra is not yet generally available」でした。

公開されている最上位モデルの提供状況がまだ整理されていない一方で、社内にはそれを大きく超えるモデルが既にある。この非対称が、今回の発表で初めて明示的に書かれました。

約1万エージェントが88時間。Leanの検証はAstraが17時間

数字を原文で押さえます。

エージェントの規模は1万のオーダー

The groups varied in size, and the group that produced the Navier–Stokes resolution involved on the order of 10,000 concurrent agents.

「on the order of（〜のオーダー）」であって、正確に1万ではありません。そしてこれはナビエ–ストークスを解いたグループの規模で、プロジェクト全体の総数ではありません。

88時間で到達し、追加で17時間かかった

The agents arrived at their resolution on Saturday, September 5, about 88 hours after the first agents were launched. Lean formalization and verification took an additional 17 hours via GPT-6 Astra.

88時間で解に到達し、Leanの形式化と検証にさらに17時間。合計ではなく、88時間の後に17時間が乗ります。

そしてこの17時間の検証を行ったのはGPT-6 Astraです。人間でも第三者でもありません。

メッセージ490万件、出力トークン約3,000億

Across all attempted problems, the agents sent 4.9 million messages and used about 300 billion output tokens. In the process of resolving the Navier–Stokes problem, the agents sent 2.7 million messages and used approximately 130 billion output tokens.

490万メッセージと約3,000億出力トークンは全問題の合計、270万メッセージと約1,300億出力トークンがナビエ–ストークス単独です。いずれも出力トークンで、入力トークンの記載はありません。

きっかけは噂だったと、OpenAI自身が書いている

経緯についても、OpenAIは自ら書いています。

9月1日に噂を聞いて着手したと書いている

On Tuesday, September 1, we heard rumors that two Millennium Prize problems had been resolved.

2026年9月1日は実際に火曜日です。この噂と社内モデルの性能変化に触発されて、未解決のミレニアム問題すべてを評価する取り組みを始めた、と書かれています。

噂の対象が誰だったかも書いている

さらに踏み込んだ記述があります。

Our effort began on September 1st after hearing a rumor which we later realized was related to Levent Alpöge, an Anthropic employee, and Tristan Buckmaster, a math professor at NYU.

のちにアルポゲ氏とバックマスター氏に関係すると判明した噂を聞いて始まった、とOpenAI自身が認めています。

ただし「噂を聞いた」ことと「相手の成果物を見た」ことは別です。OpenAIは見ていないと明示的に述べています。

共同研究は2025年9月19日、アルポゲ氏の1通のメールで始まった

ここで構図が変わります。

2025年9月19日付の勧誘メールだった

アルポゲ氏が9月8日15時14分に投稿した画像は、2025年9月19日付で本人がbuckmaster@cims.nyu.edu宛に送ったメールのスクリーンショットでした。

件名は「Normal pure math collaboration with ai」。会社の名前ではなく、個人からの誘いです。

「企業が純粋数学を所有する世界が怖い」

メール本文にはこう書かれています。

Basically for ideological reasons I fear a world in which corporations are the ones with claim to the deepest pure math work, and since it seems to me there will be only one Millennium Problem solved in the foreseeable future, I wanted to email you on a lark to ask if you’d considered working

企業が最も深い純粋数学の仕事を所有する世界を、イデオロギー的な理由から恐れている。だから声をかけた、という趣旨です。

1年がかりの共同研究だったことになる

この日付は、共同研究が約1年前に始まっていたことを示します。

「Anthropicが対抗して仕掛けた」という読み方は、この一次情報と合いません。始めたのは個人で、しかも動機は企業による独占への懸念でした。

2人が使ったのは一般提供のClaudeとCodexだった

使ったツールについても、原文があります。

声明にはClaudeとCodexの両方が挙がる

バックマスター氏の声明にはこうあります。

We used several LLMs throughout: Anthropic’s Claude, OpenAI’s Codex, especially with GPT-5.6 Sol and, more recently, Astra. The latter was only used for writeups and auditing our arguments.

Anthropicの Claude と、OpenAIの Codex の両方を使っています。Astraは書き上げと議論の監査にのみ使ったとされています。

「社内モデル」という主張には裏づけが確認できない

一方でブベック氏は、アルポゲ氏を独立した学者とみなせなかった理由として、内部のAnthropicモデルが使われたという趣旨を述べています。

ただし、この「内部」を裏づける原典を私は確認できませんでした。バックマスター氏の声明も、報道も、いずれも一般提供のClaudeと記しています。

アルポゲ氏本人もこう書いています。

on my side things were mostly me and claude having a good time yoloing random stuff in the corner rather than anything institutional

組織的なものではなかった、という趣旨です。

告発文の核心は「共著者を著者から外せと2度言われた」

声明の中身に入ります。

該当箇所の逐語は「twice asserted」

Sebastien twice asserted that he wanted Levent removed from authorship of his own work, and said it would all be simple if only it were not the case that, and it was so annoying that, Levent works at Anthropic.

2度、著者から外すよう求められた。そしてアルポゲ氏がAnthropicで働いていなければ簡単なのに、それが煩わしい、と言われた。そう書かれています。

断ったあとに返ってきたとされる2つの言葉

続けて、2つの提案を断り、公表すると告げたときの返答が記されています。

The reply was, “Why would you ruin your career?”

The reply was, “If you don’t want me to be nice, then I don’t have to be nice.”

バックマスター氏本人が置いている限定

ここを落とすと不公平になります。声明には次の段落があります。

I would like to be clear about what I am not claiming. I have not seen OpenAI’s proof. I do not know what their model did, or how. I do not know whether our data was used. I am not accusing anyone of anything.

「私は誰かを何かで告発しているのではない」。証明は見ていない、モデルが何をしたかも知らない、自分たちのデータが使われたかも分からない、と自ら限定しています。

ブベック氏は「一度も求めていない」と全面否定している

反論の側も逐語で押さえます。

4項目からなる反論を9月9日2時39分に投稿

ブベック氏は日本時間9月9日2時39分に、4項目からなる反論を投稿しました。表示回数は210万回を超えています。核心はこの一文です。

I never ever asked for Levent to be removed from authorship of his own work

「彼自身の仕事の著者から外すよう求めたことは、一度もない」。

言葉遣いについては本人が認めている

一方で、言葉遣いについては認めている部分があります。

extremely poor choice of words / I retracted them on the spot

極めてまずい言葉選びだった、その場で撤回したという趣旨です。「Why would you ruin your career?」については、根拠のない告発でキャリアを危険にさらす理由は何か、という文脈だったと述べています。

会議への出席についても主張が出ている

もう1点、こう書いています。

Levent refused to attend any of the meetings despite my repeated asking

繰り返し依頼したにもかかわらず、アルポゲ氏はどの会議にも出席しなかった、という主張です。

双方が認めている事実が4つある。出来事の骨格に争いはない

食い違いばかりではありません。両者が同じことを言っている部分を整理します。

双方が認めている4つの事実を並べる

私が両者の文書を突き合わせて確認できた一致点は、次の4つです。

• 9月6日に通話が行われたこと
• その通話にブベック氏が参加していたこと
• OpenAI側が同時公開を提案したこと
• バックマスター氏がそれを断ったこと

出来事の骨格については、争いがありません。

誰が先に接触したかも矛盾しない

一見食い違って見える点があります。声明では9月3日にバックマスター氏がOpenAIの数学者へメールを送ったとあり、OpenAIの発表ページには自社から接触したとあります。

これは矛盾しません。先に接触したのはバックマスター氏（9月3日）で、同時公開を提案するために接触したのはOpenAI（9月6日）です。順序が違うだけで、両立します。OpenAIの発表ページが9月3日の先行接触に触れていないのは、省略であって否定ではありません。

本当の食い違いは「プロンプトを何個見せたか」と「証明を見たか」

著者資格とは別に、検証可能な食い違いがあります。

OpenAIは「すべてのプロンプト」と書いている

発表ページにはこうあります。

In these discussions we offered them visibility into all of the prompts we used and later to see the proof.

使ったプロンプトすべてへの可視性を提供し、のちに証明も見せると申し出た、という趣旨です。

声明は「1つのプロンプト」と書いている

一方、声明にはこうあります。

I was shown a prompt and told the internal research model had simply been given the problem statement

I was told the proof is about 100 pages. I have not seen it.

見せられたのは1つのプロンプトで、証明は見ていない。そう書かれています。

ここは事実として食い違っている

「すべてのプロンプト」と「1つのプロンプト」、「見せると申し出た」と「見ていない」。

申し出と実際の閲覧は別のことなので、論理的には両立しうる余地があります。ただし読者が確認できる形の記録は、どちらの側からも公開されていません。

アルポゲ氏本人も投稿した。「ミレニアム賞を提示された」

当事者のもう一人も発信しています。

認証済みアカウントで9月9日2時57分に投稿

アルポゲ氏は認証済みのアカウントを持ち、4万人を超えるフォロワーがいます。日本時間9月9日2時57分、OpenAIの公式投稿を引用してこう書きました。

especially the part where a millennium prize was offered if i’d just be removed from the paper

「とくに、私が論文から外されさえすればミレニアム賞が提示された、という部分」。

OpenAIの「排除できない」という表現にも言及

同じ投稿で、OpenAIの記述にも触れています。

“we cannot rule out that de-identified data derived from their usage of our products helped improve our models.”

製品の利用から得られた非識別化データが自社モデルの改善に寄与した可能性は排除できない、という一文です。

これも当事者の一方の主張にとどまる

ただしこれも一方の当事者の主張であり、第三者の確認はありません。

バックマスター氏の声明にある表現とも言い回しが異なります。記事で扱うなら「アルポゲ氏の投稿によれば」と主語を付ける必要があります。

第三者による事実認定は、確認できた範囲で存在しない

ここが記事でいちばん慎重に書くべき点です。

私が探した範囲を先に書いておく

私が確認したのは、当事者3名の一次発信（声明PDF、X投稿、Mastodon投稿）、OpenAIの発表ページ、そして複数の報道です。

報道機関が独自に裏取りをして「どちらが正しい」と認定した記事は、確認できませんでした。

当事者以外の証言も記録も出ていない

通話に同席していた第三者の証言、録音、文書記録。いずれも公開されていません。

したがって書けるのは並置までである

「圧力があった」とも「なかった」とも書けません。

書けるのは「Aはこう書いた」「Bはこう否定した」「第三者の認定は確認できていない」という3つの事実の並置までです。この記事はその線を越えません。

formalization.yamlに「self-assessed」と書かれている

証明の検証状態に移ります。

OpenAI自身がyamlにそう記載している

公開されたリポジトリの設定ファイルに、こう書かれています。

review:
status: “self-assessed”

レビューの状態は「自己評価」です。

同じファイルには、自動化の手法としてエージェントが使われ、モデルはGPT-6 Astra、フレームワークはCodexと記載されています。

補足しておくべき点が1つだけある

この「self-assessed」は、形式化の記述規格における定型的な値でもあります。OpenAIが特別に何かを白状したわけではありません。

ただし「第三者がレビューした」とは書かれていないという事実は、そのまま読み取れます。

sorryはゼロだと「記載されている」

同じファイルには、証明の穴を表すsorryが0件、使用した公理が3つと記載されています。

これはOpenAIの自己申告です。私はLeanのビルドを実行していないので、独立には確認していません。「sorryがないことが確認されている」ではなく「sorryは0件だと記載している」が正確です。

Lean公式が「証明の正しさ」と「文の意味」を分けている

ここを落とすと決定的な誤報になります。

Lean公式ドキュメントの一文がこれ

Leanの公式リファレンスに、こう書かれています。

Furthermore it is important to distinguish the question “does the theorem have a valid proof” from “what does the theorem statement mean”.

「その定理に妥当な証明があるか」と「その定理文が何を意味するか」は、区別することが重要である。

形式検証が保証しないことは何か

つまり、Leanが通ったとしても、その定理文がクレイの公式問題文を正しく写しているかどうかは別問題です。そこは依然として人間の判断事項だ、と公式ドキュメントが述べています。

未レビューのAI生成証明の位置づけ

同じドキュメントには、リスクモデルの説明としてこうもあります。

This includes un-reviewed AI-generated proofs and programs.

これは本件以前から書かれている一般的な技術文書の記述で、特定の企業を指したものではありません。誤読しないよう、ここは明確にしておきます。

機械検証の登録簿Palomarには、9月9日朝も未登録だった

第三者検証の現在地を確認しました。

Palomarに9月9日8時32分時点で未登録

Lean検証済み数学の登録簿であるPalomarを、日本時間9月9日8時32分に確認しました。登録件数は212件、バージョンは250件。

最新200件を検索しましたが、OpenAI、Navier、Buckmaster、Alpogeのいずれの文字列も0件でした。該当リポジトリのページは404を返します。

未登録であること自体は不正を意味しない

念のため書いておきます。発表からまだ半日強しか経っておらず、登録は任意です。未登録であること自体は、何も悪いことを示しません。

そもそも登録されても査読ではない

さらに押さえておくべき点があります。Palomarの公式説明にはこうあります。

It does not accept, approve, or endorse a result. Palomar adds no human editorial step: no one here reads the mathematics the way a referee would.

結果を受理も承認も是認もしない。査読者のように数学を読む人間は誰もいない。そう明記されています。

匿名のフォークでビルドは通った。ただし最強の検査は手動

第三者の動きも1件確認できました。

身元不明のアカウントによるビルド

日本時間9月9日午前5時59分にリポジトリをフォークした匿名のアカウントが、GitHub Actionsでビルドを走らせています。日本時間7時43分46秒に、約100分かけて成功しました。

ビルドが通ったことが意味すること

ただしこれは「証明が正しいと確認された」ではありません。

実行者は身元不明の個人で、機関でも数学者でもありません。そしてビルドが通ることは、コンパイルが成功したことしか示しません。

最も強い独立検査はCIの外にある

そのフォーク自身の設定ファイルに、こう書かれています。

Comparator / nanoda (the strongest independent check …) needs the landrun sandbox and trusted-host setup, so it stays a manual process outside CI.

最も強い独立検査は、自動化の外の手動作業として残されています。別途走らせていた独立カーネル再検査は、私が確認した8時36分の時点でまだ進行中でした。

Leanの問題文はGoogle DeepMindの形式化から移植された

もう1点、興味深い事実があります。

出典はREADMEに明記されている

リポジトリのREADMEにこうあります。

Thank you to the Formal Conjectures authors for their Lean formalization of the Navier–Stokes problem statement, which we adapted for these Comparator challenges.

問題文のLean形式化は、Google DeepMindが公開しているものを適合させたものです。ファイル冒頭には、参照元のコミットハッシュまで書かれています。

参照元は発表より前から存在する

参照元のコミットは2026年7月27日付です。今回の発表より1か月以上前から存在していました。

変更は形式的なものにとどまっていた

両ファイルを比べた範囲では、相違はimport文、属性、名前空間、記法、そして不要な(A)(B)の削除にとどまり、数学的な中身は同一でした。

これは「定理文が恣意的に作られていない」ことの傍証にはなります。ただし、その定理文がクレイの公式問題文を正しく写していることの証明にはなりません。

賞金を請求しない理由は書かれていない。規則では2年かかる

賞金についての一行を確かめます。

賞金についての逐語は2文しかない

Our goal in releasing this result is to report on the substantial progress of our AI models. We do not intend to claim the Millennium Prize for this result.

「この結果についてミレニアム賞を請求する意図はない」。

請求しない理由は書かれていない

賞金を請求しない理由は、発表ページに明示されていません。直前の一文が文脈上の説明に読めるだけで、because や since のような因果を示す語はありません。

クレイの規則は公表から2年を求めている

一方、クレイ数学研究所の規則にはこうあります。

at least two (2) years have elapsed since publication of the Proposed Solution in a Qualifying Outlet

適格な媒体での公表から少なくとも2年が経過していること。加えて、世界の数学界による一般的な受容も条件に入っています。

この2つは事実として並べられますが、「要件を満たせないから請求しないと表明した」という因果を書いてはいけません。それはOpenAIが述べていない推測です。

クレイ数学研究所の公式サイトに、本件への言及はない

賞を出す側の反応も確認しました。

公式サイトの4ページを確認して記載なし

日本時間9月9日8時24分に、claymath.org のトップページ、ニュース一覧、ミレニアム問題のページ、規則のページの4か所を確認しました。

最新のニュース項目は2026年7月23日のフィールズ賞に関するもので、9月8日以降の項目はありません。本件への言及もありません。

会長のコメントは通信社宛のもの

一方、同研究所の会長がAFPの取材に答えたコメントが、複数の媒体に配信されています。

The process of evaluation is deliberately unhurried, and we shall ensure that it is absolutely rigorous.

評価の手続きは意図的に急がないものであり、絶対に厳密であることを保証する、という趣旨です。

ただしこれは「研究所が公式見解を出した」のではなく「会長が取材に答えた」ものです。そして本件の正否を評価した発言ではなく、手続きの姿勢を述べたものにすぎません。

オイラーの結果は別物。OpenAIは外力なし、2人は外力あり

混同されやすい点を整理します。

OpenAIのオイラー結果は外力なし版

発表ページにはこうあります。

Nearly 100 agents worked together for approximately 50 hours to produce our Euler regularity disproof.

その直前に、解決したのは「外力を加えない外力なし版」だと明記されています。

バックマスター氏らのオイラー結果

一方、バックマスター氏とアルポゲ氏が公開した3本のうちの3次元オイラーは、滑らかな外力つきの有限時間爆発です。

OpenAI自身が別物だと書いている

発表ページには、両者の結果についてオイラーの場合は証明された結果そのものが異なる（外力ありと外力なし）という趣旨の記述があります。

「2つのチームが同じ結果を争った」と書くのは誤りです。

読者が今日できること。Codexに入れたデータの扱いを確認する

実務に落とします。

この件で読者に直結するのはCodexの話

バックマスター氏は声明で、Codexに全ドラフトを投入していたと述べ、それが訓練に使われたか質問して回答を得られなかったとしています。

これは数学の話ではなく、AIツールに仕事のデータを預けている全員の話です。

まず自分のプランの既定値を確認する

まず確認すべきは、自分が使っているプランで入力データが訓練に使われる設定になっているかどうかです。

個人向けプランと法人向けプランで既定値が違います。設定画面のどこにその項目があるかを、一度自分の目で確かめておく価値があります。

未公開の成果を入れるかどうかを決めておく

もう1つ。まだ公表していない研究や企画を、どのツールのどこまで入れてよいかを、自分の中で線引きしておくことです。

今回の件で確定したのは、少なくとも「そこを気にした当事者がいた」という事実です。

いつ誰に何を伝えたかを記録に残す

3つ目。いつ、誰に、何を伝えたかを自分の側で記録しておくことです。

今回の食い違いが解けない理由の1つは、通話の記録が公開されていないことにあります。

総括：確定したのは経緯だけで、核心は誰も認定していない

ここまでの事実を1つの流れとして置きます。

9月8日12時58分に告発文が出て、19時にOpenAIの発表が出ました。順序は告発が先です。そして翌朝までに、当事者3名がそれぞれ発信しました。

骨格については争いがありません。9月6日に通話があったこと、ブベック氏が参加したこと、同時公開が提案されたこと、断られたこと。ここまでは双方が認めています。

食い違っているのは「著者から外すよう求めたか」の1点です。そして「見せられたプロンプトは1つか、すべてか」「証明を見たか、見ていないか」も食い違っています。第三者による認定は、私が確認できた範囲で存在しません。

構図についても、単純化はできませんでした。この共同研究は2025年9月19日、アルポゲ氏本人が「企業が最も深い純粋数学を所有する世界が怖い」という理由でバックマスター氏に送った1通のメールから始まっています。会社が仕掛けたものではありません。

証明についても、確定していることは限られます。OpenAI自身がレビュー状態を「self-assessed」と書き、機械検証の公的な登録簿には9月9日朝の時点で載っていません。Leanの公式ドキュメントは、証明の妥当性と定理文の意味は別問題だと明記しています。

引っかかるのは、その速さです。9月1日に噂を聞いて着手し、9月5日に到達し、9月8日に公開されました。クレイの規則が求める検証期間は、公表から2年です。

まとめ：9月9日時点で確定していること、していないこと

一次情報で確認できた事実だけを並べます。

OpenAIは日本時間2026年9月8日19時に、ナビエ–ストークス方程式について公式定式化の主張「C」（および「D」）を確立したと発表しました。(C)(D)は破綻を示す側の選択肢で、公式問題文は滑らかな外力の存在を明示的に許しています。

使ったのはGPT-6 Astraではなく、8月28日から訓練を続けている社内モデルです。約1万のオーダーのエージェントが88時間で解に到達し、Leanの形式化と検証にGPT-6 Astraがさらに17時間を要したと書かれています。全問題の合計で490万メッセージ・約3,000億出力トークン、ナビエ–ストークス単独で270万メッセージ・約1,300億出力トークンです。

着手のきっかけが噂だったことも、OpenAI自身が書いています。のちにアルポゲ氏とバックマスター氏に関係すると判明した噂だ、とも明記しています。

その発表の6時間前、日本時間9月8日12時58分に、バックマスター氏の4ページの声明が公開されていました。核心は「共著者を著者から外すよう2度求められた」という記述です。ブベック氏は「一度も求めていない」と全面否定し、言葉遣いについては「極めてまずい選択で、その場で撤回した」と述べています。

第三者による事実認定は、私が確認できた範囲では存在しません。通話の記録も公開されていません。書けるのは双方の主張の並置までです。

この共同研究は2025年9月19日に始まっていました。アルポゲ氏本人が「企業が最も深い純粋数学の仕事を所有する世界を、イデオロギー的な理由から恐れている」と書いてバックマスター氏に送ったメールが起点です。2人が使ったのは一般提供のClaudeとCodexだと、声明に書かれています。

証明の検証状態について、OpenAIはリポジトリに「self-assessed」と記載しています。sorryが0件であることも自己申告です。機械検証の公的な登録簿には9月9日8時32分の時点で未登録でした。Leanの公式ドキュメントは「妥当な証明があるか」と「定理文が何を意味するか」は区別すべきだと明記しています。

賞金を請求しない理由は書かれていません。クレイの規則は、適格な媒体での公表から少なくとも2年の経過を求めています。研究所の公式サイトには、本件への言及がありません。

あなたが仕事で使っているAIツールに、まだ公表していないものを入れたことはありますか。

よくある質問（FAQ）

Q1. 結局、ナビエ–ストークス問題は解けたのですか。
OpenAIは解決したと主張していますが、第三者による確認はまだありません。同社は公式定式化の主張「C」（および「D」）を確立したと述べており、これは解の存在と滑らかさを示す側ではなく破綻を示す側の選択肢です。公式問題文の(C)(D)は滑らかな外力の存在を明示的に許しているので、「外力があるから本物の問題ではない」とは言えません。一方で、証明の検証状態についてOpenAI自身がリポジトリに「self-assessed（自己評価）」と記載しており、Lean検証済み数学の登録簿には日本時間9月9日8時32分の時点で登録されていませんでした。Leanの公式ドキュメントは「その定理に妥当な証明があるか」と「その定理文が何を意味するか」は区別すべきだと明記しています。クレイ数学研究所の規則は、賞の対象になるために適格な媒体での公表から少なくとも2年の経過を求めています。

Q2. 「著者から外せと言われた」という話は本当ですか。
どちらとも言えません。NYUのトリスタン・バックマスター教授は日本時間9月8日12時58分に公開した4ページの署名入り声明で「Sebastien twice asserted that he wanted Levent removed from authorship of his own work」と書いています。一方でOpenAIのセバスチャン・ブベック氏は9月9日2時39分の投稿で「I never ever asked for Levent to be removed from authorship of his own work」と全面否定し、「Why would you ruin your career?」という発言については極めてまずい言葉選びでその場で撤回したと述べています。通話の記録は公開されておらず、報道機関が独自に裏取りをして認定した記事も、私が確認できた範囲では存在しません。なおバックマスター氏自身が声明で「I am not accusing anyone of anything.」と限定しています。

Q3. これはOpenAIとAnthropicの企業間の争いですか。
一次情報を見るかぎり、そう単純ではありません。共同研究の共著者であるレヴェント・アルポゲ氏は日本時間9月8日15時14分の投稿で、2025年9月19日付で自分がバックマスター氏に送ったメールのスクリーンショットを公開しました。件名は「Normal pure math collaboration with ai」で、動機として「Basically for ideological reasons I fear a world in which corporations are the ones with claim to the deepest pure math work」と書かれています。企業が最も深い純粋数学の仕事を所有する世界を恐れている、という個人的な理由です。共同研究は約1年前に個人の発意で始まっており、アルポゲ氏本人も「rather than anything institutional（組織的なものではなく）」と述べています。Anthropicの公式声明は、私が確認できた範囲では出ていません。

筆者より

この記事も、最初の見立てが検証で崩れました。

最初は「AI企業2社の代理戦争が学術界に持ち込まれた」で書くつもりでした。OpenAIが発表し、Anthropic社員を共著者に持つ研究者が同じ日に告発する。構図として分かりやすかったからです。

アルポゲ氏本人の投稿で崩れました。添えられていたのは、1年前に本人がバックマスター氏へ送った勧誘メールのスクリーンショットでした。動機は「企業が最も深い純粋数学を所有する世界が怖い」。会社の戦略ではなく、個人の危機感が起点でした。

次に「Leanで検証済みなのだから証明は正しい」という前提で書こうとして、これも崩れました。Leanの公式ドキュメントが、証明の妥当性と定理文の意味は別問題だと明記していたからです。そしてOpenAI自身が、レビュー状態を「self-assessed」と書いていました。

残ったのは、地味な確認作業でした。両者の発言を秒単位で時刻順に並べ、一致点と対立点を分け、第三者の認定を探すことです。

いちばん驚いたのは、認定が見つからなかったことです。これだけ大きな話で、当事者3名が実名で発信していて、それでも「どちらが正しいか」を独立に確かめた記録がありません。通話の記録も公開されていません。

もう1つ引っかかったのは、速さです。9月1日に噂を聞いて着手し、9月5日に到達し、9月8日に公開されました。一方でクレイの規則が求める検証期間は、公表から2年です。片方は日単位で動き、もう片方は年単位で動きます。

同時に、公平に書いておきたいこともあります。OpenAIは論文もLean形式化もリポジトリも公開しました。「self-assessed」と書いたのも同社自身です。隠していたら、私はここまで確認できませんでした。

そしてこの記事は「どちらが正しいか」を書いていません。書けないからです。そこを埋めたくなる誘惑がいちばん強かった、というのが今回の実感です。

参考資料

• OpenAI「On the Navier–Stokes Millennium Prize Problem」（生HTMLを取得し全文検索。公開時刻の根拠は公式RSSのpubDate＝協定世界時2026年9月8日10時00分。ページ本体にJSON-LDもdatePublishedも存在しないことを確認）
• 同発表にリンクされた証明論文PDFとオイラー論文PDF、およびGitHubリポジトリ openai/NavierStokesAndEuler（Apache-2.0）
• 同リポジトリの formalization.yaml（review status の記載、sorry_count、公理の記載を確認）および ComparatorChallenges/README.md
• google-deepmind/formal-conjectures の NavierStokes.lean（参照元コミットは2026年7月27日付。OpenAI版との差分を確認）
• トリスタン・バックマスター氏の署名入り声明PDF（cims.nyu.edu、Last-Modified＝協定世界時2026年9月8日3時58分30秒。Pythonのzlibで全4ページを抽出）
• セバスチャン・ブベック氏のX投稿（日本時間2026年9月8日15時43分、9月9日2時39分。投稿IDから本文と時刻を取得）
• レヴェント・アルポゲ氏のX投稿（日本時間2026年9月8日15時14分41秒、9月9日2時57分36秒。添付画像も確認）
• トリスタン・バックマスター氏のMastodon投稿
• テレンス・タオ氏のMastodon投稿とブログ（ブログの追記時刻はWayback Machineのスナップショットで確認）
• クレイ数学研究所「Millennium Prize Rules」（2018年9月26日改訂）および公式問題文PDF（Fefferman執筆。(A)〜(D)の原文を確認）
• claymath.org のトップページ、ニュース一覧、ミレニアム問題ページ、規則ページ（日本時間9月9日8時24分に確認。本件への言及なし）
• AFP配信記事（クレイ数学研究所会長のコメント。複数の配信先で同一文言を確認）
• Leanの公式リファレンス「Validating a Lean Proof」（証明の妥当性と定理文の意味の区別、リスクモデルの記述を確認）
• Palomar（Lean検証済み数学の登録簿）の一覧API（日本時間9月9日8時32分に確認。登録件数212件、該当リポジトリは404）およびPalomar公式の説明ページ
• GitHub Actions API（第三者フォークでのビルド実行の開始・終了時刻と結果を確認）
• Nature、Quanta Magazine、Engadget、TechCrunch、Scientific American、Fortune
• OpenAIおよびAnthropicのデータ利用に関する公式ドキュメント

※本記事の内容は2026年9月9日午前時点の公開情報に基づいています。この件は当事者による発信が続いており、記載した時刻以降に新しい発信が出ている可能性があります。本記事は「誰が何をいつ書いたか」を一次情報で確定することに徹しており、当事者の主張のどちらが正しいかについては判断していません。第三者による事実認定は、当事者3名の一次発信・OpenAIの発表ページ・複数の報道を確認した範囲では見つかりませんでした。通話の記録は公開されていません。証明の正しさについても本記事は判断していません。Lean形式化が公開されていることと、証明が正しいと確認されたことは別です。OpenAIはリポジトリのformalization.yamlにレビュー状態を「self-assessed」と記載しており、sorryが0件であることも同社の自己申告です。筆者はLeanのビルドを独立に実行していません。第三者フォークでのビルド成功は、コンパイルが通ったことを示すもので、定理文の妥当性を保証しません。クレイ数学研究所の規則に関する記述は同研究所が公開している規則文書と公式問題文に基づくもので、OpenAIが賞金を請求しない理由と規則の要件との因果関係については、原典に記載がないため判断していません。会長のコメントは通信社の取材に答えたもので、同研究所の公式サイトには本件への言及がありません。日付・時刻はすべて日本時間に換算しています。
※本記事について、事実関係の誤りや最新情報の追加などお気づきの点がございましたら、ぜひコメント欄でお知らせください。