OpenAI 公布 Astra 產生的十項數學成果，Lean 4 憑證開放獨立重建

OpenAI 公布由內部版 Astra 產生的十項數學與理論計算機科學結果，範圍橫跨高維球體堆積、編碼理論、群論、算術電路複雜度、量子平行重複、格密碼學與極值組合學。公司稱模型先找出論證，人類再與同一模型整理成總計 249 頁的手稿，最後由模型將各項論證形式化為 Lean 4 憑證。

較具體的主張包括：把一般高維球體堆積的漸近上界推進至 Cohn–Elkies 線性規劃門檻；構造非 sofic 群；提出反例否定 Connes 剛性猜想；證明 permanent 的算術公式下界達到 Ω(n⁴/log n)；以及對歐幾里得最近向量問題給出 n^(1/400) 因子的近似困難度。OpenAI 也聲稱解出兩項 Erdős 極值圖論問題，並取得多色三角 Ramsey 數的超指數下界。

與只發布自然語言解答不同，`openai/ten-proofs` 儲存庫提供十個對應的 `.lean` 模組，固定使用 Lean 4.32.0、mathlib 與 Lake。研究者可先取得 mathlib cache，再執行 `lake build All` 重建全部形式化；另有 Comparator 挑戰，用於降低錯誤公理、未宣告假設或不受信任捷徑混入證明鏈的風險。OpenAI 估算搜尋這些解法所耗 token，若依 Sol API 費率折算約為 2,000 美元，但未公開 Astra 權重、完整搜尋軌跡、失敗樣本或實際運算量。

Lean 核心接受憑證，只代表形式化陳述能由指定依賴推導，不會自動證明形式化命題與原始公開問題完全等價，也無法取代對新穎性與文獻先例的檢查。下一步應觀察各領域研究者能否獨立重建、核對定義與找出更早結果；在此之前，十項成果宜視為附機器可驗證工件的重大研究主張，而非已完成同行評審的定論。