2026 年 8 月 1 日，OpenAI 發布〈Ten advances in mathematics and theoretical computer science〉，宣稱尚未公開、被其稱為「下一個主要模型」的 Astra 內部版本產生十項數學與理論資工新論證。這批 OpenAI Astra 數學成果同時附上 249 頁手稿、推理過程的重建敘事，以及可交給 Lean 核心檢查的形式化檔案。
這正是大家興奮的原因：焦點不再只是模型答對多少題，而是模型能否提出原創、可被反駁、可被逐行檢查的研究候選成果。但「有 Lean certificate」不等於「十項突破都已獲學界確認」；形式命題、自然語言論文、問題原意、新穎性與重要性，仍是不同層次的判斷。
以下先忠實拆解 OpenAI 公布了什麼，再核對手稿與 Lean artifacts 的邊界，最後給出 AlphaLab 的獨立判讀：Astra 跨過了哪一道門檻，又有哪些關鍵證據尚待補齊。
OpenAI Astra 數學成果究竟公布了什麼？
官方描述的流程有三段：內部版 Astra 先產生數學論證；人類再與同一模型整理成手稿；之後由模型把每項論證形式化為 Lean certificate。OpenAI 也明確承認團隊參與手稿與形式化工作，並承擔正確性責任，因此這不是「完全無人介入、模型從選題到出版一手包辦」的故事。
“The results were achieved by an internal version of Astra, our next major model.”
中文：這些成果由 Astra 的內部版本完成；OpenAI 稱 Astra 是其下一個主要模型。
OpenAI，2026 年 8 月 1 日
手稿摘要列出十個主題；下表再用各章與 Lean repo 補足精確範圍。這裡刻意把「官方主張」和「不能延伸成什麼」放在同一張表，避免只看新聞標題就把適用範圍放大。
| 題目 | OpenAI 手稿／repo 的具體主張 | 判讀邊界 |
|---|---|---|
| 1. 高維球體堆積 | 算出完整 Cohn–Elkies 線性規劃在高維的精確漸近率，得到自 1978 年以來第一個一般球體堆積指數改進。 | 是高維漸近上界，不是每個有限維度的精確最密堆積。 |
| 2. 二元碼與球面碼 | 對每個固定相對距離 0<δ<1/2 的二元碼，以及每個固定最大內積 0<s<1 的球面碼，給出相對經典漸近界的指數級改進；另改善漸近 kissing-number 指數。 | 談的是漸近率，不是有限長度碼表的新紀錄。 |
| 3. 非 sofic 群 | 手稿構造明確的非 sofic 群，反駁「所有可數群皆 sofic」；Lean repo 另形式化推出存在有限表示的非 sofic 群。 | Comparator D 的設定只檢查「存在有限表示的非 sofic 群」。也不會順帶解決 non-hyperlinear 等問題。 |
| 4. Connes 剛性猜想 | 構造無限多個彼此不同構、有限生成的 ICC property-(T) 群，卻具有同構的群 von Neumann 代數。 | 推翻的是特定群與算子代數之間的剛性主張，不是泛稱「Connes 所有猜想」。 |
| 5. Permanent 算術複雜度 | 在複數域的精確符號運算模型中，無除法算術電路下界達 Ω(n² log log n)；公式下界達 Ω(n⁴/log n)。 | 仍是多項式下界，遠非證明 VP ≠ VNP；headline 的電路定理未被單獨放進 Comparator challenge。 |
| 6. 量子平行重複 | 對每個有限、雙方、單輪 entangled game 證明一般性的指數衰減。 | 其中 ε^13 的指數 13 未宣稱最佳；c_qs 只被陳述為某個普遍正常數。 |
| 7. Closest Vector Problem | 直接從 3SAT 歸約，證明歐氏 CVP 的 n^(1/400) 近似是 NP-hard。 | 是一般 CVP 的最壞情況困難度，不會直接改寫實際後量子系統的結構化或平均情況安全性。 |
| 8. Ehrhart 體積猜想 | 對所有維度中「重心為唯一內部格點」的 full-dimensional compact convex body，證明尖銳體積上界 (n+1)^n/n!。 | 證明體積界與一個取等例，但沒有完成所有取等情況的分類。 |
| 9. 多色三角形 Ramsey 數 | 證明 R_k(3)=k^{Θ(k)}，解決其是否超指數成長的問題。 | 確定成長階，不是求出精確漸近常數或個別 Ramsey 數。 |
| 10. 極值圖論 | 反駁修正版 compactness 猜想與二退化圖的 degeneracy 猜想。 | compactness 結果針對排除森林後的 cyclic 版本；原始字面版本早有平凡反例。 |
為什麼這次比 benchmark 更值得認真看？
一般 benchmark 給我們的是分數；這次公開套件給我們的是可被攻擊的研究物件。讀者可以查看每個定理的自然語言陳述、完整證明與 Lean 原始碼，並在建置後讓核心核對展開出的 proof term，也能追問形式命題在轉譯時是否變成較弱版本。即使最後有人找到錯誤，錯誤也比一句「模型達到超人類表現」更容易被定位。
關注度也反映這個差異。截至 2026 年 8 月 3 日的快照，相關 Hacker News 討論約 455 points／322 則留言，r/math 討論約 840 upvotes，公開 Lean 儲存庫約 350 stars；平台數字仍會浮動。這些數字顯示發布迅速吸引大量跨社群關注，但不能證明參與者身分，更不能替任何定理背書。
這是 OpenAI Astra 數學成果最實質的地方：它把「相信模型或相信公司」改造成「檢查定義、定理與證明」。只是可檢查性提高，與檢查已完成，仍相差一整段距離。
Lean 證書證明了什麼，也沒替你證明什麼
Lean 的價值非常具體：它把證明壓成一個小型可信核心能核對的 proof term。若定義、定理陳述與匯入公理固定，Lean 核心會逐步檢查結論是否真的能由這些前提出發。這能抓出人類審稿容易略過的代數跳步、符號混淆或隱藏前提。
AlphaLab 以 2026 年 8 月 3 日的 94bc0fe commit做文字掃描：十個主要 solution .lean 檔合計約 54.8 萬行，沒有找到 sorry、admit 或新增的顯式 axiom；工具鏈固定在 Lean 4.32.0、特定 Mathlib 與 Comparator commit。發布方的 formalization.yaml列出 12 個 main-results entries，每個對應一個 declaration，自報 sorry_count: 0，並把允許公理列為 propext、Classical.choice 與 Quot.sound；審查狀態則是 agent-reviewed。這些是原始碼文字掃描、metadata 與檢查設定，不是公開的成功執行紀錄。截至同日，這個單一 commit 的公開 tree 未附 CI／Comparator log，Actions 頁也未顯示 workflow run；這不表示 OpenAI 私下沒有執行。Comparator challenge files 另有 42 個刻意留下的 sorry placeholders，屬於待比對的 theorem／definition targets，不在正式 solution files，因此不能把整個 repo 簡化成「零 sorry」。
這裡有三道不能混在一起的門：
- 形式推導：在給定定義與前提下，proof term 是否推出形式命題？這是 Lean 最擅長的部分。
- 語意對應：Lean 裡的定義與 theorem，是否忠實表達數學界原本問的問題？這需要懂領域的人逐項比對。
- 研究判斷：結果是否新穎、文獻是否漏引、重要性多大、歸因是否準確？形式驗證不會自動回答。
Lean 官方文件本身就提醒，信任一個形式化定理仍涉及「形式陳述與非形式意義是否相符」。OpenAI repo 另提供 Comparator challenge 設定；只有在 trusted challenge 與 imports、sandbox 及檢查命令都於可信、乾淨的環境中正確執行，Comparator 才能確認設定中的 theorem names 具有相同形式陳述、只使用獲准公理並由核心接受。設定檔本身不是通過紀錄，也不能替人判斷「這是不是原來那個重要問題」。CVP 的 challenge 還包含四個 definition holes，Comparator 文件也要求這類設定再經額外、可能是人工的 verifier 檢查。
2,000 美元不是整場實驗的總帳
官方原文的精確說法是：找出這十個成功解法所用的總 token 數，若按 Sol API 費率換算，約值 2,000 美元。OpenAI 研究員 Noam Brown 也澄清這是十項合計，不是每一項各花 2,000 美元。
但這個數字不是端到端研發成本。Brown 另確認模型還嘗試過其他重大問題但未成功，並補充目前沒有 Millennium Prize problem 的成果。官方頁面與 Brown 這兩則公開說明只把 2,000 美元定義為十個成功解法的 token API 等值，沒有提供端到端成本或失敗嘗試的完整分母；因此不能把它改寫成「只用 2,000 美元完成十項研究突破」。
同樣地，OpenAI 公開的推理筆記不是原始 chain-of-thought。摘要說一個 AI 模型讀取原始 traces 與成品後，“reconstructs how the proof came together”。它確實整理出失敗方向、轉折與關鍵想法，但仍是事後重建敘事，不能拿來估計完整搜尋樹或重現整場實驗。
外部專家已經確認了嗎？
官方手稿只在非 sofic 群與 Connes 剛性兩章列出具名致謝對象，其中包括 Sorin Popa、François Charles、Cyril Houdayer 等人。原文只說他們提供 comments、careful readings 或 helpful suggestions，沒有稱他們為審稿人，也沒有說他們確認定理正確。這是有價值的前期閱讀訊號，但不是十項成果已完成同儕審查的證據。OpenAI 也直接邀請數學社群繼續檢查與放回既有文獻脈絡。
一則具體的公開專業反應來自量子複雜度研究者 Henry Yuen。他表示一般量子平行重複定理若成立，意義重大；由於據稱有 Lean 形式化，他暫時預設結果正確，但也明說自己尚未消化或核查證明。其批評針對 reasoning walkthrough：文件沒有解釋為何 resolvent purification 會是自然的研究方向。至少就 Yuen 當時的公開說法，形式化提高了他的暫時信任，但他本人尚未完成理解與確認。
Leiden Declaration on AI and Mathematics提供了更一般的制度框架：宣言指出形式化仍有機器表述與人類概念之間的 translation gap，並主張研究仍應進入同儕審查管道；新聞稿與部落格不能取代同儕審查或社群檢驗。這份宣言早於 Astra，不是對十項論證的反駁；它提醒我們應該用什麼程序把「公司公布」變成「共同知識」。
AlphaLab 如何判讀 OpenAI Astra 數學成果？
我同意 OpenAI 的地方
Astra 的發布方式確實比 benchmark 或只給答案的 demo 前進一大步。十項題目不是競賽短題，而是跨越幾何、群論、算子代數、複雜度、密碼相關格問題與極值組合的研究題；每項都有長篇論證與形式化物件，外部研究者可以直接找錯。若其中多數通過領域審查，frontier model 就不只是協助搜尋文獻或補齊證明，而是能生成原創研究候選成果。
真正的新門檻因此不是「AI 宣稱解出開放問題」，而是「AI 一次交付多個可定位錯誤的研究包」。如果多數成果通過審查，而且成本說法能被重現，研究瓶頸可能往後移：生成假說與候選證明變便宜，精確形式化、語意核對、文獻查重與人類理解反而更稀缺。
我仍保留的地方
第一，OpenAI 公布了十個成功成果，但沒有公布所有嘗試問題的完整清單、搜尋分布與總成本；我們因此無法判斷 Astra 是穩定產生研究成果，還是在大量搜尋後挑出十個例外。第二，形式化物件主要仍由同一發布方與模型建立；最有說服力的下一步不是更多宣傳，而是不同團隊一方面在乾淨環境重跑 Lean／Comparator，另一方面從原問題獨立核對或重建 formal statement，並公開 logs。
第三，「正確」本身有四層：proof term 在形式系統內成立、形式命題對應原問題、結果在文獻中確實新穎，以及學界理解它為何重要。Lean 強化第一層，也把第二層需要審查的定義攤開；它本身不驗證形式命題是否忠實對應原問題。後兩層仍是研究共同體的工作。把四層壓成一個「verified」標章，反而會掩蓋這次發布真正重要的地方。
因此，對 OpenAI Astra 數學成果最合理的暫時結論是：依 OpenAI 目前公開的產製說法，Astra 內部版本已跨進「產生研究級、可機器檢查候選成果」的階段；它是否已產生十項公認的新數學成果，仍要等各領域專家完成語意核對、文獻查重與同儕審查。
接下來最值得看三個訊號
- 獨立重跑與語意稽核：外部團隊能否在乾淨環境重跑 Lean／Comparator，並另外逐項確認定義真的對應原問題。
- 領域專家的具體回應：不是一句「很厲害」或「AI 不可能」，而是指出哪個 lemma、定義、歷史歸因或新穎性判斷成立或有誤。
- 分母與修正紀錄：OpenAI 是否補充嘗試問題數、完整評測流程與失敗分布；repo 接下來的 commits 又修正了形式問題、論文表述，還是只改善可讀性。
研究者現在可以把這次發布當成一套新工作流的壓力測試：模型生成候選論證，人類核對問題語意，乾淨環境中的 Lean／Comparator 重跑檢查形式推導與 statement 一致性，再由領域社群判斷新穎性與重要性。一般讀者則只要記住一條線：公開 artifacts 值得提高關注，但不能把「可驗證」提前寫成「已驗證」。