OpenAI 宣稱 AI 系統產生了以 Lean 形式化的 Navier–Stokes 否證

OpenAI 表示，一套內部 AI 系統已產生一項分析性證明，顯示三維不可壓縮流體運動可能在有限時間內形成奇點，從而處理了 Navier–Stokes 存在性與光滑性問題。公司已發布一份書面論證與一份以 Lean 形式化的版本，但根據現有證據，這項主張尚未經獨立驗證。

這項宣布之所以重要，是因為 Navier–Stokes 問題是七大千禧年獎難題之一，這組數學挑戰由 Clay Mathematics Institute 於 2000 年提出。若能正確解答，將不僅影響自動化數學研究的極限，也會影響 AI 系統如何被測試來面對那些人類研究者數十年來都未能解決的問題。

OpenAI 的貼文是本報導的主要來源。隨附的 wire 稿在可取得的材料中沒有額外文章內容，因此關於系統表現、規模與結果的最強主張，皆來自供應商的說法。

OpenAI 聲稱它解決了什麼

OpenAI 表示，其系統建立了這樣一個問題版本：一個平滑、初始靜止的流體在受到平滑外力且保有有限能量的情況下，會在有限時間內形成奇點。依公司描述，這項結果證明了 Navier–Stokes 問題官方表述中的「C」與「D」命題，這意味著它是否定普遍光滑性，而不是證明所有解都保持正則。

所提出的機制是一個渦旋向內捲曲，並沿其軸向拉伸。當中心區域收縮時，流體速度在數學模型中會無限增大。OpenAI 表示，這項構造依賴加速度、壓力、動量傳遞與黏滯項變大，同時又以精確方式相互抵消。外力仍保持平滑，這表示所聲稱的崩潰是由流體動力學本身產生，而不是直接插入一個無限大外力。

Navier–Stokes 方程以牛頓運動定律將流體建模為連續介質。工程師與科學家將其用於飛機設計、天氣預報與血流分析等領域。尚未解決的問題是：一個平滑的三維不可壓縮、定密度流動是否必須永遠保持平滑。

一場大型多代理實驗

根據 OpenAI 的說法，這項工作於 9 月 1 日開始，當時公司聽聞兩個千禧年獎難題已被解決的傳言。之後，公司指示一套協調系統的 AI 代理去檢視所有尚未解決的問題與若干相關問題。

公司表示，Navier–Stokes 工作大約動用了 10,000 個同時運作的代理。這些代理被分成不同群組，獲得不同的問題表述，並可使用包括快取版網際網路與程式碼執行在內的工具。OpenAI 表示，這些代理在整合最有前景的工作之前，曾同時探索證明與否證兩種變體。

OpenAI 也報告，整體專案產生了 490 萬則訊息，並使用了約 3000 億個輸出 tokens。就 Navier–Stokes 工作本身而言，則報告了 270 萬則訊息與約 1300 億個輸出 tokens。這些數字描述的是公司內部實驗，並非經獨立審計、可衡量有用數學推理的指標。

公司表示，代理在約 88 小時後於 9 月 5 日達成 Navier–Stokes 結果。根據 OpenAI，Lean 形式化與驗證又透過 GPT-6 Astra 花了另外 17 小時。公司表示，在搜尋過程中，Codex 被用來整合不同代理群組的洞見。

形式驗證是證據，不是最終接受

Lean 成果是 OpenAI 揭露內容中的重要部分，因為形式化可以暴露出在一般研究草稿中可能被保留下來的缺失假設與無效步驟。不過，單靠它本身無法決定形式化後的陳述是否正確對應官方的千禧年獎問題表述，或實作是否在定義、引入的引理或假設上存在錯誤。

OpenAI 已公開證明草稿與 Lean 形式化，但提供的證據並不包含 Clay Mathematics Institute 或獨立數學家的審查。公司明確表示，無意就此結果申請千禧年獎。這個區別很重要：公開的 AI 生成證明是一項研究主張，而獲得獎項認可則需要專家審查並依據該機構規則接受。

時機也使得歸屬需要謹慎。OpenAI 表示，它是在聽聞與 Anthropic 員工 Levent Alpöge 以及紐約大學數學教授 Tristan Buckmaster 相關的傳聞後，開始這項工作的。公司說，他們的工作關涉的是 forced Euler，而不是相同的 Navier–Stokes 結果，而且兩項工作在方法與精確結論上都不同。OpenAI 表示，在公開發布前並未存取他們特定的使用者資料或工作內容，但也承認無法排除去識別化的產品資料曾幫助改善其模型。

這項結果對 AI 建構者可能意味著什麼

對 AI 開發者而言，值得注意的變化不只是模型產生了數學文字。OpenAI 描述了一種工作流程：許多代理獨立探索表述、交換中間結果、使用軟體工具，並將候選證明交給形式驗證系統。這種架構更像自動化研究管線，而不是單一聊天機器人回應。

這種方法也凸顯了其成本與營運風險。數千億個生成 tokens 與數千個同時代理，對高價值研究基準來說或許可行，但與一般軟體產品的經濟性相去甚遠。建構者必須衡量平行探索究竟是否帶來真正的新見解，還是只是增加了看似合理、但重複的推理量。

對企業買家而言，這起事件再次強調了模型「提出結果」與組織「信任結果」之間的差異。在科學與工程工作流程中，可重現的成果、可由機器檢查的證明、專家審查，以及清楚記錄的假設，比基準分數或代理執行規模更重要。Lean 形式化可以支援這個流程，但不能取代領域專業知識。

這項宣布也是一個競爭訊號。OpenAI 表示，內部模型比 GPT-6 Astra 更強，而其訓練仍在進行中。由於這些能力比較來自 OpenAI，因此應被視為內部或供應商報告的主張，而非已定案的市場衡量。

接下來應觀察什麼

第一個訊號將是對已公開證明與 Lean 程式碼的獨立檢視，尤其要看其構造是否滿足官方 Navier–Stokes 陳述中的每一項條件。若形式證明依賴於一個微妙不同的定義域、外力條件或奇點概念，就不能解決同一個問題。

第二個則是數學家是否能重現結果、找出漏洞，或確認形式化可編譯且忠實編碼了該論證。Clay Mathematics Institute 的回應也能釐清此工作是否符合認可標準。

研究人員也應留意 OpenAI 是否會釋出足夠的實作細節，以便重現這場多代理搜尋，包括模型版本、提示詞、工具邊界與算力帳務。若缺少這些資訊，所報告的代理數量與 token 總數只能提供背景，對於打造類似系統的團隊幫助有限。

Creati.ai 觀點

OpenAI 的宣布最好被理解為一項重要的能力主張，而不是已經成立的數學事實。代理協調、程式碼工具與 Lean 形式化的組合，是 AI 輔助研究的一條可信方向，但核心結果仍取決於該公司之外的審查。

對建構者而言，實務上的教訓比標題更具體也更有用：先進的 AI 研究系統需要驗證層、明確的問題規格，以及獨立審查。若這些控制機制能在此結果上站得住腳，這起事件可能成為機器輔助數學的重要案例。若不能，它將說明為何流暢的證明與外觀正式的成果物，無法取代數學驗證。