华人女学霸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

文章来源：新智元。