OpenAI 一次公布 10 項數學成果：未發表的 Astra 模型解出長年難題，全部 token 成本約 2,000 美元

一句話看懂：OpenAI 在 8 月 1 日公布 10 項數學與理論電腦科學成果，由尚未發表的 Astra 內部版本產生，每項都用 Lean 做了形式化檢查，官方說全部的 token 成本約 2,000 美元。

先用白話講：「開放問題」和 Lean 是什麼？

數學裡有很多「開放問題」：題目大家都看得懂，但幾十年來沒人能證明它是對是錯。解開其中一題，通常就是一篇重量級論文。

那 Lean 是什麼？可以把它想成「數學證明的文法檢查器」。人把證明改寫成 Lean 看得懂的格式之後，程式會一行一行機械式檢查：每一步推理合不合規則。通過了，就代表這份證明在邏輯上沒有漏洞。

發生什麼事

OpenAI 在 8 月 1 日發表文章，分享 10 項結果。官方說每一項都解決了、或對一個長年開放的問題有實質進展，涵蓋高維幾何、編碼理論、算術電路複雜度、群論、算子代數、量子複雜度、格密碼學、極值組合學。

幾個比較容易說明的例子：

這些名詞對一般人很艱深，重點是：它們都是各自領域公認的「硬題」。

官方說了哪些做法？

• 誰做的：由 OpenAI 尚未發表的下一代主力模型 Astra 的內部版本找出
• 成本：找出這些解法所需的 token，以 Sol API 費率計算，約 2,000 美元
• 人做了什麼：人類與同一個模型把這些論證整理成論文
• 驗證：模型把每個論證形式化成 Lean 證明；官方也釋出每個解的「思考過程敘述」
• 背景：5 月，OpenAI 曾分享 AI 產生的、對 Erdős 單位距離猜想的反證，當時是評測未發表模型時發現的

要冷靜看的地方

這是 OpenAI 自己的公布。官方文章也沒有說這些成果已經過同行審查，反而是邀請數學界「深入檢視、放進脈絡」。Lean 檢查能確認邏輯無誤，但這些結果在數學界的重要性、是否真的回答了原本的問題，還需要專家評估。

另外，官方在署名問題上的立場很明確：數學論證是系統產生的，OpenAI 協助整理論文與形式化證明，並為其正確性負責，不應把完全由 AI 產生的證明，說成是人類的作品。

給開發者的技術細節

• 官方文章附了論文與各題的推理過程連結，想研究的人可以直接讀；我只讀了文章本身，沒有逐篇驗證
• 對工程師有啟發的是流程：讓模型自己做，再用機器能檢查的形式（這裡是 Lean）把結果驗證一遍。這跟寫程式時「AI 寫的程式要有測試擋著」是同一個道理
• Astra 目前只出現在這篇文章裡，官方沒有說明對外提供的時間與價格

我的看法

「約 2,000 美元」這個數字最讓我有感。以前談 AI 做研究，大家想到的是動輒需要大型實驗室的算力；這次官方給的是一個個人或小公司也能理解的金額。當然，這是官方說的 token 費用，不包含研發模型本身的花費，也不代表任何人都能重現。

我更在意的是「驗證」。AI 給的答案再漂亮，如果沒有一個能自動檢查的機制，你只能選擇相信或不相信。Lean 在數學裡扮演的角色，就像我們寫系統時的自動化測試：不是不信任 AI，而是讓它的結果可以被檢查。接案時如果要把 AI 產出放進客戶的系統，我會先問自己，這個結果有沒有類似的檢查機制。

名詞小辭典

• 開放問題：還沒有人證明出答案的數學問題。
• Lean：讓電腦檢查數學證明是否正確的證明輔助軟體。
• 形式化（Formalization）：把數學論證改寫成電腦能逐步檢查的嚴格格式。
• Token：AI 計算文字量的單位，API 費用依 token 數量計算。

資料來源

• OpenAI：Ten advances in mathematics and theoretical computer science（2026-08-01）