OpenAI 用 Astra 解出十道數學難題：Lean 可驗證，$2,000 成本仍不是產品價格

OpenAI 這次成果能否成立，有一條可以推翻的檢驗線：獨立數學家必須確認十道題的原始命題、假設與新穎性，並在相同 Lean 4.32.0 環境重建證明。若形式化檔案可以編譯，卻有題目曾被解出、命題被縮窄或關鍵假設與學界問題不同，Astra 的「解出十道開放問題」主張就需要下修。

OpenAI 在 August 1, 2026 公布〈Ten advances in mathematics and theoretical computer science〉。公司表示，內部版本的 Astra 解出十道數學與理論資工問題；這些問題至少十年沒有進展，多數停滯更久。題目橫跨高維球體堆積、編碼理論、群論、量子複雜度、格密碼學與極值組合學。The Decoder 查核公司報告後指出，Astra 是 OpenAI 下一個主要模型家族，尚無公開發布日期，也不確定最後會採 GPT-6 或 GPT-5 系列名稱。

十項結果並非平均分數。Astra 建構非 sofic 群，處理「是否每個群都能用有限置換近似」的問題；它也提出計算 permanent 的算術公式下界 $n^4 / \log n$，並解決 Erdős problems 183、146 與 180。這些命題分屬不同領域，十題全數完成不能代表任意研究問題的成功率。OpenAI 沒有公布候選題總數、完整失敗清單或挑題流程。

Lean 檔案把查核移到命題與假設

OpenAI 把十份結果形式化為 Lean 證明，並公開論文與推理過程。Lean 可檢查每一步是否由既定公理與定義推出，降低代數漏步或引用錯誤藏在長篇論證中的風險。形式驗證只回答「形式命題能否由這組假設推出」；題目是否對應原始問題、結果是否已有先例，仍需該領域研究者審閱。

公司表示，人類研究員協助整理論文與形式化證明，數學論證由 Astra 產生，OpenAI 對準確性負責。The Decoder 引述數學家 Thomas Bloom，稱非 sofic 群等結果是重大消息；OpenAI 研究員 Noam Brown 也說，團隊嘗試其他重要問題但失敗，沒有解出 Millennium Prize Problems，而且每題投入的測試時計算量不高。這是一組經篩選的研究結果，不是公開模型的盲測基準。

$2,000 衡量推論 Token，不含研究成本

OpenAI 估算，產生十份解答所用 Token 若按 Sol API 費率計算，約為 $2,000。這個數字沒有納入選題、人員審稿、Lean 形式化、重跑失敗嘗試、模型訓練或基礎設施折舊，也不是 Astra 未來的售價。它能回答已知成功案例的推論 Token 等值，不能回答每取得一項可發表成果的總成本。

未來三到六個月可檢查兩組資料：外部研究者能否重建十份 Lean 證明並確認命題的新穎性，以及 OpenAI 是否公布嘗試總數、失敗分布與單題計算量。前者決定這十項結果能否進入學術紀錄，後者才讓外界估算 Astra 從挑選後的成功案例走向一般研究工作的產出率。

來源：

• OpenAI：Ten advances in mathematics and theoretical computer science
• The Decoder：OpenAI announces its next major model Astra by dropping ten previously unsolved math solutions

延伸閱讀：

• OpenAI：Ten Advances Lean formalizations