最重要的數字是 460,000：OpenAI 於 8 月 1 日向一個公開 GitHub 倉庫上傳的可機器檢驗證明的行數，用以支撐其在數學和理論計算機科學領域自稱的十項進展。宣布這些進展的部落格文章日期同為當天早上，稱成果來自 Astra 的一個內部版本，即'我們的下一代主力模型'。十項成果各附一份 Lean 證書，即可機器檢驗的形式化證明，放在 github.com/openai/ten-proofs 倉庫，採用 Apache-2.0 授權。我們檢查了檔案：十份全部能用 Lean 4.32 和 mathlib 編譯，且沒有一份含有'sorry'占位符或自定義公理這兩個常見的逃生艙。
這十項，按 OpenAI 的表述：高維球體堆積的新上界，降至 Cohn-Elkies 閾值；二進位碼和球面碼的指數級改進界；非 sofic 群的構造；證偽 Connes 剛性猜想的反例；永久式的下界，包括一個 n 的四次方除以 log n 階的算術公式下界；量子賽局的指數級平行重複定理；最近向量問題多項式因子近似難度；Ehrhart 體積猜想的精確答案；多色三角形 Ramsey 數的超指數下界，這將解決 Erdos 第 183 題；以及緊緻性和退化性猜想的反例，解決 Erdos 第 146 和 180 題。OpenAI 的框架是每個問題都至少停滯了十年。這個框架是他們的，按 Sol API 費率約 2,000 美元總算力的數字也是他們的。
以下是今天可以獨立核驗的部分，比沒有多，比證明少。可核驗：倉庫存在，十份 Lean 檔案在內，內容如上所述，兩份配套 PDF（論文和模型的推理敘述）可以下載，倉庫還附帶獨立內核檢驗的設定。尚不可核驗：OpenAI 之外沒有人報告重建了這些證明；沒有人類數學家評審過；也沒有專家確認形式化命題與非形式定理同義，而這一步正是形式化可能悄悄出錯的地方。最強的未被批准信號：參考追蹤站 erdosproblems.com 仍把第 183 題列為開放，懸賞 250 美元，而一個較小的追蹤站已在 8 月 1 日將其標為已解。該站維護者 Thomas Bloom 稱這是'大新聞'，'就構造而言，這是大的'，這些話由 The Decoder 轉引；我們未能直接取到原文。
在命名上必須精確，因為這篇將是人們回引的出處。部落格寫的是'Astra 的一個內部版本，我們的下一代主力模型'。'下一代主力模型家族'的說法來自 OpenAI 研究員 Noam Brown，他還補充說'遺憾的是沒有千禧年難題（暫時）'，並指出該模型在其他重大問題上失敗了。其餘一切都是報導而非確認：The Information 經 The Decoder 轉述，稱 Astra 是與 Sol、Terra、Luna 並列的新模型類，GPT-6 還是 GPT-5.7 尚未決定，也沒有發布日期。OpenAI 自己的倫理說明值得整段引用：'為一個完全由 AI 系統生成的證明聲稱人類作者身分，會同時歪曲系統的貢獻和真正人類智力工作的性質'，公司表示他們為正確性負責，而論證本身由模型生成。等重建結果到來時，就該用這句話來要求他們。