OpenAI 宣佈系統完成了對百年數學難題的 lean 證明

OpenAI 宣佈，其內部 AI 系統針對著名的納維爾–斯托克斯存在性與光滑性問題給出了一個新的結果，並公開了論文以及 Lean 形式化證明。

納維爾–斯托克斯方程描述的是水、空氣等流體的運動，也是現代流體力學的基礎。

如果初始狀態足夠平滑，那麼三維流體的運動是否會永遠保持平滑？

這是克雷數學研究所（Clay Mathematics Institute）七大千禧年大獎難題之一，懸賞金額爲 100 萬美元。