AI證偽百年數(shù)學(xué)猜想被打假！Lean證明驚現(xiàn)漏洞，哥大教授破防了

新智元報(bào)道

OpenAI內(nèi)部最新推理模型，一口氣發(fā)布了十項(xiàng)驚人的數(shù)學(xué)進(jìn)展。

其中包括：

• 首次證明了非Sofic群（Non-sofic groups）的存在性 ；

• 給出了全新的電路下界（Circuit lower bounds）；

• 攻克了最近向量問題（Closest Vector Problem，CVP）難度極限；

• 以及雙人量子博弈并行重復(fù)指數(shù)衰減定理（Quantum parallel repetition）。

最令哥倫比亞大學(xué)副教授Henry Yuen在乎的是最后一個(gè)——

2016年，Yuen在該問題上取得了重大進(jìn)展，但并未徹底解決。10年來，他屢戰(zhàn)屢敗，甚至一個(gè)月前他還用ChatGPT 5.5再次向終極證明沖鋒，但收獲寥寥。

而AI在他的肩膀上，輕輕一腳，把球送進(jìn)了球門。

證明對(duì)了，人類卻沒理解

幾天前，Lijie Chen發(fā)給Henry Yuen和另外幾個(gè)人一份論文草稿。

當(dāng)時(shí)生活很忙，他無暇深入研讀。現(xiàn)在，論文已經(jīng)公布。他不吐不快，有話要說。

量子并行重復(fù)定理（Quantum parallel repetition theorem），是Henry Yuen在研究生階段耗費(fèi)數(shù)年心血鉆研的領(lǐng)域，也是他最引以為傲的成果。

Henry Yuen，現(xiàn)任哥倫比亞大學(xué)Srivani Family計(jì)算機(jī)科學(xué)副教授

他記得那些泡在咖啡館里的午后，坐在辦公室里的深夜，還有無數(shù)個(gè)本該休息的周末，反復(fù)拆解研讀Ran Raz的經(jīng)典并行重復(fù)定理。

他想解決這個(gè)定理的量子版本，為此夜不能寐、輾轉(zhuǎn)反側(cè)。他吞下了成噸的數(shù)學(xué)工具，最終成功證明了多項(xiàng)式衰減。

https://arxiv.org/pdf/1604.04340

更重要的是，他從中建立了信心，終于認(rèn)清自己的實(shí)力，證明了他確實(shí)能解決那些（至少一部分）別人也在乎的問題。

他相信OpenAI的這份證明應(yīng)該是正確的，畢竟已經(jīng)有Lean形式化證明。但要消化這個(gè)新證明，Henry Yuen還需要一些時(shí)間。

雖然新證明確實(shí)從他之前結(jié)束的地方繼續(xù)出發(fā)，但AI突破了他原有證明策略的限制，使用了一些技巧和方法。這些方法或許已經(jīng)被算子理論（operator theory）和泛函分析（functional analysis）領(lǐng)域的研究者所掌握。

興奮之外，Yuen的第一個(gè)感受是失望，對(duì)論文寫作風(fēng)格的失望。

他說這份證明讀起來滿是AI味兒：冗長(zhǎng)的鋪墊繞了半天，關(guān)鍵環(huán)節(jié)卻像變魔術(shù)，讓人一頭霧水。

OpenAI的證明，讀來頗有意思，卻也有些令人頭疼。

它先把問題端端正正地?cái)[在桌上，然后忽然一躍到「用預(yù)解式去找正確的purification」這個(gè)方向，中間幾乎不留任何邏輯階梯。

接下來，便是一連串頗為另類的矩陣熵計(jì)算，彎彎繞繞地算下去，末了告訴你：這條路走得通。

可那最關(guān)鍵的一步，那個(gè)直覺究竟從何而來，它沒有說。

而最精妙、最考驗(yàn)創(chuàng)造力的那一筆——利用Uhlmann 變換（Uhlmann transformation）進(jìn)行算子空間膨脹的技巧，本應(yīng)是整篇證明最動(dòng)人心魄的高潮，卻被AI棄子如泥沙，毫無預(yù)警、毫無解釋地丟在了第四節(jié)。

正確的證明，卻藏起來了最重要的想法。

他希望OpenAI能多花幾個(gè)提示詞，把這篇文稿好好理一理。

更扎心的是第二層：Lean驗(yàn)證通過，不等于理解。

機(jī)器可以保證每一步推導(dǎo)無懈可擊，但「為什么這一招有效」「它在更大的理論版圖里意味著什么」「還能用在哪里」——這些問題，Lean一個(gè)都答不了。

Yuen坦言，他到現(xiàn)在還在消化這份證明。

答案擺在面前，他卻要像讀外行的論文一樣，一行行去還原AI沒說出口的直覺。

沒錯(cuò)，是有個(gè)Lean證明在那兒。可那只是形式化，不代表我懂了。真要消化，恐怕只能靠時(shí)間慢慢磨。

的確，AI拓寬了人類理解的疆域，但然后呢？研究的樂趣和意義還剩什么？要是AI把他魂?duì)繅?mèng)繞的難題都解決了，他還剩什么？

問題接踵而至。但有一點(diǎn)他越來越確定：數(shù)學(xué)家接下來的日子不會(huì)閑，既要馴服這些思想巨獸，還得把它們的黑話翻譯成人話。

AI「證偽」百年數(shù)學(xué)猜想被打假！

Lean也不是保險(xiǎn)箱

上周，Ramana Kumar用300行Lean證偽了最出名的數(shù)學(xué)未解之謎「科拉茲猜想」（Collatz conjecture）。

它問的問題特別簡(jiǎn)單：給你一個(gè)正整數(shù)，按兩條規(guī)矩反復(fù)操作——偶數(shù)就除以 2，奇數(shù)就乘以3再加1——最后是不是不管從哪個(gè)數(shù)出發(fā)，都會(huì)一路跌到1？

你可以算一下：

這個(gè)猜想說的就是：不管你拿哪個(gè)正整數(shù)開頭，最后都會(huì)掉進(jìn)這個(gè) 4→2→1 的圈里。

這個(gè)問題自數(shù)學(xué)家Lothar Collatz在1937年提出后，沒有人能證明它成立，也沒有找到反例。

它被數(shù)學(xué)家Paul Erd?s稱為：「數(shù)學(xué)還沒準(zhǔn)備好應(yīng)對(duì)這樣的問題」，而美國科學(xué)院院士、數(shù)學(xué)家Jeffrey Lagarias則認(rèn)為「這是個(gè)異常困難的問題，完全超出了當(dāng)今數(shù)學(xué)的范圍」。

如果被證偽，無疑是數(shù)學(xué)界爆炸性新聞。

可惜的是，3天后，這份形式化的Lean證明被判無效，因?yàn)樗鼘?shí)際上只是利用了Lean內(nèi)核的一個(gè)底層漏洞。

OpenAI的Daniel Selsam，帶著一個(gè)專攻網(wǎng)絡(luò)安全方向的 AI，協(xié)助Lean FRO做了一次內(nèi)核審計(jì)。

結(jié)果，他們?cè)贚ean內(nèi)核里發(fā)現(xiàn)了不止一起漏洞！

幾乎同一時(shí)間，Rutgers大學(xué)數(shù)學(xué)教授、Lean專項(xiàng)研究組織顧問Alex Kontorovich發(fā)文提醒：別把Lean當(dāng)全能驗(yàn)證者。

他直指死穴——語義對(duì)齊（Semantic Alignment）。

即使Lean內(nèi)核無懈可擊，Lean也只管代碼編譯。誰來確保你寫在代碼里的「定義」和人類在自然語言里的「直覺意圖」是一回事？

Lean能確認(rèn)的只有一件事：代碼編譯通過，形式邏輯無誤。但它絕不驗(yàn)證一個(gè)更要命的問題：這段形式化陳述，真的對(duì)應(yīng)你想證的那個(gè)定理嗎？

定理證對(duì)了，題目抄錯(cuò)了，Lean照樣綠燈放行。

而這個(gè)對(duì)齊問題，沒法純靠計(jì)算機(jī)解決。

在ICM 2026的演講里，Kontorovich就點(diǎn)過：形式化數(shù)學(xué)最大的盲區(qū)，不在「推對(duì)了導(dǎo)」，而在「說對(duì)了話」。最后把關(guān)的，還得是人類專家。

當(dāng)年Liquid Tensor Experiment之所以封神，靠的恰恰是研究者對(duì)每個(gè)數(shù)學(xué)定義近乎偏執(zhí)的人工審查。

把兩位教授的話放在一起看，指向同一個(gè)事實(shí)：AI能證明，機(jī)器能驗(yàn)證，但理解和把關(guān)，還是人類的活。

最后，還有個(gè)關(guān)于AI推理模型的八卦：

參考資料：

https://www.henryyuen.net/posts/on-openai-and-quantum-parallel-repetition/

https://x.com/AlexKontorovich/status/2083919186825236831

https://x.com/henryquantum/status/2083623700608237956

編輯：大衛(wèi)