克雷數學研究所發布公告，指出納維-史托克斯方程的存在性與光滑性問題「似乎」已獲解，並啟動千禧年大獎的審查程序。此進展源於 OpenAI 使用 Lean 4 系統產生的形式化證明。儘管被視為數學與人工智慧領域的里程碑，且可能提升 AI 在形式化驗證中的可信度，但由於該成果尚未正式發表，千禧年大獎的兩年審查計時尚未開始。公告措辭謹慎，特別使用「似乎」一詞且未明確提及 OpenAI，反映出對歸屬權爭議的考量。

事件背景

納維-史托克斯方程的存在性與光滑性問題是七個千禧年大獎問題之一，旨在證明三維空間中描述流體運動的方程是否存在光滑解。這些方程是物理學和工程學的基礎，但對其理解仍不完整，特別是關於湍流的特性。克雷數學研究所為首個正確解答提供一百萬美元的獎金。

社群觀察

社群成員指出，根據規則，證明必須在合格刊物上發表後，審查計時才會正式開始。大家熱烈討論公告中避免提及 OpenAI 的謹慎措辭，認為這是在爭議平息前的中立做法，並就研究人員在形式化驗證前能否完全信任 AI 產生的證明展開辯論。