文 | 硅谷 101

最近，2025 年国际数学奥林匹克（IMO）在澳大利亚落幕的两天内，AI 界因 "IMO 金牌认证 "，开展了一场人才与技术话语权的双重争夺战。

OpenAI 抢先宣布其保密推理模型以 35 分达到金牌线，DeepMind 两天后也亮出 IMO 官方认证的同等成绩单。这标志着 AI 首次在 IMO 中比肩顶尖学生，实现从 2024 年银牌到 2025 年双金牌的数学推理能力跃升。

伴随技术进展而来的，是行业竞争 " 好戏 "：当 Demis Hassabis 公开谴责 OpenAI 提前泄露成绩时，媒体曝出 DeepMind 金牌团队三名核心研究员已被 Meta 挖角。

AI 数学能力的进步速度令人惊叹。但 IMO 金牌究竟意味着什么？这是数学界的 AlphaGo 时刻吗？AI 将会成为数学研究中值得信赖的合作者，还是沦为市场逻辑下的技术产品，消解数学的真正意义？

本篇文章，我们邀请了 IMO 金牌得主，以亲历者的角度来聊聊两大 AI 的解题逻辑和数学水平，并透视竞赛背后的技术突破与数学的未来。

一觉醒来，我以为我穿越回高中了：朋友圈竟然有人提起 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 就评价说：非常了不起。

将解答 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 发布了自己的模型生成出来的解答，这个解答就完全是自然语言了，就没有一些代码之类的。但是相比于去年使用的那一套系统就是，它可能最终输出也是自然语言的，但是它需要先把这些东西翻译成一个逻辑语言，然后进行一些形式化的证明之后，再输出回来。

可能过往数学家会把用电脑辅助数学跟形式化方法等同起来，但是经过了这些语言模型的发展，以及它们证明了自己能够显示出一定的数学能力之后，他们可能会改变这个想法。

为了让大家直观地对比 AI 和人类选手的解答，我们邀请了前 IMO 中国国家队成员胡苏麟，为我们分享他对 AI 回答的感受。

他告诉我们，AI 在作答的五道题中解答思路清晰、逻辑链条完整，获得满分是实至名归的。

但在具体题目里对比两个 AI 的回答，还是能发现一些有意思的情况。就比如第二题，一道平面几何题。

胡苏麟

2019 年 IMO 金牌得主：

平面几何题对于 AI 来说，算是最容易做的题型之一了。在这里，两个 AI 也给出了不一样的做法。DeepMind 的做法是一个更加几何的，更加自然的做法，我觉得也是更接近于正常人类选手能想到的做法。相比起来，OpenAI 的方法就非常暴力，因为它直接使用了解析几何的手段。用解析几何的办法，直接把这道几何题转化成了一道代数题，并且在它的解答过程中出现了巨量的计算。不过通常来说，人类选手通常不会在考场上做那么大量的计算。所以这个方法可能对 AI 来说，实行起来比人类选手要容易。

他还提到，两个 AI 作答时的语言风格也不同于人类选手。

两个 AI 的一个共同点就是：解答过程中会不断引入新符号，来定义一些概念或者公式。这个选项在我上大学的高等数学的学习中比较经常出现，但在我以前的竞赛生涯中不太经常出现。原因是高中的竞赛题没有那么复杂，如果在解答过程中不断引入新的符号，反而会增加我们理解解答过程以及解答思路的难度。

两个 AI 的语言风格也有非常明显的区别。比如说 OpenAI 在它的解答过程中会经常出现一些人性化的描述词，比如 "XXX so far good" 或者 "XXX 我们完成了这一步 " 或者 "nice" 之类的词汇。在一些方面也会适当省略一些细节，比如它会说 " 很容易验证 " 或者 " 根据某某公式可以很容易检查下面这些东西是对的。"

所以总的来说，它给我的感觉像是一个在课堂上给学生讲题的老师，所以它会经常使用一些口语化的语言来鼓励学生，循循善诱，比如它会说 " 我们已经完成了关键的一步，非常棒 "，又比如 " 我们已经完成了这个结论，真是一个漂亮的结论 " 之类的话，来强调关键的步骤。

而相比之下，DeepMind 所用的语言则更加书面化，像是在阅读一篇数学论文。

虽然和之前相比，大模型在 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 或类似的系统提供给你的，可以说是一个非常强大的工具，它可以帮助数学家和科学家们做一件大事：试图理解这个世界。