新智元報道

編輯：傾傾

【新智元導(dǎo)讀】2026數(shù)學(xué)界直接寄了！頂尖學(xué)者未能推進(jìn)的證明被跑通，連菲爾茲獎得主也被指出論文邏輯瑕疵。當(dāng)AI智能體能自主接管真理的驗(yàn)證權(quán)時，現(xiàn)有的科研范式還能維持多久？

太離譜了！數(shù)學(xué)界被AI Gauss洗劫了。

僅5天，它就啃完了人類15月都啃不動的硬骨頭。

Viazovska 8維+24維球填充證明，硬轉(zhuǎn)成20萬行Lean代碼，90倍效率碾壓！

人類精英 VS AI？純屬算盤懟量子，根本打不過。

網(wǎng)友吐槽：救命，這AI卷瘋了，DeepMind都得認(rèn)慫？

Gauss給菲爾茲獎主發(fā)「糾錯郵件」

8維和24維的證明針對的是球體堆積問題。

在n維歐幾里得空間中，如何將相同大小的球（無重疊）盡可能密集地排列，并證明特定格子達(dá)到最優(yōu)。

這個問題已有數(shù)百年歷史。在大多數(shù)維度難以嚴(yán)格證明最優(yōu)，但8維和24維是特殊維度。

2022 Viazovska靠8維E8+24維Leech晶格球填充爆殺全場，成第二位女菲獎得主。

論文傳送門：http://arxiv.org/abs/1603.04246

論文傳送門：https://arxiv.org/abs/1603.06518

但現(xiàn)在，AI卷上來了！

Viazovska的論文有幾十頁，人類邏輯壓縮成自然語。

但電腦眼里，「理應(yīng)如此」這種詞根本不能理解。

在Gauss介入之前，一個團(tuán)隊(duì)耗時15個月，試圖將這一菲爾茲獎成果進(jìn)行Lean形式化。

但受制于人類認(rèn)知帶寬的限制與注意力衰減，工程推進(jìn)緩慢。

從15個月到5天，人類處理超大規(guī)模邏輯鏈條的算力已經(jīng)觸達(dá)上限。

8維證明形式化：AI狠戳菲獎?wù)撐蔫Υ?/strong>

Gauss底層是推理智能體閉環(huán)，碾壓老代碼。檢索模塊狂掃千篇文獻(xiàn)補(bǔ)背景，重構(gòu)模塊直轉(zhuǎn)Lean代碼+實(shí)時編譯驗(yàn)證。

處理Viazovska 8維E8模系數(shù)時，Gauss發(fā)現(xiàn)了30個邏輯瑕疵。

在Lean社區(qū)中，這些尚未被機(jī)器驗(yàn)證的步驟通常被標(biāo)注為「sorry」。

而對于人類開發(fā)者而言，填補(bǔ)這些「sorry」意味著需要查閱巨量的文獻(xiàn)，并將其翻譯成機(jī)器能識別的語法。

轉(zhuǎn)折點(diǎn)出現(xiàn)在論文第14頁的一處不等式推導(dǎo)。

Gauss在連續(xù)執(zhí)行4096次推理步進(jìn)后，反饋了編譯錯誤，并指向了原論文中的一處排版與微觀邏輯瑕疵。

在沒有人類干預(yù)的情況下，Gauss通過自主搜尋歷史定理庫，重構(gòu)了這一步的邊界條件，并補(bǔ)全了這段缺失的證明。

在此之前，人類數(shù)學(xué)家始終作為邏輯的主理人，AI僅負(fù)責(zé)執(zhí)行；而現(xiàn)在，Gauss展現(xiàn)出了比人類更敏銳的糾錯直覺。

對于學(xué)界而言，8維證明的完全形式化本身就是一個分水嶺。

它不僅產(chǎn)出了數(shù)萬行高質(zhì)量的Lean代碼，更證明了推理智能體具備識別并修復(fù)人類邏輯盲點(diǎn)的能力。

這種能力將數(shù)學(xué)驗(yàn)證從模糊地帶，推向了100%可運(yùn)行的數(shù)字絕對值。

24維證明：零藍(lán)圖自主重構(gòu)

在數(shù)學(xué)界，24維空間的Leech Lattice遠(yuǎn)比8維的E8晶格復(fù)雜。

Gauss這一次沒有任何預(yù)設(shè)的藍(lán)圖可以參考，其復(fù)雜程度顯著高于8維情況。

在8維證明的形式化過程中，人類團(tuán)隊(duì)已經(jīng)提前在Lean社區(qū)搭建了腳手架，標(biāo)注了大量的「sorry」作為導(dǎo)向。

但在24維證明中，Gauss面對的是一片邏輯真空。

24維球體填充證明的難點(diǎn)在于，它深度耦合了關(guān)于Leech晶格唯一性的復(fù)雜群論證明。

Gauss展現(xiàn)出的核心突破是無藍(lán)圖推理。

在證明Leech晶格是24維空間中唯一能夠?qū)崿F(xiàn)最大密度的結(jié)構(gòu)時，Gauss表現(xiàn)出了超強(qiáng)的文獻(xiàn)綜合能力。

論文傳送門：https://arxiv.org/abs/2601.04567

系統(tǒng)通過其檢索模塊，定位了數(shù)十篇跨越30年的關(guān)聯(lián)論文。

它理解了Viazovska原始論文的邏輯主線，通過跨文獻(xiàn)比對，自行識別出需要引入的外部引理，例如關(guān)于Co0康威群的對稱性特征。

在24維證明的深度推進(jìn)中，Gauss需要生成并驗(yàn)證超過12萬行的Lean代碼。

在這一規(guī)模下，任何由于上下文理解偏差導(dǎo)致的邏輯漂移，都會引發(fā)指數(shù)級的報錯崩潰。

Gauss通過推理鏈條都監(jiān)控，實(shí)時計算每一個推論步驟的置信度。當(dāng)置信度低于閾值時，它會觸發(fā)回溯機(jī)制，重新檢索數(shù)學(xué)公理庫。

在24維證明的第2048個邏輯塊中，Gauss獨(dú)立補(bǔ)全了拉普拉斯算子在特定流形上的譜隙估計。

這一步在原論文中被視為「顯而易見」的結(jié)論，但在形式化驗(yàn)證中，它需要近萬行的證明代碼。

Gauss僅用14小時就完成了這段邏輯的填補(bǔ)。AI對高難度智力活動的重塑，變成了全流程科研鏈條的自主接管。

在邏輯驗(yàn)證的競技場上，人類已經(jīng)不再不可或缺。

范式轉(zhuǎn)移：數(shù)學(xué)證明的工程化紀(jì)元

長期以來，數(shù)學(xué)證明的傳播媒介是自然語言論文。這種媒介形式雖然靈活，卻伴隨著極高的理解門檻與邏輯驗(yàn)證成本。

Gauss的出現(xiàn)，標(biāo)志著數(shù)學(xué)正從自然語言文學(xué)轉(zhuǎn)向可運(yùn)行的軟件工程。

Math,Inc.首席執(zhí)行官Jesse Han將這一轉(zhuǎn)變比作計算機(jī)科學(xué)從打孔紙帶時代進(jìn)入高級語言時代。

在打孔紙帶時代，程序員需要關(guān)注每一個底層的物理比特；而在高級語言時代，開發(fā)者得以站在抽象層級上構(gòu)思復(fù)雜的系統(tǒng)邏輯。

Jesse Han認(rèn)為：

這種技術(shù)的最終結(jié)果將是解放數(shù)學(xué)家……讓他們?nèi)粝胄碌臄?shù)學(xué)世界。

未來數(shù)學(xué)家將轉(zhuǎn)向更高的架構(gòu)設(shè)計，數(shù)學(xué)證明等工作將由類似Gauss的推理智能體自動完成。

數(shù)學(xué)作為所有自然科學(xué)的底層語言，其工程化進(jìn)度的加快，將直接傳導(dǎo)至密碼學(xué)、量子計算、航天軌道計算等強(qiáng)邏輯領(lǐng)域。

在這種新范式下，人類將作為指揮家，繁重的演繹推理則交給具備ASI潛力的智能體。

Maryna Viazovska曾被視為人類智力的巔峰，如今它已轉(zhuǎn)化為服務(wù)器中202000行的比特。

在這個真理不再需要人類中介的時代，我們是否有勇氣沿著AI開辟的路徑，去觸碰那些超越人類直覺的未知疆域？

參考資料：

https://spectrum.ieee.org/ai-proof-verification?share_id=9202657&utm_campaign=RebelMouse&utm_content=IEEE+Spectrum&utm_medium=social&utm_source=twitter

https://x.com/mathematics_inc/status/2028542388717986135?s=20