华人女学霸公开：12道难题，AI全都答对新智元

在人类满分都罕见的普特南数赛上，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多行。