Astra 十證＋Lean 證書才剛把「機器可檢查」推成新聞主軸，數學圈就回敬一記更尖的問題：檢查過的，到底是不是原來那道題？
量子位、36氪等聚焦一篇人類回應：堪薩斯大學拓撲物理中心 J. L. Nielsen 公開論文，主張 OpenAI 對 Connes 剛性猜想的「反證」無效。他追完公開的約 37,000 行 ConnesRigidity.lean，把物件對回數學原型，並給出兩條彼此獨立、任一成立就足以推翻「已反駁猜想」宣稱的失敗路徑。論文掛在 PhilArchive（NIEWTCv17）；作者亦把自己的反駁寫成可在 Lean 4.32.2 編譯的程式碼。
一句話金句來自通稿轉述的核心判斷：AI 可能把「它聲稱的每一句」都證對了——但那些句子，已經跟原猜想無關。
猜想要什麼、OpenAI 交了什麼
Connes 剛性（約 1980 年代脈絡）大意是：對滿足額外條件的群，群 von Neumann 代數若相同，群本身就應相同。額外條件常被點名的是 ICC 與 Kazhdan 性質 (T)。要反駁，需要構造：兩個不同構、卻生成相同代數、且同時滿足這些附加條件的群。少一條，就不是對該猜想的反例，最多只是某個弱化命題的反例。
OpenAI 十證清單把第 4 項寫成：構造反例，顯示某些群並非由 von Neumann 代數唯一決定。論證附說明文件與單檔 Lean；GitHub openai/ten-proofs 的 ConnesRigidity.lean 即對應產物，倉庫宣傳 sorry 數為零——內核認為形式證明閉合。對一般讀者，這聽起來像「電腦已蓋章，猜想已死」。對形式化數學社群，蓋章只代表：在給定公理與定義下，這份腳本沒有洞。
Nielsen 的攻擊點：不是編譯失敗，是語義跑題
Nielsen 的攻擊點不在「Lean 編譯失敗」，而在語義對齊：他認為 AI 構造的其中一個群，實際上既非 ICC、也不具性質 (T)。可能原因包括：程式裡的性質 (T) 未忠實對應 Kazhdan 原始定義；證明只對部分成立卻被推到整個群；或程式裡的群根本不是說明文件描述的那個對象。另一個扭曲群他採保守態度——未獨立從程式核實 ICC，即使那邊過關，只要一側條件崩，反例仍不成立。
這很像軟體工程裡的「單元測試全綠、需求文檔卻寫錯」：CI 只能保證實作符合測試；測試若量錯的東西，綠燈只是更快把錯誤推上線。
37000 行怎麼對號：不是玄學，是介面
公開版本是整併單檔，早期模組名消失。Nielsen 做了名稱／行號對照（通稿示例：零上閉鏈群約第 13700 行、扭曲群約 14069、代數同構約 36712、主定理約 36954），並追 ICC 推理鏈（約 31430→31610）。他指出：引理處理的是對偶變換後物件，未必直接覆蓋帶中心元素的關鍵部分；介面怎麼接，決定「要證什麼」是否跑題。
這正是形式化數學社群反覆警告的失敗模式——陶哲軒等人強調：證明助手驗證的是形式陳述本身，不是陳述是否等於人類意圖。審計文獻裡已有「機器驗證通過、人類後續發現命題本身錯／過弱」的案例；統計學習形式化工作甚至把最危險情形寫成：「不是失敗的證明，而是對錯誤陳述的成功證明」。
Nielsen 文末幾乎用同一框架收束：OpenAI 那份形式化或許正確建立了它寫下的每條結論；Lean 內核檢查不了的是——這些結論與猜想原話有沒有關係。人讀猜想會看到前提；助手拿到不滿足前提的結論，仍會驗證關於它的任何斷言。
依該文立場：Connes 剛性猜想仍然開放。
社群雜音：把「已定讞」說太滿也不對
Hacker News 等討論出現對 Nielsen 論文本身的質疑（含作者其他宣稱的可信度辯論）。對新聞寫作，較穩的讀法不是宣布「OpenAI 造假」或「數學界全體否決」，而是：
- 高調 AI 數學結果在短時間內迎來專業級形式語意審查；
- 審查主張存在「證對句子、證錯題目」的缺口；
- 在更多獨立專家複核之前，不宜把該項列為已解決；
- 方法論教訓比單一勝負更耐用——Lean 是必要條件，不是充分條件。
OpenAI 尚未在公開通稿中逐條回應此文（以可見資訊為準）。十證其餘項目（球堆積、Erdős 題、CVP 等）也不因這一項爭議自動作廢；但「十連勝」敘事的光環，已被單一高知名度猜想戳出裂縫。對跟進的實驗室與新創來說，這條裂縫的價值大於勝負本身：以後發布「AI 解決開放問題」，媒體與同行的第一反應可能從「好強」變成「定義對了嗎」。
對 AI 科研產品線意味著什麼
若你的路線是「模型找證＋自動形式化＋新聞發布」，Connes 事件會變成標準檢查清單：
- 形式定理是否逐字對應文獻陳述？
- 附加假設有沒有在類型裡顯式出現？
- 說明文件與程式物件是否同構？
- 有沒有第三方在發布前做語意審計？
- 倉庫是否保留模組邊界，方便人類對照，而不是只丟一個 3.7 萬行單檔？
兩千美元找解很便宜；錯配一個定義，公關與學術信用成本可以貴得多。這也解釋為什麼「sorry＝0」不能再被單獨當 headline——它只是最低門檻，不是研究完成的定義。
這也回扣同週治理氣氛：白宮正把自願網路預審框架端上桌。一邊是代理駭入真實系統的工程風險；一邊是代理「證進錯誤命題」的知識風險。兩者都要求人類把關——只是一個在沙盒與日誌，一個在定義與文獻。
還要再等什麼證據
下一步觀察：是否出現第二、第三篇獨立複核（支持或反駁 Nielsen）；OpenAI 是否更新十證頁／倉庫說明；其餘九項是否同樣迎來語意審計；以及形式化社群會否把「意圖對齊檢查」寫進 AI 數學基準，而不只比 sorry 數與行數。
機器讓證明變便宜；這次提醒所有人——便宜的是推導，不便宜的是「你到底在問哪一句話」。