如果一家公司說自己的模型解了數學難題，第一個麻煩通常是驗證。8月1日，OpenAI沒有用聊天產品介紹Astra，而是拿出數學與理論計算機科學的10個結果、249頁論文、GitHub上的Lean形式化證書，以及每個解法的推理記錄。
這些結果橫跨高維幾何、編碼理論、群論、算術電路複雜性、量子複雜性、格密碼和極值組合。OpenAI稱，相關主結果至少10年沒有進展，多數更久；找到10個解所需token按Sol API價格估算約2000美元。
先把證據擺出來
官方列表包括高維球堆積新上界、二進制碼與球面碼界限改進、非sofic群構造、Connes剛性猜想反例、permanent的算術公式下界、一般雙人量子博弈的指數並行重複定理、最近向量問題的近似困難性、Ehrhart體積猜想、多色三角Ramsey數下界，以及Erdős兩個極值圖論問題。
技術口徑也可核查：permanent的公式下界是n^4/log n量級；歐氏最近向量問題給出n^1/400因子困難性；多色三角Ramsey數寫成R_k(3)=k^Theta(k)。GitHub倉庫使用Lean 4.32.0、mathlib和Lake，並提供NonSoficGroup.lean、ConnesRigidity.lean等文件。
“claiming human authorship for a proof generated entirely by an AI system would misrepresent both the system’s contribution and the nature of genuine human intellectual work.”
2000美元帶來新的審稿壓力
這個成本不包含選題、提示設計、人工整理、形式化工程與外部複核。它不能被理解成「2000美元買十個定理」。但它仍然重要，因為OpenAI把一部分探索過程價格化了：模型可以低成本產出候選證明，數學共同體需要承接更多檢查工作。
對中文研究者和模型團隊來說，這裡的提醒很直接。單說模型數學強會越來越不夠，證明文件、代碼、可復現路徑和形式化檢查會成為科研型模型發布的新門檻。Lean也可能從小眾工具變成AI數學與安全證明的基礎設施。
後續看外部驗證
Astra仍是內部模型，外界無法重放OpenAI的搜索過程。接下來要看第三方能否順利構建Lean倉庫，相關領域專家是否接受結果與歸屬，以及十個證明是否因邊界條件或文獻關係被修訂。若三關走穩，Astra就不只是模型預告，而會成為AI參與可驗證研究的先例。
參考來源：OpenAI官方研究發布、OpenAI 249頁證明論文、GitHub ten-proofs倉庫、CocoLoop、IT之家與Developers Digest；核驗Astra內部模型口徑、10個結果列表、Sol API約2000美元token成本、Lean 4.32.0構建方式、n^4/log n與n^1/400等技術指標。