Clay Institute 審查 OpenAI 的 AI 生成 Navier–Stokes 解法

Clay Mathematics Institute 表示，Navier–Stokes 千禧年獎問題「似乎已經解決」，但尚未宣布該問題已解決，也未頒發其 100 萬美元獎金。該機構正開始正式審查一項工作；OpenAI 將其描述為由 AI 生成的解法，並附有書面論證與以 Lean 撰寫的形式化證明。

這項發展意義重大，因為 Navier–Stokes 問題是 2000 年宣布的七項千禧年獎問題之一。它詢問用來描述三維空間流體運動的方程，在相關條件下是否總能產生光滑且完整的解。若能成功證明，將解決一個數十年來懸而未決的問題，並成為一項嚴格測試，檢驗先進 AI 系統是否能為原創數學研究作出貢獻。

一個可能的解法進入刻意緩慢的程序

Clay Mathematics Institute 表示，該結果目前正在審查中，並強調其程序是「刻意不急不躁」的。該機構未指明最終裁定，未公布獨立驗證，也未確認是否已滿足獎金條件。該機構表示，隨著評估持續進行，會提供最新進展。

這個區分很重要。在數學中，一項提議中的證明可以在尚未被接受為正確之前，就被流通、形式化並由專家檢視。審查必須確認論證處理的是精確的問題陳述，其假設有效，而且推理中沒有留下任何缺口。

OpenAI 的官方帳號將這項工作呈現為一個針對 Navier–Stokes 千禧年獎問題的 AI 生成解法。該公司表示，其提交內容同時包含一般性文字說明與 Lean 中的形式化證明；Lean 是一種證明助理系統，用於將數學論證以可由機器檢查的形式表達。Lean 形式化可以增強人們對編碼步驟遵循系統規則的信心，但它本身無法判定形式化命題是否完全符合原始挑戰，或建模選擇是否恰當。

為何這項主張不僅僅關乎一個定理

這項宣布向 AI 開發者與研究者提出了一個高度關注的問題：模型能否從產生看似合理的數學文本，進一步構建出能經受專家審查與形式驗證的結果？

Navier–Stokes 問題尤其艱難，因為它涉及三維中非線性偏微分方程的行為。一項有用的結果不只是證明 AI 能生成方程或提出證明策略，而是要顯示 AI 輔助工作流程能在一個被選為人類數學能力基準的問題上，支持發現、嚴謹闡述與形式檢查。

對產品團隊而言，更實際的問題是工作流程設計。即使系統提出了一個證明，仍需要人類數學家來定義目標、檢查抽象、測試邊界情況，並解讀機器驗證的產物是否真正捕捉了預期定理。因此，價值或許不在於取代研究者，而在於縮短從猜想、實驗到驗證之間的路徑。

證據仍然有限且具爭議

來源材料中最強且已確認的證據是程序性的：Clay Mathematics Institute 承認該問題似乎已被解決，並表示審查正在進行中。這並不是對正確性的獨立確認。OpenAI 對 AI 生成解法與 Lean 證明的描述，是來自公司自身公告的主張，而來源材料並未提供完整證明、系統技術細節或外部專家評估。

The Decoder 也報導了圍繞這項工作的爭議。根據該刊物，數學家 Tristan Buckmaster 指控 OpenAI 在有關其研究的傳聞外洩後，將資源轉向該問題、把他的草稿用於訓練資料，並將共同作者 Levent Alpöge 排除在作者名單之外。就目前可得證據而言，這些指控尚未被證實，而 OpenAI 的說法也不應被視為已解決這些爭議。

作者歸屬與資料使用的問題，幾乎可能與數學裁定同樣重要。即使證明被接受，研究者仍會想知道系統是如何產生它的、有哪些人類貢獻、哪些材料影響了結果，以及誰應獲得功勞。當 AI 系統是以大量數學著作訓練，且可能涉及研究者未公開的草稿時，這些問題尤其敏感。

對 AI 研究與企業使用的影響

若審查成功，將提高 AI 輔助研究 的上限，但不會消除機構控管的必要。將 AI 部署於科學或工程工作的組織，將需要來源紀錄、明確的作者政策、可重現的評估，以及將模型輸出與已驗證結果區分開來的審查程序。

這件事也凸顯了以基準測試為導向的宣布之限制。形式化證明或許比非正式的模型回答更容易稽核，但其周邊的研究流程仍然難以評估。買家與研究主管應該詢問系統是否能解釋其依賴關係、保留完整的機器與人工編輯材料軌跡，並支援獨立重現。

對 AI 公司而言，此案可能加劇數學推理與證明助理方面的競爭。但 Clay 的審查提出了比公開展示更高的標準：該工作必須經得起不會輕易接受供應商敘事的專家檢驗。在那之前，較恰當的說法是這是一項嚴肅的提議解法，而不是已確認的突破。

接下來要關注什麼

最直接的訊號是 Clay Mathematics Institute 的審查。其未來更新應能釐清提交的論證是否符合問題的官方表述，以及獨立數學家是否發現缺口。

研究者也會關注完整證明的發布、關於 AI 系統的技術細節，以及外部專家可檢視的可重現 Lean 產物。進一步報導也可能釐清據稱使用研究草稿的情況，以及 Tristan Buckmaster 與 Levent Alpöge 的角色。

最後的里程碑將是該機構的正式確認，以及對 Millennium Prize 的任何決定。在此之前，對該系統數學能力的說法仍屬供應商報導或初步報導，而非已被接受的定理。

Creati.ai 觀點

這則故事之所以重要，是因為它測試的是比流暢回答或單一基準分數更有意義的 AI 表現。如果結果能通過審查，AI 生成的發現、人類數學判斷與可由機器檢驗的證明之結合，可能成為高風險研究工作流程的範本。

目前的證據仍然值得保持克制。Clay Mathematics Institute 已表明有重要內容正在審查，而 OpenAI 則提供了核心技術主張。下一階段——獨立驗證、透明的來源，以及清楚的作者歸屬說明——將決定這究竟是一項經過驗證的數學成就，還是一項仍待修正的雄心提案。