10 月 6 日OpenAI 在 GitHub 上一次性公開了 722 篇數(shù)學手稿聲稱在幾何、代數(shù)、計算機科學等方向的 372 個問題上取得進展。第二天撤回 3 篇一個符號錯誤讓其中一篇的論證失效另外兩篇依賴了同一個構造一并作廢同時修訂 14 篇還改了一處過時引用。手稿總數(shù)從 722 變成 719。這批東西沒走同行評審也沒發(fā)在 arXiv而是直接傳到自家倉庫。據(jù) OpenAI 方面對媒體的說法錯誤是內(nèi)部審計時發(fā)現(xiàn)的約一半結果在發(fā)布時并未經(jīng)過確認合作方 AGMAI 的建議是不必等完全形式化再發(fā)。10 月下旬陶哲軒和鄧煜在一場對談里把這類產(chǎn)出稱作有毒廢料——這話針對的不是 AI 會不會做數(shù)學而是把解數(shù)學題當基準測試這種做法。技術上看變的是發(fā)布方式AI 能不能做數(shù)學兩位數(shù)學家都沒否認甚至看好它在真正的研究里加速。爭的是產(chǎn)出和驗證之間的順序被調(diào)換了。以前的路子是人有想法AI 補細節(jié)寫完自己核一遍。現(xiàn)在的路子是AI 批量生成人來做驗收。據(jù)報道這批手稿來自約 4000 次會話產(chǎn)出 722 篇成功率不到兩成——這個比例本身不算丟人問題是剩下那八成里有多少被當成結論發(fā)了出來。生產(chǎn)端的邊際成本接近零驗證端的成本一點沒降。甚至更高讀一份沒有思維鏈、引用不透明、符號還可能有錯的證明比自己做一遍更累。鄧煜提的兩條邊界說的就是這個——過去有證明的問題和人類理解的問題是同一條線現(xiàn)在中間裂開了一條有證明但只有 AI 知道人不懂。這跟寫業(yè)務代碼是一回事看著離得很遠其實是同一個結構。AI 生成代碼的成本已經(jīng)很低低到不少團隊開始用每天合入多少 PR衡量效能。但驗證成本沒變code review 要人看測試要人寫線上出事要人背。產(chǎn)出量一旦成了 KPI被壓縮的一定是驗證環(huán)節(jié)。表現(xiàn)是 review 從逐行看變成掃一眼 CI 綠了就過測試從覆蓋邊界變成跑通主流程。賬不會消失只是從開發(fā)階段挪到了故障復盤會上。Lean 這類形式化工具本來是條出路——證明可以機器校驗不依賴人的耐心。但據(jù)報道這批手稿里大量文字證明和 Lean 代碼之間存在斷層形式化覆蓋并不完整。工具在覆蓋率不夠約等于沒有。三個能落地的做法一、把驗證做成流水線別指望自覺。類型檢查、lint、單測、集成測試該卡的卡住。人一定會偷懶機器不會。二、獨立復算別讓模型自證。讓生成答案的同一個模型去檢查答案等于讓它給自己判卷。能用確定性方法驗的就別用概率方法驗。比如下面這段fromfractionsimportFractiondefcheck(n_max50):用精確有理數(shù)復算 sum(k^3) (n(n1)/2)^2返回第一個反例。forninrange(1,n_max1):lhssum(Fraction(k)**3forkinrange(1,n1))rhsFraction(n*(n1),2)**2iflhs!rhs:returnn,lhs,rhsreturnNoneprint(check(200))# None表示 1..200 全部成立跑 1 到 200 返回 None全部通過。這不是證明只是低成本證偽——但對 AI 產(chǎn)出來說絕大多數(shù)錯誤死在這一步就夠了。這里用 Fraction 而不是 float因為浮點誤差既會制造假陰性也會掩蓋真問題。三、留痕。記錄 prompt、模型版本、生成時間、人工改動。出問題時這段到底是誰寫的、怎么來的必須有答案。AI 不會背鍋簽字的那個人會。幾個坑LLM 自評不可靠。讓模型輸出我已仔細檢查沒有任何信息量它對自己的錯誤沒有感知能力語氣卻一樣篤定。形式化驗證有成本。寫 Lean 比寫自然語言證明慢得多只值得用在高價值、高風險的斷言上全量上不現(xiàn)實?？雌饋韺κ亲钗ｋU的信號。符號錯誤、量詞順序、隱含假設這些地方 AI 出錯時讀起來依然通順而人讀的時候會自動腦補缺失的一步。最后陶哲軒在那場對談里用了個開車的比喻車確實比走路快但不是所有原本走路的路都該換成開車——有時候你就是想走一走。放到工程上也成立。生成成本趨近于零之后稀缺的東西不再是產(chǎn)出而是誰來驗、驗到什么程度、驗不出來的時候敢不敢說不。你怎么看評論區(qū)聊聊。