OpenAI Navier-Stokes 候選解：Lean 形式化與研究信用爭議（2026）

2026 年 9 月 8 日，OpenAI 發布了〈On the Navier–Stokes Millennium Prize Problem〉，公開一份 OpenAI Navier-Stokes 候選解、166 頁分析證明與 Lean 形式化程式。它可能是 AI 參與新數學研究的重要轉折，但截至 2026 年 9 月 9 日，Clay 數學研究所仍把這道題列為未解；因此現在能確認的是「候選解已公開」，不是「千禧問題已獲承認解決」。

這篇文章分三步走：先忠實拆開定理到底聲稱什麼；再用 Clay 的正式題目、公開程式與認定規則逐項對帳；最後才判斷約一萬名代理、未公開模型與研究信用爭議真正改變了什麼。

OpenAI Navier-Stokes 候選解，究竟證明了什麼？

一句話版本：OpenAI 主張，對任意正黏滯係數，都能讓一個起初靜止的三維不可壓縮流體，在施加平滑、時空緊支撐的外力後，於有限時間內出現無界速度，同時保持動能有界。

“Our system produced an analytical proof and a Lean formalization.”

中文：我們的系統產出了一份分析證明，以及一份 Lean 形式化。

OpenAI，2026 年 9 月 8 日

這裡最容易被標題吃掉的兩個條件，是「有外力」與「速度無界、動能仍有界」。論文的 Theorem 1.1 不是說日常流體會在沒有推動時自行爆開，也不是一般數值模擬中的劇烈渦流；它構造的是一組非常精細的外力與流場，讓經典平滑解無法延伸過有限時間。

讀者常聽到的版本	公開手稿實際主張
證明無外力流體一定會奇異	構造一個有平滑外力的反例；無外力的 A、B 路線並未因此解決
能量爆炸	速度的最大值趨向無界，但總動能維持有界
繞過 Clay 題目	Clay 的正式題目本來就允許以 C、D 的有外力崩潰路線作答

所以，「有外力」不是偷換題目。Charles Fefferman 為 Clay 撰寫的正式問題敘述列出四條可能路線：A、B 要證明無外力時全域光滑；C、D 則允許選擇平滑外力，證明不存在全域平滑且符合能量條件的解。若 OpenAI 的每一步都正確，C、D 在形式上確實足以回答千禧問題；但它回答的不是大眾最直覺想像的「無外力流體會不會自行形成奇點」。

從一萬名代理到 88 小時：這些仍是 OpenAI 的自述

OpenAI 表示，內部模型自 8 月 28 日起訓練；Navier–Stokes 解題評測則在 9 月 1 日聽聞傳聞後啟動。不同代理群組分別探索 A、B、C、D 與較容易的相關問題，先得到無外力 Euler 方程的結果，再把中間洞見交叉彙整到 Navier–Stokes。公司稱，最後產出候選解的群組約有一萬名同時運作的代理，約 88 小時後得到結果，再以 GPT-6 Astra 花 17 小時做 Lean 形式化與驗證；單是 Navier–Stokes 階段，就產生約 270 萬則訊息與 1,300 億個輸出 token。

同一篇公告還稱，核心使用的是一個仍在訓練、未具名的內部模型，能力顯著高於 GPT-6 Astra。截至 2026 年 9 月 9 日，OpenAI 連結的公告、論文與 GitHub 儲存庫提供了結果檔案，但沒有附上完整提示、代理通訊、失敗分支、算力配置或可重跑的代理執行紀錄。因此，這些數字能證明的是 OpenAI 如何描述自己的研究管線，不能當成第三方已稽核的模型能力測量。

手稿的直觀圖像，是把渦旋層不斷向內壓縮，同時沿軸向拉伸，使更小尺度的旋度持續放大；再用多層振盪修正抵消殘差，讓外力仍保持平滑。真正的難度不在畫出一個越轉越快的渦，而在證明所有修正能同時收斂、外力的每階導數受控、解在爆破前保持平滑，且動能不發散。

Lean 讓證據更硬，但不會自動頒發「正確」

這份 OpenAI Navier-Stokes 候選解最有分量的地方，是 OpenAI 沒只貼一篇宣傳文，而是同步公開Lean 儲存庫。本文把唯讀盤點固定在 2026 年 9 月 8 日的提交 8937a8f：整個 Navier–Stokes 與 Euler 儲存庫共 2,486 個 .lean 檔、約 61.6 萬行；形式化中繼資料把主要結果標成零個 sorry，也同時把審查狀態寫成「自我評估」。儲存庫另有四個刻意留給 comparator 挑戰的 sorry 位置，並非主要定理的依賴。

Lean 的核心價值，是要求每一步都產生可交給小型核心檢查器驗證的證明項。這大幅降低「某個細節藏在 166 頁文字裡」的風險。不過，Lean 官方的證明驗證說明也提醒了一個必要邊界：核心檢查的是形式定義與定理之間是否成立；人仍要審核形式定義是否忠實對應原來的偏微分方程、分析假設與 Clay 的命題，並由獨立環境實際建置。

本次環境沒有儲存庫指定的 Lean 4.34.0-rc2 與 Lake，因此本文沒有把唯讀檔案盤點包裝成「已重現」。更精確的結論是：一份規模可觀、可供機器檢查的證明工件已經公開；它比單純手稿更容易被逐條攻擊，但截至 2026 年 9 月 9 日，該儲存庫的 GitHub Actions API回傳 0 次工作流程執行，尚不能替代第三方建置與數學審查。

為什麼 Clay 仍寫著「未解」？

截至 2026 年 9 月 9 日，Clay 的 Navier–Stokes 頁面仍標示「Unsolved」。這不是 Clay 已判定 OpenAI 手稿錯誤，而是機構認定本來就不會在公告隔天完成。

依照 Clay 公開的千禧問題規則，候選解要先出現在合格出版管道；出版後至少經過兩年，並在全球數學界取得普遍接受，Clay 才會進入正式考慮。OpenAI 的網站與 GitHub 發布提供了審查材料，卻不等於已走完這條路。OpenAI 自己也明言不打算申領獎金。

信用爭議不是「誰先解出同一題」這麼簡單

同期研究者是 NYU 數學家 Tristan Buckmaster 與 Levent Alpöge；公開質疑則由 Buckmaster 以第一人稱提出。兩人同期共同宣布平滑外力下的 Boussinesq 與三維 Euler 爆破結果；不可壓縮多孔介質論文另有 Matei P. Coiculescu 共同署名。他們並表示另有次耗散（hypodissipative）Navier–Stokes 工作尚未完成 Lean 驗證；那不是 OpenAI 這份任意正黏滯 Navier–Stokes 定理的同一個已公開結果。

日期	公開可核對的說法
8 月 15 日	Buckmaster 稱，他與 Alpöge 得到平滑外力 Boussinesq 與 Euler 爆破結果
8 月 22 日	Buckmaster 稱，兩人完成上述結果的 Lean 驗證
9 月 1 日	OpenAI 稱，聽到兩道千禧問題可能被解出的傳聞後啟動探索
9 月 3 日	Buckmaster 稱，他主動寫信給 OpenAI 內部數學家澄清兩人的工作範圍
9 月 5–6 日	OpenAI 稱，代理完成 Navier–Stokes 候選解與 Lean 驗證；Buckmaster 稱雙方於 9 月 6 日通話
9 月 8 日	OpenAI 公告、論文、Lean 儲存庫與 Buckmaster 聲明都已公開

Buckmaster 的第一人稱聲明提出三層質疑：他主張，這套多尺度、跨尺度放大的強迫爆破計畫承接 Diego Córdoba 與 Luis Martínez-Zoroa 的先行工作；OpenAI 的啟動時間晚於相關傳聞流出；他曾把未公開草稿放進 Codex，因此追問這些資料是否進入模型訓練。他也把自己能證明到哪裡說得很窄：

“I do not know whether our data was used. I am not accusing anyone of anything.”

中文：我不知道我們的資料是否被使用；我沒有指控任何人做了任何事。

Tristan Buckmaster，2026 年 9 月 8 日

OpenAI 的回應同樣需要精確拆字：公司稱研究人員與代理在兩人公開工作前都沒有看到相關內容，這次解題也沒有查看兩人的特定使用者資料；公司還稱曾提議讓對方查看提示與證明，並在聯合公告中承認對方工作的優先性。但 OpenAI 也承認，無法完全排除由產品使用衍生的去識別化資料曾改善模型。前兩項是 OpenAI 對過程的說法；最後一項留下歷史訓練資料來源問題。公開證據目前不足以證明草稿被挪用，也不足以把「沒有直接查看」擴張成「訓練完全不可能受益」。

更重要的是，Clay 的 C、D 路線與 Córdoba、Martínez-Zoroa 的先行論文本來就已公開，OpenAI 手稿的歷史回顧也確實引用這些強迫爆破解法。因此，只看到「有外力」、渦旋或多尺度方法相近，還不足以推出未公開資料被使用；需要逐項比較 ansatz、引理與消去機制。真正有爭議的是發布敘事是否充分呈現前史、傳聞如何影響選題與算力配置，以及模型供應商該如何證明未公開研究資料的邊界。

AlphaLab 的判讀：這是驗證制度的壓力測試

1. 最強訊號不是「一萬名代理」，而是可攻擊的公開工件

代理數、token 與內部模型排名都由 OpenAI 單方掌握；論文與 Lean 程式則允許外部研究者指出一個具體錯誤。科學可信度不該隨算力敘事上升，而應隨可重建、可對照、可反駁的證據上升。這次發布比只給 benchmark 分數前進了一大步，但最後一哩仍是獨立審查。

2. 「模型解題」其實是模型、代理系統與人類選題共同產物

OpenAI 的描述包含題目拆分、相關簡化題、代理分組、跨群彙整、模型中途升級與 Lean 驗證。這不是一個聊天視窗收到題目後靈光一閃，而是一套大型研究搜尋系統。論文只以「OPENAI」署名，公開 Git 歷史也只有一個提交；若未來只把成果歸因於公司或模型名稱，會掩蓋提示設計、算力、工具、選擇壓力與數學研究者的具體判斷。

3. 信用應拆成成果、路線、驗證與資料來源四本帳

OpenAI 可以因公開這份特定候選證明與形式化工件獲得成果信用；公開紀錄至少支持把 Córdoba、Martínez-Zoroa 列為這套多尺度構造的重要先行者，精確優先權仍需逐項比對證明；Alpöge、Buckmaster 的同期推進有獨立的結果與時間線；而 Lean 工件的可信度，最終要由外部建置與逐一定義審查累積。資料來源則另立一帳，不能靠成果新穎性自動結清。

4. 真正的里程碑要等「人能理解」追上「機器能檢查」

形式證明能把邏輯縫隙壓到極小，卻可能把理解成本推進大量形式化程式。若數學界只能相信檢查器輸出的綠燈，卻說不清新機制為何有效，成果仍難以變成可傳授、可延伸的知識。接下來最有價值的工作，不只是找 bug，也包括把候選證明壓縮成數學家能重用的引理與直覺。

我同意的部分：公開分析手稿、形式化程式與精確定理範圍，是 AI 科學成果應有的證據起點；若獨立審查成立，這會是 AI 從解題基準跨入新數學的重大案例。

我存疑的部分：用未公開模型的內部比較與龐大代理數，提前替數學正確性與模型能力背書。兩者都缺少外部可重跑資料，而且目前甚至尚未滿足 CMI 正式考慮的前置條件。

現在該看哪四個訊號？

1. 獨立建置：不同團隊能否用固定提交與指定工具鏈重建 Lean 工件，並公開完整日誌。
2. 定義對齊：偏微分方程專家能否確認形式化命題、正則性條件、唯一性與週期化步驟完整對上 Clay 的 C、D。
3. 可讀證明：166 頁論證能否被壓縮成清楚的關鍵引理，讓專家不依賴原作者也能重建核心機制。
4. 研究資料治理：模型供應商能否提供比口頭保證更可稽核的訓練資料、產品資料隔離與優先權處理規則。

對研究者而言，未公開草稿不只要保存版本與時間戳，也要記錄曾送進哪些模型、採用哪種資料控制與帳戶設定；對讀者而言，最可靠的判斷順序是「定理範圍 → 公開工件 → 獨立重建 → 社群接受」，而不是從公司公告直接跳到「問題已解」。