8 月初，OpenAI 在一篇標題只談數學的部落格文章裡，低調公布了下一代模型 Astra，並用一種不尋常的方式證明它的實力：沒有公布 benchmark（基準測試）分數，而是揭露其能破解 10 道長年無人能解的數學與理論電腦科學難題。
根據《Gizmodo》，Astra 的名字甚至不是這篇文章的主角，而是被塞在第三段，OpenAI 只用一句話帶過：這些成果「由內部版本的 Astra 完成，也就是我們的下一個主要模型」。這款被輕描淡寫帶過的新模型，究竟是什麼？
Astra 是什麼？OpenAI 連正式名稱都沒說清楚
OpenAI 只把 Astra 描述為「下一個主要模型」，並未說明完整定位，連正式名稱都留白。《Gizmodo》觀察，OpenAI 現行模型以拉丁文命名，Terra 意思為地球、Luna 為月亮、Sol 為太陽，而 Astra 意為「群星」，按這個命名邏輯，Astra 可能是另一個 GPT-5.6 系列版本，但也可能是 GPT-6，甚至就叫 Astra，OpenAI 並未清楚說明。這些目前都僅止於推測。
至於這款模型能做什麼，《Gizmodo》引述《The Information》報導指出，Astra 具備執行「長時間任務」的能力，OpenAI 執行長 Sam Altman 上週也在華府向聯邦官員展示了這款模型。更值得注意的是，OpenAI 選擇用這些數學成果，作為 Astra 首次公開亮相的內容。
10 項數學成果，成了 Astra 第一份公開成績單
OpenAI 這次公布的 10 項成果，橫跨高維幾何、編碼理論、群論、算子代數、量子複雜度、格密碼學與極值組合學等領域。OpenAI 表示，這些問題都已開放至少十年、多數更久，且主要結果長期毫無進展；而找出全部解答所需的運算量，換算成 Sol API 費率大約只要 2,000 美元。
其中最受矚目的一項，是建構出首個已知的「非 sofic 群」（non-sofic group）。根據《Tech Times》與《The Next Web》，這個概念由數學家 Mikhail Gromov 於 1999 年提出，是否存在非 sofic 群，是群論領域懸而未決近 27 年的核心問題，而 Astra 的建構給出了答案。此外，Astra 也推翻了 1980 年由費爾茲獎得主 Alain Connes 提出的剛性猜想，並解決了 Erdős 著名難題集裡的三道題目。
過去實驗室發表新模型，慣例是端出各項 benchmark 成績與新功能，OpenAI 這次卻直接以原創科研成果作為能力證明。它在文章中說明，這些數學論證由 Astra 生成，人類研究員負責把論證整理成手稿，並不宣稱人類是證明的作者。用 OpenAI 自己的話說，若把 AI 系統獨力完成的證明冠上人類作者之名，等於同時扭曲了系統的貢獻，以及人類智識工作的本質。
Lean 證明，讓「AI 說它解開了」變得任何人都能查
這篇文章另一關鍵設計，藏在每道題附帶的一份 Lean 證明檔。Astra 的每一項解答，都附上一份可由 Lean 4 驗證的機器可讀證明，並公開在 GitHub 上。
這個細節之所以重要，要回到 AI 數學成果長期以來最大的爭議：外界很難獨立驗證。根據《Tech Times》，OpenAI 今年 5 月推翻 Erdős 單位距離猜想時，靠的是 9 位外部數學家讀完論證後背書，這是很強的驗證，卻是一種社會信任，得仰賴夠格的專家願意花時間，也無法在沒有這些人的情況下重現。
Lean 證明改變了這個等式。《Tech Times》解釋，Lean 4 的核心是一個「可信核心」（trusted kernel），任何證明都必須通過它逐步比對數學公理，結果只有通過或不通過兩種，不需要博士學位、也不必等待漫長的同儕審查，任何人只要有一台筆電和 Lean 編譯器，就能自己跑一次驗證。這也讓 OpenAI 能把焦點放在數學成果本身，而不是只依賴 benchmark 分數。
不過驗證也有一條界線。《Tech Times》指出，Lean 通過只證明了這份證明對於在 Lean 裡形式化陳述的那個定理成立，並不自動保證形式化後的陳述，精準對應到數學界原本理解的那道難題，這一層對應仍需要人類判斷。換句話說，證明本身可以自動查核，但「有沒有問對問題」還是得靠數學社群來確認。
對照去年的誇大爭議，這次連原本的批評者都改口
OpenAI 會如此在意驗證，與它去年留下的紀錄有關。根據《Tech Times》，2025 年 10 月，時任 OpenAI 副總裁的 Kevin Weil 曾在 X 上宣布 GPT-5 解開了 10 道未解的 Erdős 難題。但維護 erdosproblems.com 難題集、後來受託查證的曼徹斯特大學數學家 Thomas Bloom 發現，該模型其實沒有產出任何原創證明，只是從文獻裡找出既有解答，Bloom 稱這是「嚴重的不實陳述」。Google DeepMind 執行長 Demis Hassabis 形容此事「令人難堪」。
同一位 Bloom，這次改了口。《Tech Times》與《The Next Web》都提到，Bloom 在 X 上稱 Astra 的 10 項成果是「大新聞」，評價高於 5 月的單位距離反例。
根據《The Next Web》，數學家今年 6 月發表《萊頓宣言》（Leiden Declaration），並獲國際數學聯盟背書，警告 AI 公司未經同意使用已發表的研究、繞過同儕審查，並點名那些用新聞稿而非期刊發布成果的公司。OpenAI 這次主動在公告中引用這份宣言，並言明數學想法來自 Astra、而非整理手稿的人類研究員，正是宣言所要求的揭露方式。
不過，這次的成果也有它的邊界。根據《Tech Times》，OpenAI 研究員 Noam Brown 在 X 上坦言，Astra 沒能攻下任何一道克雷數學研究所的「千禧年大獎難題」（每題懸賞百萬美元），但他也補了一句，這次在每道題上花的算力其實不多，還有很大的推進空間。
從 5 月推翻 Erdős 單位距離猜想，到這次一次公開 10 項成果，並附上可由 Lean 驗證的形式化證明，OpenAI 對外展示前沿模型能力的方式，開始不再只圍繞 benchmark 或產品功能，而是把原創科研成果放到舞台中央。這也讓另一個問題浮上檯面：一份能被機器驗證、卻尚未完成傳統同儕審查的研究成果，數學社群將如何評價它的地位？目前答案仍有待時間驗證。
【推薦閱讀】
◆ OpenAI 才出事，Anthropic 也承認：Claude 測試曾誤駭 3 家公司
＊本文開放合作夥伴轉載，資料來源：OpenAI、《Gizmodo》、《Tech Times》、《The Next Web》、《The Information》，首圖來源：Unsplash
