研究與評測
OpenAI 發布 AI 生成的千禧年大獎難題 Navier-Stokes 解答與 Lean 形式化證明
OpenAI News一手來源
核實資料不足
來源為發布方或研究資料；不代表所有主張已獲獨立核實。
查證回合用盡，未形成有依據結論
OpenAI 宣布發布由 AI 生成的千禧年大獎難題 Navier-Stokes（納維-斯托克斯方程式）解答。官方表示，此次公布的成果包含完整的分析報告（writeup），以及使用 Lean 語言編寫的形式化證明。
讀原始報導背景
納維-斯托克斯存在性與平滑性問題（Navier–Stokes existence and smoothness）是克雷數學研究所提出的七大千禧年大獎難題之一。Lean 則是一種證明輔助工具與函數式程式語言。
社群討論
社群驚嘆 OpenAI 僅花約 88 小時、動用 10,000 個 agent 並耗費估計 1500 萬美元算力，就解開懸宕 26 年的 Navier-Stokes 千禧年大獎難題，認為 AI 在高階數學領域正迅速突破人類極限。然而，多數留言強烈質疑 OpenAI 的學術道德，懷疑其在聽聞人類學者即將破解的謠言後，利用用戶「去識別化」的對話紀錄與提示詞來搶發成果（scoop），引發嚴重的 IP 外洩疑慮。包含 Terence Tao 在內的評論者擔憂，這種靠龐大算力截胡的行為將破壞開放科學傳統，迫使研究者未來不敢輕易分享早期想法或將機密輸入給 AI 模型。
來源
本期分類