文 | 硅谷 101

最近，2025 年國際數學奧林匹克（IMO）在澳大利亞落幕的兩天內，AI 界因 "IMO 金牌認證 "，開展了一場人才與技術話語權的雙重爭奪戰。

OpenAI 搶先宣布其保密推理模型以 35 分達到金牌線，DeepMind 兩天后也亮出 IMO 官方認證的同等成績單。這標志著 AI 首次在 IMO 中比肩頂尖學生，實現從 2024 年銀牌到 2025 年雙金牌的數學推理能力躍升。

伴隨技術進展而來的，是行業競爭 " 好戲 "：當 Demis Hassabis 公開譴責 OpenAI 提前泄露成績時，媒體曝出 DeepMind 金牌團隊三名核心研究員已被 Meta 挖角。

AI 數學能力的進步速度令人驚嘆。但 IMO 金牌究竟意味著什么？這是數學界的 AlphaGo 時刻嗎？AI 將會成為數學研究中值得信賴的合作者，還是淪為市場邏輯下的技術產品，消解數學的真正意義？

本篇文章，我們邀請了 IMO 金牌得主，以親歷者的角度來聊聊兩大 AI 的解題邏輯和數學水平，并透視競賽背后的技術突破與數學的未來。

01 前后獲得 IMO 金牌，DeepMind 與 OpenAI 之戰

一覺醒來，我以為我穿越回高中了：朋友圈竟然有人提起 IMO（國際數學奧林匹克競賽，International Mathematical Olympiad，面向高中生的國際性數學競賽）。記得當年還是萬里挑一的學霸才會去挑戰這個比賽，最近卻被 AI 拿下了：OpenAI 和谷歌 DeepMind 前后宣布他們的模型達到了 IMO 金牌的標準。

這個 " 前后 " 雖然只差兩天，但卻充滿了戲劇性：今年的 IMO 是 7 月 20 日周日在澳大利亞閉幕，而 OpenAI 在周五，也就是 7 月 18 日晚上，就早早宣布了這個消息。

研究員 Alexander Wei 在 X 上說：OpenAI 最新的實驗性推理大模型，實現了人工智能領域長期以來的一項重大挑戰，在 IMO 競賽的 6 道題目中解出了 5 道，并且最終獲得了 35 分。IMO 的滿分是 42 分，而 35 分恰好就達到了金牌的門檻。

兩天之后，DeepMind 也下場宣布：Gemini Deep Think 的進階版本模型也達到了這一成就。DeepMind 的模型在整個過程中完全使用自然語言操作，最后同樣獲得了 35 分的成績，并且 IMO 官方組委會也證明了這一成績。

IMO 主席 Gregor Dolinar 說：DeepMind 的解題在許多方面都令人驚嘆，閱卷官認為這些解答清晰、嚴謹，而且大多數都很容易理解。

這個組委會親自背書的待遇，卻沒有給到 OpenAI。Demis Hassabis 甚至特意下場，在 X 上表示：我們之所以沒有周五公布，是因為我們尊重 IMO 組委會最初的請求。所有 AI 實驗室都應該在官方成績經過獨立專家驗證，并且參賽學生已經獲得應有的表彰之后，才公開各自的結果。

他還說：我們的模型是第一個獲得官方 " 金牌水平 " 評級的 AI 系統——這簡直就差點 OpenAI 的名了。OpenAI 之前的歡呼好像就沒那么名正言順了。

但更戲劇性的是，隔天媒體就爆出，DeepMind 這一金牌模型背后的研究團隊中，有三名研究員已經被 Meta 挖走了。在此之前的六個月內，DeepMind 已經有 20 名員工被挖去了微軟。

看來這場頂尖實驗室之間的斗爭，還在愈演愈烈。在吃瓜的同時，我們還是回到 IMO 競賽這個話題上：AI 達到金牌水平，到底意味著什么？

首先要知道的是，這還遠遠說不上是數學領域的 AlphaGo 時刻。當年 AlphaGo 擊敗了世界圍棋冠軍李世石，震驚全球，最核心的原因是圍棋被認為是人類智慧最難被機器超越的領域之一。

2022 年 DeepMind 的 AlphaFold 準確預測蛋白質結構，也被稱為是生物學的 AlphaGo 時刻，我們硅谷 101 在去年的文章《AI" 入侵 " 生物醫療史》里詳細解讀了它的重要性。

但是這次，有 72 位高中生的成績也達到了金牌標準，其中 5 位獲得了 42 分滿分的成績，也就是完美地解答了 6 道題，但兩個 AI 模型都只做出來了 5 道。所以要說 AI 在數學能力上已經勝過人類，還為時過早。

但即使沒有到 AlphaGo 的標準，IMO 金牌的結果也足夠證明當下大模型優秀的數學能力了。紐約大學的計算機教授 Gary Marcus 和 Ernest Davis 就評價說：非常了不起。

02 作為能力標準的 IMO，證明了 AI 的數學推理能力

將解答 IMO 題目作為評估 AI 推理能力的標準，其實早有先例。

比如去年，DeepMind 發布了兩個專為數學設計的模型：AlphaGeometry 和 AlphaProof。在 IMO 的六道題中，它們解出了四道，成為第一批達到銀牌標準的 AI 系統。

圖源：Google DeepMind

不過，這兩個模型當時并不是用自然語言來解題，而是結合了 " 形式化證明 " 方法。簡單來說，形式化證明（Formal Proof）就是把數學問題轉成機器能 " 看懂 " 的語言，再由 AI 用這種形式化語言一步步寫出邏輯嚴謹、可驗證的解答。

而這套語言的寫作工具，就叫做 Lean（一種現代的定理證明助手和函數式編程語言，由微軟研究院開發），類似編程語言。

為了讓 AI 解題，研究者得先把自然語言題目 " 翻譯 " 成 Lean，讓 AI 去處理，再轉回人類可讀的答案。整個過程耗時長達三天——遠超 IMO 給高中生兩天、共 9 小時的比賽限制。

但這一次，DeepMind 最新的 Gemini Deep Think 模型在完全自然語言輸入輸出的條件下，達到了 IMO 的金牌標準。也就是說，AI 直接從自然語言讀題、用自然語言作答——沒有再依賴 Lean 或其他形式化工具。這背后的意義很重要。

一直以來，很多人都認為語言模型不具備真正的推理能力。比如問它："strawberry 這個詞里有幾個 r？"，它可能就會開始 " 內耗 "，反復計算還出錯。因為自然語言里沒有明確的邏輯結構，推理過程也就不穩定。這也是為什么過去像 AlphaProof 那樣的模型，需要把自然語言轉成 Lean，繞開語言的不確定性。

但現在，DeepMind 證明了：語言模型本身，也可以完成高難度數學推理。雖然 DeepMind 和 OpenAI 都沒有公開模型的具體訓練過程，但和一年前相比，這確實是一次重大進展。

李元杉

圣母大學邏輯學博士生 :

現在 AI 大家都知道是根據很多技術、從很多數據當中學習出來的一些參數，這樣的一個結果，就不是說，我們預先給定了很多邏輯規則，然后它去執行。同理，在數學上，最早期的用電腦來做數學的人會認為，把數學全部都形式化，然后運用這些規則，是解決數學問題的方法。但是現在，我們更多地看到這些公司會想辦法把兩者結合起來，甚至是直接使用語言模型去輸出自然語言的數學，而完全不借助于形式化系統。

此前以 Gary Marcus 為代表的 AI 學者一直認為，語言模型無法獨立完成真正的數學推理。在他的設想中，AI 模型必須依托像 Lean 這樣的形式化語言，輸出可以機器驗證的邏輯結構，最后再人工轉換成自然語言。也就是說，只有像 AlphaProof 這樣的 " 混合模型 " 才有可能達到數學研究的標準。

因此，Gemini Deep Think 的成功，無疑在一定程度上挑戰了 Gary Marcus 的觀點。

圣母大學邏輯學博士生：

你可以看到 DeepMind 發布了自己的模型生成出來的解答，這個解答就完全是自然語言了，就沒有一些代碼之類的。但是相比于去年使用的那一套系統就是，它可能最終輸出也是自然語言的，但是它需要先把這些東西翻譯成一個邏輯語言，然后進行一些形式化的證明之后，再輸出回來。

可能過往數學家會把用電腦輔助數學跟形式化方法等同起來，但是經過了這些語言模型的發展，以及它們證明了自己能夠顯示出一定的數學能力之后，他們可能會改變這個想法。

03 前 IMO 金牌得主點評，OpenAI 與 DeepMind 解題差異

為了讓大家直觀地對比 AI 和人類選手的解答，我們邀請了前 IMO 中國國家隊成員胡蘇麟，為我們分享他對 AI 回答的感受。

他告訴我們，AI 在作答的五道題中解答思路清晰、邏輯鏈條完整，獲得滿分是實至名歸的。

但在具體題目里對比兩個 AI 的回答，還是能發現一些有意思的情況。就比如第二題，一道平面幾何題。

胡蘇麟

2019 年 IMO 金牌得主：

平面幾何題對于 AI 來說，算是最容易做的題型之一了。在這里，兩個 AI 也給出了不一樣的做法。DeepMind 的做法是一個更加幾何的，更加自然的做法，我覺得也是更接近于正常人類選手能想到的做法。相比起來，OpenAI 的方法就非常暴力，因為它直接使用了解析幾何的手段。用解析幾何的辦法，直接把這道幾何題轉化成了一道代數題，并且在它的解答過程中出現了巨量的計算。不過通常來說，人類選手通常不會在考場上做那么大量的計算。所以這個方法可能對 AI 來說，實行起來比人類選手要容易。

他還提到，兩個 AI 作答時的語言風格也不同于人類選手。

兩個 AI 的一個共同點就是：解答過程中會不斷引入新符號，來定義一些概念或者公式。這個選項在我上大學的高等數學的學習中比較經常出現，但在我以前的競賽生涯中不太經常出現。原因是高中的競賽題沒有那么復雜，如果在解答過程中不斷引入新的符號，反而會增加我們理解解答過程以及解答思路的難度。

兩個 AI 的言風格也有非常明顯的區別。比如說 OpenAI 在它的解答過程中會經常出現一些人性化的描述詞，比如 "XXX so far good" 或者 "XXX 我們完成了這一步 " 或者 "nice" 之類的詞匯。在一些方面也會適當省略一些細節，比如它會說 " 很容易驗證 " 或者 " 根據某某公式可以很容易檢查下面這些東西是對的。"

所以總的來說，它給我的感覺像是一個在課堂上給學生講題的老師，所以它會經常使用一些口語化的語言來鼓勵學生，循循善誘，比如它會說 " 我們已經完成了關鍵的一步，非常棒 "，又比如 " 我們已經完成了這個結論，真是一個漂亮的結論 " 之類的話，來強調關鍵的步驟。

而相比之下，DeepMind 所用的語言則更加書面化，像是在閱讀一篇數學論文。

04 AI 用于數學研究的前景，學術界褒貶不一

雖然和之前相比，大模型在 IMO 競賽中的表現已經達到了質的飛躍。但我們的采訪嘉賓告訴我們，IMO 終究只是數學能力的一個側面：它是在一個限時、封閉的環境中，需要參賽者進行巧妙的思考，從而找到固定答案的一個競賽。

這不是我們在生活中買菜逛街要用的數學，也不是數學家要窮盡一生思考的目標。

李元衫

真正的數學研究，有時候目標可能更加開放，比如說，有些人可能會覺得自己做研究的目的是描述出一種現象，或者是發現一些具有規律性的結構。但是在你真正做出這些發現之前，你能發現出什么是不知道的。

所以說，相比于解決真正的開放性數學問題，可能解決競賽問題對于這些模型來說，現在是更可及了。

在 AI 不斷發展的過程中，數學學界也分裂成了兩派：有人認為，AI 在數學和推理能力上的進展，已經能夠在很大程度上幫助數學家。

比如澳籍華人數學家陶哲軒（Terence Tao，菲爾茲獎得主，被譽為 " 數學界的莫扎特 "）就說：2023 年，AI 已經能夠為職業數學家生成有啟發性的提示和有前景的思路。當它與形式化證明及驗證、搜索引擎、符號數學工具等結合使用時，2026 年的 AI 將會成為數學研究中值得信賴的合作者。

但與此同時，也有數學家對 AI 不那么信任。哥倫比亞大學的數學家 Michael Harris 就在自己的 Substack 博客中提出了對 AI 數學的批判。

他提出，數學的真正意義在于自由探索和內在洞見，而不是將其淪為市場邏輯下的技術產品。而像 Lean 這樣的計算機語言，卻將數學簡化成機器能看得懂的邏輯，讓他鐘愛的數學失去了自由創造和思辨力。

同時，他十分關注數學研究資本化的趨勢，擔心類似 Google、NSA（美國國家安全局，National Security Agency）這樣的資助者傾向于以應用價值衡量數學，而忽視其內在價值。

他批評當前關于 AI 輔助數學的討論過分關注 " 它管用嗎 "" 會帶來效益嗎 "，卻忽略了 " 對誰有益？"" 為什么需要它？" 這類值得探討的根本問題。

我們知道，李世石在被 AlphaGo 擊敗后選擇提前退役。頂尖的數學家們會因為 AI 在數學上的成就，懷疑自己研究的意義嗎？DeepMind 的 Pushmeet Kohli 在去年 AlphaProof 達到 IMO 銀牌標準后就說，他認為這會促進數學學術研究。

Pushmeet Kohli

DeepMind 科學家：

即使在圍棋的例子中，我們看到的是，當圍棋選手在比賽結束后開始分析 AlphaGo 的策略時，他們發現了很多以前沒見過的關于圍棋的新理論。而數學并不是一個游戲。AlphaProof 或類似的系統提供給你的，可以說是一個非常強大的工具，它可以幫助數學家和科學家們做一件大事：試圖理解這個世界。

你怎么看待這些不同的意見？歡迎在評論區告訴我們你的想法。