新智元报道
【新智元导读】
在人类极难拿满分的Putnam数学竞赛中，AI首次实现12题全对、总分120分。由24岁华人女学者Carina Hong领衔开发的AxiomProver系统达成这一里程碑。陶哲轩等顶尖数学家认为，AI已在形式化数学与难题求解上取得关键突破。GPT-5.2 Pro亦展现出超常数学能力，强化了“奇点临近”的共识。
「本科最难数赛」夺下满分，全网震撼
AxiomProver在2025年Putnam数学竞赛中斩获满分——12道题全部答对。该赛事是北美本科生最高水平数学竞赛，需在6小时内完成12道高难度证明题。Putnam总分120分，人类选手极少接近满分，历年仅前五名（Putnam Fellows）有望达到110分以上。
AxiomMathAI官方博客已公开全部Lean形式化证明，并将题目按AI与人类认知差异分为三类：
- 人类直觉简单、但形式化极为繁琐的问题；
- AI出人意料攻克、人类此前未预期可解的问题；
- AxiomProver与人类采用不同数学路径解决的问题。
团队指出：未来理想的研究范式将是“人类提供灵感，机器负责形式化验证与落地”，甚至辅助抽象概念的生成与选择。
人类觉得简单，AI直接「怀疑人生」
Putnam竞赛中看似最易入手的微积分题（如A2、B2），反而成为形式化最大挑战。
以A2题为例：人类仅需观察函数图像即可把握趋势；但Lean系统要求将所有视觉直觉转化为严格数学语言——包括定义域划分、单调性、拐点、边界行为等，每一步均须显式声明。
类似地，B2题中一个简单正性引理（psi_support_pos），在Lean中需60余行代码才得以严谨表达。这揭示了形式化数学的核心代价：它不拒绝直觉，但拒绝用直觉替代可验证陈述。
组合构造：友善的「野兽」
组合题常被视作AI短板，近年IMO最难题目多属此类。但AxiomProver在Putnam 2025中成功破解A5题——一道典型的归纳构造型组合问题。
人类两三段文字即可讲清的思路，在Lean中扩展为2054行代码，耗时518分钟生成。每个边界情形、每处隐含假设、每个“显然成立”的步骤，都必须展开为机器可校验的原子操作——这是从“人类可理解”走向“机器可验证”必须缴纳的形式化税。
AI神来之笔，人类没想到的
AI有望破解组合数学，几何引擎并非必需
A3（组合博弈）与B1（欧氏几何）原被Axiom团队视为高风险题目——因系统尚未集成完整几何引擎。结果AxiomProver不仅解出，且策略出人意料：
- A3中，AI发现后手玩家存在简洁必胜策略，规避复杂博弈树搜索，契合Lean对确定性逻辑的高效验证优势；
- B1中，AI全程未绘图，却通过纯符号推理确立“两圆恰交于两点”等关键几何事实，反令人类数学家需补画草图才能理解其推导逻辑。
这表明：AI与人类的“难度感知”存在本质错位——所谓“难点”，实为表征方式与验证机制的结构性差异。
蛮力的胜利：数学家几乎都栽在了这个问题上
A6题属p进算术动力系统范畴，涉及高度敏感的幂级数展开。团队多位数学家识别出方向，却未能完成全部推导；而AxiomProver在5小时内完成证明，且Token消耗量居12题第二高位。
其方法看似“笨拙”——例如对幂级数逐项求导并暴力验证收敛性——但完全有效。这印证了一种现实：对机器而言，“正确性”比“优雅性”更根本；蛮力本身即是一种确定性的力量。
同一道题，两条完全不同的路
A4：人类想推公式，AI先把它变成几何
A4题天然激发代数直觉（如群表示、向量空间结构）。人类尝试构造k=3解并推测普适规律；AxiomProver则提出几何化方案：将每个A_i设为单位向量v_i上的秩一投影。验证焦点落在“构造是否满足题设条件”——这恰恰是形式化最擅长的机械核查环节。
Lean大量篇幅用于将“显然成立”的直觉（如相邻垂直、环状闭合）转译为可检验命题——凸显形式化本质：它不否定直觉，但坚持用语言将其锚定为文本证据。
B4：人类用一张图讲完，AI直出1061行代码
B4要求构造特殊对角线到取值为1位置的单射。人类观图即得函数定义及正确性；AI无法读图，转而将矩阵结构拆解为1061行Lean代码，逐格枚举行列关系、边界条件与映射唯一性。
这种“无图推演”能力，使AI能在缺乏视觉中介的条件下，将组合结构转化为可验证流水线——不是模仿人类思维，而是开辟独立证明路径。
奇点临近，GPT-5.2攻克难题
菲尔兹奖得主陶哲轩指出，当前AI已在数学推理上迈过关键门槛。波兰数学家Bartosz Naskręcki测试GPT-5.2 Pro后表示：面对非琐碎数学问题，AI极少卡死；多数高难度题在一至两小时交互内即可给出完整解答。
他半开玩笑称：“要么OpenAI背后有全天候数学家团队实时托底，要么模型已具备扎实的自主推理能力。” 这种突破感催生强烈共识：AGI临界点正在加速逼近。
AxiomProver团队总结道：“看着系统实时硬啃竞赛数学，确实有种说不出的爽感——尤其当它用我们根本想不到的方式解决问题。”
这引出深层命题：数学题对机器的“难”，不再等同于对人类的“难”。人类畏惧灵感缺失与枚举爆炸；机器的瓶颈尚不明晰，但其与人类的互补性已成必然路径——
人类负责提出猜想与直觉框架，机器负责形式化验证与边界探索；二者共同抬高数学研究的“水位”，让难题随基础稳固而自然消解（Grothendieck式“涨潮的海”）。
AxiomProver的Putnam满分与GPT-5.2 Pro的持续突破共同指向一个结论：通用人工智能在数学领域的奇点，已非远景，而是进行时。