OpenAI 在 2026 年 8 月 1 日發布一份報告，宣稱一個尚未公開的內部模型解出了十道停滯至少十年的數學與理論計算機科學開放問題，並且——這才是重點——把十份 Lean 4 形式化證明檔一起放上了 GitHub。同一天，OpenAI 首度正式確認「Astra」是它下一代模型家族的名字。
先把判斷放最前面：這件事真正的分水嶺，不是「AI 解開了難題」，而是這次的宣稱附了機器可驗證的產物。 過去要判斷這類新聞，你要嘛選擇相信公司，要嘛等少數看得懂的人讀完；這次儲存庫可以點開，證明檔可以在自己的電腦上跑一次。但話要講清楚——「解出」目前仍然只是宣稱，尚未經過同儕審查。十題裡任何一題後來被撤回，都會很大聲。
硬證據到哪裡為止：儲存庫是真的，「解出」是宣稱
不需要相信任何人、可以直接查證的，是這一批：openai/ten-proofs 儲存庫確實存在，採 Apache-2.0 授權，說明文件要求 Lean 4.32.0 與 mathlib，給的建置指令是 lake build All。裡面十份 .lean 檔對應十個結果，加總超過 2,100 萬位元組，最大的一份是對應最近向量問題的 GapCVP.lean，單檔就有 533 萬位元組。儲存庫本身建立於 2026 年 8 月 1 日。
這些不是宣傳素材，是可以被機器逐行檢查的東西。
需要標成「宣稱」的，則是另外一批。據 the-decoder 報導，OpenAI 說這十題「至少十年沒有進展」，數學論證本身出自 Astra，人類研究員之後才把輸出整理成論文。據 The Next Web 的整理，十題包含首個明確的非 sofic 群構造（這個概念由 Gromov 在 1999 年提出）、推翻 Connes 剛性猜想、證明 Ehrhart 體積猜想，以及 1978 年以來首次改進高維球堆積密度上界的指數。據 Implicator.ai，隨附的手稿有 249 頁。
至於那個被到處轉載的數字——十題所耗的 token「按 Sol 的 API 費率換算約 2,000 美元」——多家媒體說法一致，但請注意它的性質：那是掛牌價換算，不是這項研究的真實成本。
Astra 本身尚未發布，外界拿不到、也無法自己測試。據 the-decoder 報導，它預計會是首批走美國聯邦審查流程的模型——這條線我們在白宮把前沿模型使用權收回政府端那篇談過。
（一併交代：OpenAI 的報告頁在我們查證當下回 403，同網域其他頁面也一樣，屬於擋爬蟲而非頁面失效；因此本文所有細節都改以一手儲存庫與可讀的二手報導交叉佐證。）
為什麼「附上 Lean 檔」跟以往的宣稱不一樣
Lean 是一種證明語言：每一個邏輯步驟都要寫到程式能自己檢查，能編譯過，就代表這串推理在該形式系統裡沒有跳步。
差別在成本結構。以前要判斷一則「AI 解開難題」的新聞可不可信，你需要的是一位真的懂這個領域的人，花上數週到數月——而全世界熟悉 Connes 剛性猜想的人，可能不超過三位數。現在你需要的是裝好 Lean、抓 mathlib 快取、跑一次建置。驗證從「稀缺專家的時間」變成「一台電腦的時間」。
我們在 Claude 找出 Jacobian 猜想反例那篇下過一個判斷：AI 最適合被放在「答案容易驗證、搜尋空間巨大」的問題上。那次的反例短到能塞進一則貼文，人人可以手算；這次的證明大到沒有人會用眼睛讀完，卻反而更好驗，因為驗的人換成了編譯器。同一個原理往上放大一個量級：可驗證性不是加分項，它決定了一個宣稱值不值得你花時間。
形式化保證的，跟它不保證的
這是外行最容易誤讀的地方，也是本文最想講清楚的一段。
Lean 建置成功，保證的是：在給定的那個形式化陳述之下，推理沒有邏輯漏洞。
它不保證的是：那個被形式化的陳述，就是數學界原本在問的那個問題。 把一個猜想從自然語言翻成形式語言，中間有大量選擇——定義怎麼下、量詞放在哪裡、邊界條件收不收。翻歪一個地方，你會得到一份完美編譯、卻證明了別的東西的檔案。這一步沒有機器可以代勞。Implicator.ai 也點出同一件事：Lean 通過的論證不等於通過同儕審查，社群還是得同意「被形式化的那個陳述，就是他們在意的那個陳述」。它同樣不保證新穎性與重要性——這題以前是不是真的沒人解過、解出來對這個領域意味著什麼，都要人回去對文獻。
而且這件事發生在一個相當緊繃的背景上。2026 年 6 月 2 日，一群數學家發表了萊頓宣言並獲國際數學聯盟背書，明確要求：使用自動化工具時，論證與結果的正確性責任仍完全屬於人類作者，而且數學結果應該發表在同儕審查的場域。宣言也直接批評企業以新聞稿的形式，搶在社群評估之前發布成果，並指出外界拿不到方法、提示詞、訓練資料與算力消耗等評估所需的資訊——被拿來當背景對照的案例之一，正是 OpenAI 在 2026 年 5 月宣稱推翻 Erdős 單位距離猜想那一次。這次至少多了 Lean 檔，但發布路徑仍然一樣：先發稿，再讓學界追。
台灣角度：格密碼那一題，兩個方向都容易讀錯
十題裡有一題直接碰到台灣正在做的事：最近向量問題（closest vector problem）的近似困難度。它是格密碼的地基，而格密碼正是後量子密碼的主流路線。
這裡要先把方向講對，因為兩邊都很容易讀反。 這個結果的方向是「證明它更難」，不是「把它破解掉」。它強化的是這類問題的困難度證據，不是一次攻擊。所以——
- 不建議把這則新聞讀成「AI 快要破解加密了」。方向完全相反。
- 也不建議讀成「地基更穩，遷移可以緩一緩」。最壞情況的困難度結果，跟實際密碼系統依賴的平均情況安全性，本來就不是同一件事。
台灣的時程不會因為這則新聞改變。數位發展部數位產業署已於 2025 年 4 月 16 日偕同後量子資安產業聯盟發布《後量子密碼遷移指引》，該署同時指出美國 NIST 與英國 NCSC 都預計在 2035 年全面停用傳統加密演算法。該做的準備，一天都不會少。
另一個只能當觀察、不能當定論的訊號：如果「按掛牌價換算約 2,000 美元」這個量級大致成立，那麼「要投入多少資源才可能推進一道長期難題」的分母正在改變。這不代表台灣學界該去追同一種打法——這類產出高度依賴模型本身，而 Astra 拿不到。但它值得國科會的補助配置與博士培育放進視野：當搜尋與形式化的邊際成本大幅下降，真正稀缺的會變成「有能力判斷該問什麼、以及形式化對不對」的人。
下次看到「AI 解開某某難題」，先問三件事
這是我認為讀者最該帶走的東西，比這則新聞本身耐用得多：
- 有沒有可驗證的產物？ 有 Lean 檔、有能跑的程式碼、有可重現的資料，跟只有一篇部落格文章，是完全不同的兩種宣稱。
- 誰驗過了？ 「可以被驗證」不等於「已經被驗證」。要看的是有沒有獨立的人真的跑過、讀過，而不是產物存在就算數。
- 形式化的是不是原本那個問題？ 這是最容易被跳過、也最需要人類判斷的一關。
同一套問法可以搬去用在別處。我們寫過 AI 大規模標記疑似論文工廠研究那件事，結論是同一個形狀：停在「初篩」很有價值，被當成「定罪」就要出事。而 AlphaFold 團隊被拆、AI 科學從專職團隊轉向通用模型這個趨勢，只會讓這類宣稱越來越密集——把判斷框架練起來，比追每一則新聞重要得多。
常見問題
OpenAI 說 Astra 解開十道數學難題，這件事確定了嗎？
還沒有。可確認的是 OpenAI 在 2026 年 8 月 1 日發布了報告，並把十份 Lean 4 形式化證明檔公開在 GitHub 上，任何人都能自己跑一次建置。但「解出這十道題」目前仍然是 OpenAI 的宣稱，尚未經過期刊同儕審查，外部數學家也還沒有時間逐題讀完並判斷新穎性。十題裡只要有任何一題後來被撤回，都會是很大的事。
什麼是 Lean 形式化證明？它能證明 AI 沒有出錯嗎？
Lean 是一種證明語言，每一個邏輯步驟都要寫到程式能自己檢查，編譯通過就代表推理在該形式系統裡沒有跳步。所以它能排除「看起來很有道理、其實有隱形漏洞」這種錯誤。但它只保證「在那個形式化陳述之下推理是對的」，不保證「那個陳述就是原本的猜想」——翻譯得對不對，仍然要由數學家判斷。
Astra 現在可以用嗎？跟 GPT 系列是什麼關係？
不能用。Astra 是 OpenAI 這次首度正式確認的下一代模型家族名稱，這十道題是由內部版本產出的，模型本身尚未發布，也沒有公開的釋出日期。據 the-decoder 報導，它預計會是首批走美國聯邦審查流程的模型。也就是說，外界目前無法自行測試模型，只能檢查它留下的證明檔。
十題裡有格密碼相關的結果，會影響台灣的後量子密碼遷移嗎？
短期內不會改變任何時程。那一題處理的是最近向量問題的近似困難度，方向是「提供更強的困難度證據」，不是破解密碼系統。反過來也不能因此鬆懈——最壞情況的困難度結果，跟實際系統依賴的平均情況安全性是兩回事。數位產業署 2025 年發布的《後量子密碼遷移指引》該怎麼跑，還是怎麼跑。
參考來源
- GitHub 官方：openai/ten-proofs — Lean certificates accompanying proofs in mathematics and theoretical computer science（2026-08-01，Apache-2.0、Lean 4.32.0 與 mathlib、
lake build All、十份 .lean 檔） - the-decoder：OpenAI announces its “next major model” Astra by dropping ten previously unsolved math solutions（2026-08-01，十題至少十年無進展、論證出自 Astra、聯邦審查流程）
- The Next Web：OpenAI says its next model, Astra, has solved ten open problems in mathematics（2026-08-01，非 sofic 群與 Gromov 1999、球堆積 1978、Connes、Ehrhart）
- Implicator.ai：OpenAI Says Astra Solved 10 Math Problems With Lean Proofs（2026-08-01，249 頁手稿、Sol 費率換算約 2,000 美元、Lean 通過不等於同儕審查）
- Leiden Declaration 官方：The Leiden Declaration on Artificial Intelligence and Mathematics（2026-06-02，國際數學聯盟背書，正確性責任屬人類作者、應發表於同儕審查場域）
- 數位產業署官方：數產署攜手後量子資安產業聯盟發布「後量子密碼遷移指引」（2025-04-16，NIST 與 NCSC 預計 2035 年全面停用傳統加密演算法）