華人女學霸AI殺瘋！本科最難數賽12題全對，自主證明首次公開

在人類滿分都罕見的普特南數賽上，AI直接12題全對拿滿分。陶哲軒等大佬預言AI已經取得了重要里程碑，再加上GPT-5.2 Pro在數學上強到「離譜」的表現，那種「奇點將近」的直覺，真的壓不住了。

全網震撼！

今天，24歲華人女學霸Carina Hong初創打造的AxiomProver，在2025 Putnam數學競賽拿下了滿分成績。

12道題，AI全部答對！

與此同時，AxiomProver自主生成的Lean證明也正式公開。

這一競賽，堪稱北美本科生數學競賽的天花板級別，人類需在6小時攻克12道題。

Putnam競賽總分120分，要接近滿分極其罕見，通常只有Putnam Fellows（前幾名）才能做到。

網友表示，「AxiomProver拿下Putnam競賽比奪得IMO金牌更厲害，解決下一個千禧難題可能比預想的要來得更快」！

最近，陶哲軒公開表示，ChatGPT等AI鞠躬基本可以自主解決「埃爾德什問題」，瞬間登上HK熱榜。

OpenAI總裁Greg、科學家Sebastien Bubeck紛紛激動轉發。

看來，千禧年難題，或許離破解之日不遠了......

「本科最難數賽」奪下滿分，全網震撼

先來看看AxiomProver，如何在「本科版最難數學競賽」中拔得頭籌。

https://axiommath.ai/territory/from-seeing-why-to-checking-everything

在AxiomMathAI的官方博客中，把所有的Lean證明都公開了，還把題目分成了這么幾類：

人類直覺簡單，但形式化起來卻極為繁瑣的問題；

AI出人意料地攻克人類未曾預料到的問題；

AxiomProver和人類采用不同數學思路解出來的問題。

之所以這么分，在于AI與人類對「難度」感知并不一致。

團隊指出，以后更理想的工作流大概是：

人主要負責提供靈感的想法，而機器負責快速自洽檢查與形式化落地，甚至推動數學研究中的新抽象選擇。

人類覺得簡單，AI直接「懷疑人生」

但在Putnam競賽中，最「好下手」的往往是微積分題。

回想Mathlib庫（ Lean語言的數學庫，相當于給AI用的「數學字典」）的早期，隨便一本分析教材第一章里的簡單概念，都要花很長時間才能定義清楚。

而在Putnam2025里，這類題通常出現在每個部分的第二題。

以A2題為例。

這道題如果給人看，我們只需要附上一張函數圖像，你的眼睛會瞬間捕捉到曲線的走勢，非常直觀。

但是這在系統那里，你必須把這些線條、趨勢、拐點，統統翻譯成嚴格的數學語言。

人類要是逐行去讀Lean代碼，那就更像是在「坐牢」。

B2也是同樣的故事。

對人類來說一個很簡單的「正性引理」，在Lean里要寫60多行。

A2的引理h_nonpos_on_Icc和B2的引理psi_support_pos，成了各自證明里最難啃、最費篇幅的「釘子戶」。

這就是形式化的代價。

組合構造：友善的「野獸」

假如你正在下午茶時間的黑板邊聊天，朋友給你展示了一個精妙的組合構造，你卡殼半天，他只說了句：「先這樣，再那樣，把這個切開……」

然后你恍然大悟：怎么就變得這么簡單了？

這種感覺很震撼，問題仿佛一瞬間就溶解了。

但一旦你試圖把這種直覺「釘死」成一個完全形式化的證明，尤其是在證明助手里，事情就會出奇地棘手。

拿A5題來說。

Axiom團隊和AxiomProver都想到了同一個很自然的思路：

對一個排列里最大（或最小）的元素做歸納，把剩下的切成兩段，然后據此推理。

用人類語言來講，這種論證可能兩三段就寫完了，但在Lean的世界里并非這樣簡單。

每一個小角落的特殊情況、每一處記賬式的繁瑣細節，都必須被明確寫出來，沒有任何模糊空間。

當然，也不能使用人類最愛的「省略號」。

于是結果就令人咋舌：這份Lean形式化代碼長達2054行，生成耗時518分鐘！

這并非要吐槽Lean，而是從「人類顯而易見的證明」走到「這是機器校驗過的證明」，你所必須繳納的稅。

AI神來之筆，人類沒想到的

AI有望破解組合數學，幾何引擎并非必需

一直以來，大家都覺得組合題是AI的軟肋。

事實上，這類題目「臭名昭著」到很多工程團隊直接選擇放棄。

看看近幾年的IMO，最難的硬骨頭幾乎都是組合題。IMO 2025唯一沒做出來的題，以及IMO 2024的兩道題，全是組合。

所以，當Axiom團隊看到Putnam的A3是一道組合博弈論，B1是一道歐式幾何時，心里的預期其實是極低的。

畢竟，AxiomProver目前連一個完整的幾何引擎都沒有。

然而，奇跡發生了。

系統自主解出了A3和B1。那一刻，Axiom辦公室里直接有人尖叫了起來。他們根本沒想到它現在就夠解開這兩道題！

Axiom團隊賽后分析，這并不意味著幾何或博弈論變容易了，而是說明他們之前的悲觀判斷有點過于草率了。

這些例子說明，這道「門檻」比他們之前判斷的更微妙、更有層次。

A3的解決的確有點運氣成分。

在這道題中，「后手玩家」有一個非常干凈的必勝策略，一旦看破，只需要機械執行，不需要去探索復雜的博弈樹。這種「少狀態、無分支」的邏輯，恰好是Lean最擅長的。

B1題可能更有趣。

問題B1的概要

題面涉及「外心」這個純幾何概念。系統給出的解法風格非常幾何，但當Axiom團隊的數學家讀的時候，如果沒有圖，根本跟不上。

這就有點諷刺了，因為機器從頭到尾也沒畫過圖。最后，人類不得不自己畫了個草圖，才弄明白機器到底干了什么。

機器似乎很滿足于純符號推理，它沒畫過一張圖就建立了一個「兩條圓恰好相交于兩個點」的事實。

而人類則強烈依賴圖像。

為了更具體地讓人感受這些機器證明如何和人類的幾何直覺對齊，這里截取了一段Lean代碼，用來建立這樣一個事實：

在某個特定構型下，兩條圓恰好相交于兩個點（這個構型里，每個圓都經過另一個圓的圓心，而且兩個圓心不同）。

而對人類讀者來說，配圖能立刻把情況講清楚。

作為對照，Axiom小組也想出了一個類似的幾何論證。

Axiom團隊對于B1的解法

這次AxiomProver意外搞定人們原本沒指望它能做出來的組合題，而且也證明了沒有幾何引擎也不一定不行。

蠻力的勝利：數學家幾乎都栽在了這個問題上

Axiom團隊坦言，這次AxiomProver系統最終解出A6，令他們非常震驚。

因為這道題幾乎把他們內部的所有人都打敗了。

他們的一位數學家認出它屬于p進算術動力系統的范疇，他知道處理p進冪級數展開必須非常小心，甚至他的大方向都是對的。

但「方向對了」和「把題徹底做完」是兩碼事。在A6這場硬仗上，機器贏了。

AxiomProver居然5小時就做完了它，而且這是12題里Token用量第二高的一題。

而且，它在處理相關冪級數的求導上用了一種特別笨拙、但確實有效的方法——人類絕對不會這么寫，但它就是能跑通。

有時候，我們不得不承認，蠻力本身也有一種不講道理、碾壓一切的優雅。

同一道題，兩條完全不同的路

A4可能是這一批里最有故事的一題，因為它完美展示了「人類的代數直覺」與「AI的幾何視角」的碰撞。

人類數學家看到這道題，本能地去找代數方法，靠符號推演。

然而在競賽中，AxiomProver展示了另一種思路：它會把人類覺得「應該代數」的東西轉成幾何，把人類想用圖講清楚的內容，變成機械化的組合核算。

在下面兩道很有代表性題：A4和B4，人類和AxiomProver解法各有特色。

A4：人類想推公式，AI先把它變成幾何

A4的設定看起來就很「代數」。

人類選手在這套題上分歧也很典型：

有人很快給出k=3的構造，于是開始懷疑答案會隨著n以某種方式增長；另一個人從小n往上堆，排除了k=2，直覺上覺得答案應該就是3。

兩人一起拼出了若干針對不同n的臨時構造，能支持「答案是3」這個猜測，但離「統一的通用構造」還有距離。

與此同時，他們隱約覺得背后可能藏著表示論的影子：這也很符合人類的經驗——當一個條件像「關系編碼」時，很容易聯想到群作用、表示、代數結構。

AxiomProver的建議簡潔到有點「反常識」：讓每個A_i 都是投影到某個單位向量v_i上的秩一投影（rank-one projection）。

驗證層面，形式化里最「重」的節點，往往集中在一件在人類眼里極其自然的事：

認真檢查一圈n個向量的構造確實滿足要求。

人們往往認為，「顯然相鄰垂直，其他不垂直，環狀閉合也沒問題」。

Lean大量篇幅被花在「把直覺變成可檢驗的陳述」上，這恰好反映了形式化的性格：它不反對直覺，它拒絕用直覺替代證明文本。

B4：人類用一張圖講完，AI直出1061行代碼

在B4中，思路是構造一個從特殊對角線（第一條非零對角線）到取值為1的條目的單射。

人類選手盯著圖看一會兒，函數怎么定義就很清楚了；也能看出來它為什么成立，圖自己就把話說完了。

題在于Lean不會「看圖」。

AxiomProver直接產出了1061行Lean代碼，把行列的組合性質一條條磨到結論出來。

它能在缺乏圖像溝通的情況下，用耐心把組合性質逐格展開，把證明變成可驗證的流水線。

奇點臨近，GPT-5.2攻克難題

不僅如此，就連菲爾茲獎得主陶哲軒認為，AI已經取得了重要里程碑。

這兩天，波蘭數學家Bartosz Naskr?cki在X上發的帖把這把火點得更旺了。

他直言，GPT-5.2 Pro在數學上的表現強得離譜：面對非瑣碎問題，很難找到真正能讓AI卡死的點。

即使是高難題，一到兩小時的來回交互，模型就能把答案推出來。

最要命的是，他還用半開玩笑的方式表達震撼：

要么OpenAI 背后有一支「全天候的小精靈與頂尖數學家團隊」在實時代打，要么模型已經具備非常扎實的能力。

甚至，讓人產生「奇點將近」的直覺。

這次Putnam 2025競賽的成績，對于AxiomProver團隊來說是一次重要的勝利。

他們在博客最后總結道，「看著系統實時硬啃競賽數學，確實有種說不出的爽感：即使它經常用一些我們根本想不到的方式。」

這也引出了一個深層問題：到底是什么讓一道數學題對機器來說「難」？

顯然，人類覺得難的，和機器覺得難的并不是一回事。

人類怕繁瑣的枚舉，怕沒有靈感（巧妙構造）就卡死的死胡同。但對機器而言，什么才是真正的障礙？目前還是一個黑盒。

但正因為雙方擅長和卡殼的點不一樣，「人機協作」才顯得如此合理。

而Axiom正在構建這樣一個世界：人類直覺由機器驗證來「落地」，而機器驗證反過來激發人類直覺。

這就好比做咖啡：機器負責磨豆子，人類負責品咖啡。

在Axiom看來，我們不需要去硬攻數學研究每一個問題。

正如Grothendieck所說的「漲潮的海」——我們抬高水位，直到問題被那些堅硬的陸地慢慢包圍，最終自然溶解。

雖然目前人類還未完全到達那一步，但奇點已經臨近。

AxiomProver在Putnam 2025競賽中取得滿分，以及GPT-5.2 Pro在數學上的驚艷表現，都在提醒我們：

這個未來更近了。

參考資料：

https://x.com/apples_jimmy/status/2009742681166229687

https://x.com/axiommathai/status/2009682955804045370

https://x.com/nasqret/status/2008672809094905970

https://jmlr.org/papers/v24/22-125.html

文章來源：新智元。