零道歉，一個大星號：深入OpenAI的十個機器驗證證明
專欄概述
2026年8月1日，OpenAI發布了一份手稿，若在兩年前聽起來會像虛構小說：其下一代模型的未發布內部版本，代號Astra，為十個至少十年未解的問題生成了完全機器驗證的Lean 4證明，涵蓋群論、算子代數、球堆積、電路複雜性和拉姆齊理論。這份249頁的文件附帶一個GitHub存儲庫，其中包含採用Apache 2.0許可的證明證書，而大家反覆提及的細節是Lean代碼中的「sorry」計數為零——這意味著沒有步驟被留作未證明的佔位符，沒有漏洞被假設掩蓋。每一行都經過證明助手檢查，該助手不在乎聲譽、炒作週期或論文作者是誰。
實際解決了什麼
頭條結果是對非sofic群的顯式構造，解決了Mikhail Gromov在1999年定義soficity時提出的問題。單單這一項就足以成為人類數學家的職業生涯定義性成果。與此並列的還有對Connes關於群馮諾依曼代數的剛性猜想的一個反例，這是一個歷史上進展以十年計而非以月計的子領域。手稿還報告了高維球堆積的漸近上界改進——這個問題的公眾形象很奇怪，因為八維和二十四維的情況因Maryna Viazovska的著名工作而聞名，而一般高維漸近性則相對不引人注目且頑固。其餘十項結果涉及電路複雜性和拉姆齊理論，這兩個領域歷史上組合爆炸使得計算機輔助搜索要么不可行，要么即使可行也缺乏說服力。
這份清單與通常的「AI解決數學問題」的新聞週期不同之處在於驗證層。Lean不會按曲線評分。經Lean檢查的證明要么能針對形式陳述編譯，要么不能，沒有審稿人需要討好，沒有導師需要安撫，沒有委員會需要滿足。這與「模型產生了專家認為合理的證明草圖」的說法有本質區別，後者更接近早期AI數學公告的實際情況。
反響分歧
在職數學家的反應確實存在分歧，而且並非沿著典型的AI炒作故事所預期的路線。Timothy Gowers擁有菲爾茲獎，且長期對誇大的AI主張持懷疑態度，他表示會毫不猶豫地推薦其中一個證明給頂級期刊——這是一位不會輕易給出認可的人的真正背書。Thomas Bloom在曼徹斯特大學管理Erdos問題目錄，因此對「未解」在實踐中的含義有最清楚的認識，他稱這些結果為「重大新聞」。
但熱情並非一致，懷疑態度值得認真對待，而非視為條件反射的守門行為。葉史瓦大學的Steven Miller指責OpenAI在產生這些結果時實際上借鑒了他自己發表的研究而未註明出處——這項投訴與一般的「AI偷了我的內容」的不滿不同，因為它來自特定數學社區內部，該社區數十年來發表的引理和技術正是這類模型所需的訓練基礎。而且時機並非中立：萊頓宣言現已獲得國際數學聯盟的認可，已發出警告，指責AI公司未經同意利用已發表的數學研究，繞過同儕審查，並對該領域長期依賴的註明出處和證明規範施加壓力。這項公告正好落在這場爭論之中，而非之前。
2,000美元的問題
OpenAI自身的框架大力強調成本：按當前API費率，約2,000美元的計算成本產生了十個證明，而數學界集體花費超過一百人年未能解決。這是一個驚人的數字，而且設計上就是為了驚人。但該數字僅涵蓋成功運行——它未提及有多少嘗試未成功，有多少候選證明被生成並丟棄，或有多少計算投入到未納入手稿的問題中。批評者迅速指出，這使得2,000美元成為發表成本，而非發現成本。這相當於公司只報告盈利交易：就其所涵蓋而言是真實的，但如果你想估計過程的實際經濟性，這不是你要的數字。
還有一個在興奮中容易忽略的可重現性問題。OpenAI外部無人能運行Astra——它是一個未發布的內部版本，而非已發佈的產品。因此，證明本身可以獨立檢查，因為Lean是開放的，證書是公開的。但產生證明的過程無法由其他人獨立重複。這是一個不尋常的認識論立場：輸出層面完全透明，方法層面完全不透明。值得深思這一區別，因為「已驗證」和「可重現」在這裡扮演不同角色，混淆它們正是準確的新聞稿變成誇大的公眾敘事的方式。
同樣值得注意的是，這項公告沒有聲稱什麼。早期OpenAI的數學公告有時會附帶廣泛的外部審查或專家驗證的聲明；這次沒有這樣做。這裡的背書——Gowers、Bloom——更像是個人反應，而非精心策劃的審查過程，OpenAI似乎依靠Lean的形式驗證來承擔可信度工作。這可以說更誠實，但也意味著社區的非正式審查——通常通過研討會、審稿報告和多年試圖找出結果漏洞的方式——尚未對數學實質內容進行，即使形式邏輯已通過檢查。
對照本週其他事件解讀
這一切並非發生在真空中。在同一段時間內，OpenAI將GPT-5.6「Luna」的定價削減約80%，降至每百萬輸入代幣0.20美元，而ChatGPT據報導每週活躍用戶數約達十億。歐盟AI法案的透明度和標籤要求也於8月2日生效。將這些與數學公告放在一起，一個模式浮現：一家公司同時在價格和規模上競賽其消費產品，同時試圖在最困難的領域——純數學——插旗，在那裡「幻覺」不僅是煩惱，而是範疇錯誤，因為錯誤的證明根本無法編譯。
這正是Lean驗證細節比2,000美元數字或用戶數里程碑更重要的原因。價格戰和使用量是商業指標，可以朝任一方向解讀。形式證明檢查器中的零「sorry」計數則無法以同樣方式解讀——它要么為真，要么存儲庫無法編譯。有趣的張力在於，這個最困難、最可驗證的主張也是以最少可重現性、包裹在最具爭議的註明出處問題中到來的，恰逢數學界圍繞萊頓宣言組織起來，抵制AI實驗室使用已發表研究。Astra是否代表數學發現的真正階段性變化，還是從更大、更混亂的搜索過程中精心挑選的精彩片段，這個問題需要未來一年的審查來回答，而非這一份手稿。