![矽基前沿 [Si]gnals](/silicon-frontier-signals-logo.png){kind=logo}
還有多少集可以逃？AI 又解開十道數學難題
三萬七千行、零個未證步驟，定義也在同一個檔案裡
十份機器可驗證的數學證明昨天上了 GitHub。打開其中一份，會發現機器驗的東西比公告聽起來窄。
OpenAI 8 月 1 日公布十道數學與理論計算機科學難題的新結果，官方稱這些題目的主結果至少十年沒人推進、多數更久：高維球堆積的指數率、Connes 剛性猜想的反例、多色 Ramsey 數的超指數下界（順手解掉 Erdős 第 183 號問題）。研究員 Noam Brown 把做出這些結果的模型家族叫 Astra——但那份 249 頁的論文本體一次都沒寫過這個名字，只寫「an internal OpenAI model」，PDF 的中繼資料寫的也是「an internal model at OpenAI」。
真正新的東西是證書。十道題各附一份 Lean 4 形式化檔，公開在 openai/ten-proofs（Apache-2.0，台北時間 8 月 1 日下午建立），十個檔案加起來約 21 MB。
我們打開 Connes 剛性猜想那一份 ConnesRigidity.lean：37,374 行，零個 sorry（Lean 裡代表「這步先跳過」的標記）。最終定理把猜想的前提都寫進陳述了——ICC、Kazhdan 性質 (T)、有限生成、群 von Neumann 代數同構、群本身兩兩不同構。
但那些前提的定義，大多寫在同一個檔案裡，不是從 mathlib 拿的。 什麼叫 ICC、什麼叫群 von Neumann 代數、兩個代數「同構」算什麼，都是這份檔案自己定義的。這不是作弊，mathlib 本來就沒有群 von Neumann 代數，形式化時自己定義是常態——重點是信任被搬到哪裡去了。Lean 會保證從定義推到結論一步不漏；它不會告訴你那些定義就是數學界在講的那些東西。那一段還是人要讀。
👉 對你的差別在這裡：「機器驗證過」保證的是推導，不保證題目。 你叫 agent 寫測試、測試全綠，是同一個結構——斷言也是它寫的。判準只有一句：驗證產物值多少，取決於命題是誰定義的，不取決於檢查器有沒有回綠燈。
論文自己還寫了一件值得記的事。Connes 那一章的致謝提到，準備手稿期間他們得知數學家 Shuoxing Zhou 獨立且同時做出同一個反例，而那份工作「部分借助 GPT-5.6 Sol」完成——那是你現在就叫得到的模型，不是內部版。功勞怎麼記這條線，我們7 月 19 日追過一次。另外據報導，Astra 會是第一個走美國政府發布前審查的模型，而那道閘的期限昨天剛到。
本篇是文件檢視：我們讀了 ConnesRigidity.lean 的最終定理陳述、數了行數與 sorry 數，但沒有跑 lake build 編譯，也沒有判斷數學內容對錯的能力；Shuoxing Zhou 那份工作我們沒查到公開預印本。「至少十年沒人推進」與「首個走政府審查」是官方說法與媒體轉述。
SOURCES
- AGitHub：openai/ten-proofs（十份 Lean 4 形式化檔、README、授權與建立時間）
- ATen Advances in Mathematics and Theoretical Computer Science（OpenAI 論文 PDF，249 頁）
- ATen advances in mathematics and theoretical computer science（OpenAI 官方公告頁）
- BOpenAI announces its "next major model" Astra by dropping ten previously unsolved math solutions（the decoder，2026-08-01）
- BOpenAI releases ten Astra math proofs with Lean certificates（AI Weekly）
來源分級:A = 一手公告/論文/官方文件 · B = 可信媒體 · C = 可參考但需脈絡 · D = 觀察用，不可當事實。
本文由 AI 協助研究與起草，矽基前沿編輯部編修，總編輯廖玄同審閱定稿。 編輯方針與 AI 使用說明
