24岁华人女学霸打造的AI在2025普特南数学竞赛中拿下满分，12道题全对。这一成绩不仅打破了人类对AI数学能力的认知，更通过公开的Lean证明展示了机器独特的解题视角与逻辑，标志着AI在解决复杂数学问题上的重大突破。
智能速览
华人AI在普特南数学竞赛中取得12题全对满分成绩。
公开Lean自主证明代码，揭示机器与人类解题思路差异。
AI意外攻克被认为困难的组合博弈与几何题目。
机器利用“蛮力”解决了连数学家都棘手的算术动力系统问题。
陶哲轩等数学家看好AI解决千禧难题的潜力。
精华内容
普特南竞赛不仅是一场智力较量，更是观察AI与人类思维差异的绝佳窗口。
难易感知的差异
人类直觉与机器对“难度”的感知截然不同。在普特南竞赛中，微积分题对人类而言往往只需一张函数图像即可直观理解走势。然而，机器必须将这些线条、趋势严格翻译成数学语言。例如A2题的引理和B2题的“正性引理”，在人类眼中显而易见，但在Lean形式化系统中却需要60多行代码来定义，成为证明中最费篇幅的部分。
意料之外的突破
组合数学和几何常被视为AI的软肋，但此次表现却出人意料。AxiomProver虽无几何引擎，却自主解出了组合博弈题A3和几何题B1。在B1题中，机器全程未绘图，仅通过纯符号推理建立了“两条圆恰好相交于两个点”的事实。这种完全不依赖图像、仅靠符号逻辑的解题方式，展示了与人类依赖几何直觉截然不同的路径。
蛮力与视角碰撞
面对极具挑战的A6题（p进算术动力系统），AI展现了一种不讲道理的“蛮力”优雅。机器用时5小时，采用人类看来笨拙却有效的幂级数求导方法完成了证明，解决了连内部数学家都感到棘手的问题。而在A4题中，人类倾向代数推演，AI却将其转化为几何视角，通过构造秩一投影验证，体现了思维方式的根本差异。
AxiomProver的满分不仅是技术的胜利，更预示着人机协作数学研究的未来。人类负责灵感直觉，机器负责形式化验证与“涨潮”，这种协作模式将加速攻克千禧难题等数学高峰。随着GPT-5.2等模型在数学领域的突破，AI解决复杂数学问题的奇点似乎已近在咫尺。
