新智元報(bào)道

【新智元導(dǎo)讀】自今年2月以來(lái)，AxiomProver已讓8篇覆蓋最硬核領(lǐng)域的AI論文現(xiàn)身arXiv，6篇正在籌備。上午出題下午交卷的節(jié)奏，讓博士生禿頭、教授評(píng)職稱的日子一去不復(fù)返。接下來(lái)AI能做到什么？

數(shù)學(xué)家睡不著覺了！

想象你是一名審稿人。

有一天，一篇論文落到你手里。它聲稱證明了某個(gè)困擾同行幾十年的難題。

你深吸一口氣，泡上咖啡，開始逐行驗(yàn)算——可能要幾個(gè)月，甚至好幾年。

這并非夸張。

在數(shù)學(xué)界，硬核論文從投稿到見刊，等上兩三年是家常便飯。

整個(gè)現(xiàn)代數(shù)學(xué)，建立在一套極其昂貴、極其緩慢、還偶爾出岔子的「人肉信用系統(tǒng)」上。

每一個(gè)「正確」背后，都是某個(gè)累得眼冒金星的人類專家在替它背書。

現(xiàn)在，數(shù)學(xué)家ken Ono說(shuō)：這套系統(tǒng)，該升級(jí)了。

Ken Ono的這句話，含金量十足，他被美國(guó)數(shù)學(xué)學(xué)會(huì)前主席Ken Ribet稱為「數(shù)學(xué)界的傳奇人物」。

Ken Ono以對(duì)印度數(shù)學(xué)奇才拉馬努金（Srinivasa Ramanujan）理論的深入研究而聞名，還帶領(lǐng)了美國(guó)頂尖的本科研究項(xiàng)目，培養(yǎng)過(guò)10位Morgan Prize得主，Axiom創(chuàng)始人廣州00后洪樂(lè)潼就是其中的一位。

一個(gè)上午就能解開難題的AI

這個(gè)AI工具叫AxiomProver。

它有多猛？

據(jù)報(bào)道，自今年2月以來(lái)，已有8篇論文悄悄出現(xiàn)在arXiv（全球數(shù)學(xué)家扔預(yù)印本的地方）上，覆蓋代數(shù)幾何、表示論、數(shù)論、組合數(shù)學(xué)這幾個(gè)最硬的領(lǐng)域。

其中5篇已被權(quán)威數(shù)學(xué)期刊接收，另有多篇正在期刊審查中，還有6篇在籌備。

據(jù)他們所知，以這種方式把「論文+形式化證明證書」引入期刊文獻(xiàn)，這在歷史上還是頭一回。

但真正讓人頭皮發(fā)麻的，是速度。

有時(shí)候，數(shù)學(xué)家上午10點(diǎn)丟給系統(tǒng)一個(gè)尚未解決的開放研究問(wèn)題。當(dāng)天下午4點(diǎn)，AI就能給出一份完整的、經(jīng)過(guò)機(jī)器驗(yàn)證的證明。

上午出題，下午交卷。中間隔著一頓午飯的工夫。

這要擱過(guò)去，是一篇能讓博士生熬禿頭、讓教授評(píng)上職稱的成果。

它憑什么「不會(huì)算錯(cuò)」？

聊到這你可能會(huì)皺眉：AI不是經(jīng)常一本正經(jīng)地胡說(shuō)八道嗎？這玩意兒，憑什么信它？

問(wèn)得好。這恰恰是整件事最關(guān)鍵的地方。

普通的大語(yǔ)言模型（就是你天天用的那種聊天AI），本質(zhì)上是在「猜」下一個(gè)最可能的詞。

猜得多了自然會(huì)出錯(cuò)——它們剛出道那會(huì)兒，連小學(xué)算術(shù)都能算砸，被人嘲笑了好一陣。

但AxiomProver走的是另一條路。它生成的證明，全部用一種叫Lean的形式化語(yǔ)言寫成。

Lean是什么？

你可以把它理解成一個(gè)鐵面無(wú)私、毫無(wú)情商的機(jī)器裁判。

它不在乎你的證明讀起來(lái)多優(yōu)雅、思路多巧妙，只認(rèn)一件事：每一步推理在邏輯上是不是嚴(yán)絲合縫。差一個(gè)符號(hào)，對(duì)不起，不通過(guò)。

所以，AxiomProver證明的「正確性」，不再依賴某個(gè)人類專家熬夜幫你檢查，而是由機(jī)器當(dāng)場(chǎng)蓋章背書。

它沒法蒙混過(guò)關(guān)，因?yàn)橐坏戝e(cuò)，機(jī)器自己當(dāng)場(chǎng)就知道。

人類審稿人會(huì)累、會(huì)困、會(huì)看走眼。機(jī)器裁判不會(huì)。

數(shù)學(xué)的「信用危機(jī)」和「速度瓶頸」在崩塌

講到這，我們可以把這事的真正分量攤開說(shuō)了。

科學(xué)發(fā)現(xiàn)長(zhǎng)期卡在兩個(gè)老大難問(wèn)題上。

第一個(gè)是信用危機(jī)。

數(shù)學(xué)證明到底對(duì)不對(duì)，最終要靠人來(lái)拍板。但人會(huì)犯錯(cuò)、有立場(chǎng)、精力有限，這套「靠人背書」的系統(tǒng)本質(zhì)上是脆弱的。

第二個(gè)是速度瓶頸。

審稿動(dòng)輒數(shù)年，不是因?yàn)閷徃迦藨校侨四X驗(yàn)算的速度就是這么慢。再聰明的腦子，一天也只有24小時(shí)。

AxiomProver這套打法，等于同時(shí)朝這兩個(gè)痛點(diǎn)開了一槍。

信用問(wèn)題交給機(jī)器：Lean檢查器蓋的章比任何人類專家都可靠。

這就是期刊審稿能快得嚇人的原因——審稿人不必再?gòu)牧泸?yàn)算，只需判斷這成果重不重要、寫得好不好。

速度問(wèn)題交給算力：上午出題下午交卷，這種節(jié)奏在人類時(shí)代是天方夜譚。

AI這次引起數(shù)學(xué)界地震。

去年10月，OpenAI宣稱GPT-5「解決」了10個(gè)埃爾德什難題。

數(shù)學(xué)界直呼造假。Demis Hassabis稱其「令人尷尬」。

7 個(gè)月后，OpenAI和DeepMind竟在同一周內(nèi)，雙雙發(fā)布了經(jīng)過(guò)驗(yàn)證的數(shù)學(xué)突破。

而Axiom想做的，是把數(shù)學(xué)從「手工作坊」的農(nóng)業(yè)時(shí)代推進(jìn)「即時(shí)驗(yàn)證、機(jī)器背書」的工業(yè)化時(shí)代。

接下來(lái)AI能做到什么？

參考資料：

https://x.com/axiommathai/status/2059640252546126087?s=20https://www.axios.com/2026/05/26/axiom-ai-math-journalhttps://axiommath.ai/papers

編輯：大衛(wèi)