OpenAI Astra 推進十項數學難題，AI 開始試做長時間原創研究
論文同 Lean 證明已公開，同行核實仍然啱啱起步
Astra 做緊咩
OpenAI 8 月 1 日公開一批由內部模型 Astra 產生嘅研究成果，範圍由高維球體堆疊、編碼理論、群論，去到量子複雜度同格密碼學都有。官方稱 Astra 係下一個主要模型系列嘅內部版本，暫時冇公開 API、推出時間、收費或者使用限制。Astra 呢個名現階段代表研究系統，冇足夠證據叫佢 GPT-6。 TechNews 科技新報報道亦提到，OpenAI 仲未定最終產品名，所以見到網上自行加代數字，先當估計會穩陣啲。
十項成果唔可以全部叫「解決十題」
今次個清單入面，有啲成果完整處理咗多年懸案，例如構造出 non-sofic group、提出 Connes rigidity conjecture 嘅反例；有啲就係改善已知界限，例如二元碼、球面碼同 arithmetic circuit complexity；高維球體堆疊嗰篇亦聲稱刷新咗 1978 年以來嘅一般漸近上界。換句話講，十項都可能有研究價值，但成果形式同份量並唔一樣。用「攻克十道數學題」概括得太爽，會令人以為每項都似交功課咁有單一標準答案。
同一般聊天模型差喺可以一路試落去
平時聊天模型收到問題，通常喺一次對話內砌出一個睇落合理嘅答案；Astra 呢類研究系統就似一個可以跑較耐嘅 agent，會試唔同方向、發現條路行唔通，再改用另一套工具或者觀點。OpenAI 另外公開咗 62 頁「discovery notes」，入面包括失敗方向同轉折位。不過呢份文件係另一個模型讀過原始思考紀錄同完成稿之後整理，唔等於完整原始運算紀錄，外界仍然未能重演成個探索過程。
OpenAI 話，成功搵到呢批解法所用嘅 token，按 Sol API 費率折算大約值 2,000 美元。呢個數字幾搶眼，但只反映官方計算嘅成功解題 token，唔包括訓練 Astra、揀題、失敗實驗、人手整理論文同驗證環境嘅成本。現階段用佢判斷研究自動化有幾平，仲早咗少少；佢較有用嘅訊息係，當模型可以長時間搜尋，一次成功研究 run 未必一定要燒到天文數字。
有 Lean 證明，未等於十篇論文全部過關
OpenAI 放出一份 249 頁論文集，亦喺 GitHub 公開十套 Lean 4 formalization，外界可以下載後自行 build。Lean 會逐步檢查形式邏輯有冇斷位，可信度高過只靠模型用自然語言話「證明完成」。不過 Lean 證書、專家審閱同正式同行評審係三層嘢：形式系統可以證明程式內寫低嗰個命題，但仍要有人確認命題有冇準確對應原本難題、前提有冇收窄、引用同新穎性又有冇問題。
公開論文顯示，non-sofic group 同 Connes rigidity 章節曾獲相關數學家提供意見或仔細閱讀；Connes 嗰項亦提到有另一項同期獨立研究得出反例。呢啲都係正面訊號，但「提供意見」唔等同替整篇論文背書，而官方亦冇交代十項成果全部完成獨立專家核實或者期刊評審。篇章公開至今時間好短，較準確嘅講法係：證明材料已經開放畀學界檢查，驗證程序先啱啱開始。
Coding agent 都可以抄呢套做法
Astra 最值得 developer 留意嘅地方，其實係「長時間搜尋加硬驗證器」呢個組合。數學有 Lean，寫 code 就有 compiler、type checker、測試、static analysis 同可重現嘅執行環境。Agent 可以同時試幾條修正路線，但每次改動都要俾工具驗收，失敗就退返去再試。呢種閉環有機會令 coding agent 處理跨檔案重構、追長尾 bug 同大型 migration 時穩定好多，前提係測試本身真係覆蓋到產品要求。
科研都一樣：模型愈識得大量產生候選證明，人類時間就會由搵思路，逐步轉去揀問題、定義可驗證命題、查舊文獻同覆核結果。下一步要睇嘅係其他團隊可唔可以重建十套 Lean 證明、各領域專家點評原稿，仲有 Astra 日後面對冇現成形式驗證器嘅任務時，表現會唔會一樣可靠。
參考來源
- TechNews 科技新報 — OpenAI 揭露新一代模型 Astra，宣稱攻克 10 道數學難題 — original report
- OpenAI：Ten advances in mathematics and theoretical computer science — 官方公布十項成果、Astra 身份、token 成本估算同形式驗證安排。
- OpenAI：Ten Advances in Mathematics and Theoretical Computer Science — 249 頁完整論文集，可核對各項定理、研究背景、致謝同聲稱範圍。
- OpenAI：How the Ideas Came Together — 官方整理嘅研究思路、失敗方向同關鍵轉折，亦交代文件並非原始思考紀錄。
- OpenAI ten-proofs GitHub repository — 十套 Lean 4 formalization、重建指令同獨立 proof checking 資料。
- OpenAI Academy：Terence Tao on AI in mathematics — 補充 AI 輔助研究、自然語言證明風險同 Lean 正式驗證嘅背景。
本文根據原文及公開資料整理；資料有出入時，以原文及官方資料為準。
