OpenAI 於 2026 年 10 月 6 日宣布發布一系列由其內部前沿模型(internal frontier model)產生的新數學成果。為了改善與數學社群分享結果的方式,OpenAI 諮詢了高等研究院(Institute for Advanced Study)下設的獨立「數學與人工智慧諮詢小組」(Advisory Group on Mathematics and Artificial Intelligence),並依據該小組的建議與公開推薦來制定發布策略。
此次發布將結果存放在一個 GitHub 儲存庫中,並制定了論文修訂與引用的協議。OpenAI 表示正在繼續探索符合該委員會指南的其他社群託管替代方案。對於未來的發布,OpenAI 承諾將透過改進引用、數學表述及結果呈現方式,進一步提升論文品質以促進理解。
作為 GitHub 儲存庫的一部分,OpenAI 分享了許多證明的 Lean 形式化版本。Lean 是一種允許電腦檢查數學證明的程式語言。OpenAI 表示隨著獲得更多形式化證明,將持續更新儲存庫。
為了促進科學透明度與開放性,OpenAI 還在儲存庫中發布了關於如何獲得這些結果的額外細節,包括 10 份模型推理摘要、以 ChatGPT Pro 使用量計算的算力估算,以及嘗試問題數量的統計數據。根據官方說明,平均每個結果使用了相當於約三小時 ChatGPT Pro 思考的算力。
OpenAI 表示希望這些進展能推動人類知識的前沿,並促進數學領域的進一步發展。OpenAI 將資助一系列關於理解 AI 產生的重大成果的工作坊、會議和特別項目,並承諾近期將分享更多相關資訊。此外,OpenAI 正努力負責任地發布產生這些結果的模型,並持續評估其內部前沿模型在數學及其他科學領域的表現,以加速開發推動這些領域發展的工具。OpenAI 表示將繼續根據社群回饋行動,並更新未來重大科學進展披露的標準。
事件背景
Lean 是一種程式語言與定理證明器,允許數學證明透過電腦進行形式化驗證,確保邏輯的嚴謹性。高等研究院(Institute for Advanced Study)是一個獨立的學術研究中心,其下設的數學與人工智慧諮詢小組為獨立機構,旨在為 AI 在數學領域的應用與發布提供最佳實踐建議。
社群觀察
社群討論集中在對 AI 解決長期未解數學問題的反應。有用戶提到曾花費數年研究 Barnette 猜想,對其被證明感到複雜情緒。另有用戶指出唯一遊戲猜想(Unique Games Conjecture)的證明對理論計算機科學影響巨大,可能導致教科書重寫。部分討論提及 AI 在千禧年大獎難題(如 Hodge、Birch-Swinnerton-Dyer、Riemann、Navier-Stokes)上的進展,但指出 P vs NP 和 Yang-Mills 問題尚未解決。還有用戶將此進展與科幻作品中的情境進行類比,並討論 AI 發現新知識的速度加快現象。



