關於納維－斯托克斯千禧年大獎難題

我們現分享納維－斯托克斯存在性與光滑性問題的解法。這是千禧年大獎難題之一。這項證明由 OpenAI 內部系統得出，顯示在描述流體運動的納維－斯托克斯方程下，流體的動力學演化可在有限時間內產生奇點。我們同時分享詳述這項證明的論文及其 Lean 形式化版本。

千禧年大獎難題⁠（在新視窗中開啟）涵蓋數學前沿中一些最深奧的問題。原本光滑的三維流體運動會否失去光滑性，約 90 年來一直懸而未決。

我們工作的主要目標之一，是協助科學家推進惠及全人類的研究與技術。為解決納維－斯托克斯問題，我們採用了一個能力遠勝 GPT‑6 Astra 的內部模型。我們認為，讓全球了解 AI 的發展速度，以及可以對即將推出的模型有甚麼期望，至關重要。

納維－斯托克斯方程運用牛頓第二運動定律（「F=ma」）描述流體如何運動。重要的是，這些方程把流體視為連續介質，而非追蹤個別分子。這些方程式用於飛機設計、天氣預報和血流研究。

這些動力方程式一直有一項尚待解答的根本問題：把流體視為連續介質的近似方法會否失效。具體而言，即使運動起初光滑，描述密度恆定的三維不可壓縮流體的納維－斯托克斯方程，會否產生「奇點」？這裏的奇點，是指流體速度隨動力學演化，在有限時間內無限增長。黏性通常會令運動趨於平滑，因此奇點若要形成，就必須在黏性仍然存在的情況下出現。真實流體不可能以無限速度運動，因此這代表方程式對流體的描述失效。此後如要繼續為該系統建立模型，便需要逐一追蹤每個粒子的行為。

這些方程式源自 Claude-Louis Navier 和 George Gabriel Stokes 在十九世紀的研究。1934 年，Jean Leray 證明廣義解存在，但這些解是否總能保持光滑，則成為一項尚待解答的核心問題。2000 年，Clay Mathematics Institute 把納維－斯托克斯存在性與光滑性問題列為七項千禧年大獎難題之一。

我們的系統得出了分析證明及 Lean 形式化版本，證明起初靜止且光滑的流體可在有限時間內產生奇點。流體受到光滑的力作用，而從靜止到形成奇點的整個動力演化過程中，其能量一直保持有限。這項成果確立了千禧年大獎官方問題陳述⁠（在新視窗中開啟）中的命題「C」（以及「D」），從而解決納維－斯托克斯千禧年大獎難題。

這個解是一個渦旋，即旋轉的流體漩渦，會向內螺旋收縮，並像意大利粉般愈拉愈長。其中心區域一面縮小，一面加速，而能量仍按物理定律的要求保持有限。技術上的挑戰，在於讓流體本身的運動導致方程的描述失效，而不是例如由我們人為加入無限大的力。用數學語言來說，納維－斯托克斯方程式中描述運動的各項，包括加速度、壓力梯度、動量傳遞和黏性，必須同時變得很大，卻又以精確方式互相抵消。這種精細平衡令外力保持光滑，即使流體速度無限增長亦然。

自 8 月 28 日起，我們一直在訓練一個新的內部模型。這個模型在我們包括數學測試的基準測試中，展現了前所未有的表現。目前訓練仍在進行，模型表現亦持續提升。

9 月 1 日星期二，我們聽聞有兩項千禧年大獎難題已獲解決的傳聞。受到這些傳聞及內部模型表現躍升的啟發，我們開始評估模型處理所有尚未解決的千禧年大獎難題，以及另外數項影響深遠的問題時的表現。

我們採用了一套由內部模型驅動、可互相協調的智能代理系統。智能代理可使用多種工具，包括讀取互聯網快取版本及執行程式碼。智能代理分成多個小組，並可在組內溝通。各組規模不一；得出納維－斯托克斯問題解法的一組，約有 10,000 個智能代理同時運作。我們全程維持評估所有前沿模型時採用的同等嚴格保障措施，包括監察與隔離。

對於每個問題，我們向不同的智能代理小組提供不同版本的問題陳述作為提示詞，涵蓋問題的所有變體。針對納維－斯托克斯問題，我們向不同小組分別提出版本「A」和「B」（這些特定形式對應的是證明命題成立），以及版本「C」和「D」（對應的是證明命題不成立）。

除了完整的千禧年大獎難題，我們亦要求多智能代理系統嘗試處理一組「較容易」的問題。其中一項是在移除黏性項後的納維－斯托克斯極限情況下，研究解會否同樣變得無界。這稱為歐拉方程式的正則性問題；令我們意外的是，智能代理解決了這個問題。智能代理解決的具體變體是無外力版本，即沒有外力施加於流體。近 100 個智能代理協作約 50 小時，得出了推翻歐拉方程式正則性命題的證明¹。

看到歐拉問題的解法後，我們認為納維－斯托克斯是最有希望取得成果的問題。因此，我們決定把資源集中於納維－斯托克斯問題。為此，我們把原本處理其他千禧年大獎難題的智能代理調配過來，並向這些智能代理提供歐拉問題的解法作為提示詞。工作期間，內部模型經進一步訓練的新版本可供使用後，我們便讓智能代理改用該模型。

我們鼓勵不同的智能代理小組探索多種方法。一段時間後，我們使用 Codex 整合各組最有用的見解，讓各組互相借鑑。這些後續提示詞運用了智能代理本身得出的中間成果。找到納維－斯托克斯問題解法的小組，就是以這種方式獲得引導。

智能代理於 9 月 5 日星期六得出解法，距首批智能代理啟動約 88 小時。其後使用 GPT‑6 Astra 進行 Lean 形式化與驗證，另需 17 小時。

在嘗試處理的所有問題中，智能代理共傳送 490 萬則訊息，使用約 3,000 億個輸出 Token。在解決納維－斯托克斯問題的過程中，智能代理傳送了 270 萬則訊息，使用約 1,300 億個輸出 Token。

我們在 9 月 1 日聽聞一項傳聞後展開工作，其後才得知這項傳聞與 Anthropic 員工 Levent Alpöge 及 NYU 數學教授 Tristan Buckmaster 有關。² 我們於 9 月 6 日完成整個項目及 Lean 驗證後，由於根據傳聞相信他們亦已找到納維－斯托克斯問題的解法，便聯絡二人，提議同步發表成果，並在聯合公告中承認他們率先取得成果。這時我們才得知，他們使用 Anthropic 內部模型，解決了有外力作用的歐拉問題。討論期間，我們提出讓他們查看我們使用的所有提示詞，其後亦提出讓他們查看證明。我們承認他們率先取得有外力歐拉問題的研究成果，並祝賀他們取得卓越的數學成就。

在他們公開發表成果前，我們（研究人員及智能代理）從未透過任何途徑看過其研究；尤其是，我們並無為解決這個問題而存取任何特定用戶資料。

經調查後，我們確認，在我們於 2026 年 9 月 8 日發表這項公告和論文之前的兩個月內，Buckmaster 輸入的 Codex 提示詞不可能以任何方式影響這個系統，包括透過訓練造成影響。得出這項成果的 OpenAI 內部模型，是以先前已完成預訓練的模型為基礎，透過大規模強化學習開發而成。我們的證明亦有重大差異。在歐拉問題上，Alpöge 和 Buckmaster 證明的是有外力作用下的結果，而 OpenAI 系統證明的則是無外力作用下的結果。

我們發表這項成果，是為了報告我們的 AI 模型取得的重大進展。我們無意憑這項成果申領千禧年大獎。

這項里程碑凝聚了數學家與 AI 研究人員的大量工作。然而，這並非終點，而只是 AI 發展進程在此刻的縮影。

我們相信 AI 發展現已進入下一階段⁠，今天的成果進一步印證了這一點。我們正致力了解這個模型，並運用所學，引導我們進一步提升能力的方式與步伐。我們的主要目標⁠之一，是建立可引導、可問責並與人連繫的 AI 系統。隨着我們繼續履行確保 AGI 惠及全人類的使命，這或會要求我們更審慎地決定發展步伐。