全球三大AI包揽IMO满分，击败99%人类

第67届国际数学奥林匹克正式落幕中国队以232分斩获桂冠。三名少年拿下42分满分。现场掌声还未散尽GitHub上悄然浮现了另一份亮眼的成绩单。前Google工程师Deedy Das甩出一场AI横评7个前沿大模型全自主单挑IMO 2026全部6道题。Claude Fable 5狂揽42分满分。耗时仅仅2.5小时烧掉51美元。GPT-5.6 Sol的xhigh版本同样满分。用时3.8小时成本更是压到了极低的20美元。KimiK3紧随其后拿下满分。历经17.4小时鏖战花费31美元。再算上独立交卷的AxiomProver整整四方势力全部登顶满分。作为参照过去七年IMO4347名人类选手参赛只有30人拿过满分——比例0.69%。成绩断层式碾压从结果来看不仅满分42和第四名28之间横着14分的鸿沟而且三个满分模型登顶的姿势截然不同。Claude Fable 5打得干净利落。9轮对话6轮有效输出单趟最长73分钟P3全程输出70万token。GPT-5.6 Sol显得有些坎坷。在P2上磨了106分钟跑4轮中途被网络故障打断两次。但算力控制堪称恐怖——总输出只有23万token三个满分里最省。KimiK3像一头不知疲倦的巨兽。2.8万亿参数的MoE模型一口气喷涌出154万token是Sol的6.5倍。光P3一道题就发起6次冲锋鏖战491分钟。数学直觉的正面交锋P1是全场最温和的开胃菜所有模型几分钟搞定人类选手也几乎无一失手。题目大意是黑板上写着2026个大于1的正整数。每一步选两个数m和n擦掉换上gcd(m,n)和lcm(m,n)/gcd(m,n)。反复操作直到无法继续。证明(a) 过程一定会终止最终恰好剩一个大于1的数M(b) M的值不依赖于操作顺序。为了便于理解这道题我们先做一个微缩实验。黑板上只有12和18。12 2² × 318 2 × 3²。第一步gcd(12,18) 6lcm(12,18)/6 6黑板变成[6, 6]。第二步gcd(6,6) 6lcm(6,6)/6 1黑板变成[6, 1]。只剩一个大于1的数游戏终止。M 6。不管你怎么打乱操作顺序M永远是6。为什么答案藏在素因子里。对每个素数p取所有数被p整除次数的最大公约数再把这些素数幂乘起来——这个值从第一步到最后一步都一直不变。Claude Fable 5直接生造了一个每步必定缩水的计数器。对于这道题Fable 5定义了一个量Φ T N。T是黑板上所有数的素因子个数之和重复计N是大于1的数的个数。比如黑板[12, 18]12的素因子是2、2、3共3个18的是2、3、3共3个T 6N 2Φ 8。然后它证明了每执行一步操作Φ至少减少1。分两种情况——如果gcd(m,n) 1素因子总数T会减少如果gcd(m,n) 1T不变但大于1的数少了一个N减1。Φ是正整数每步至少减1过程必须在有限步内终止。单一计数器一刀斩断。GPT-5.6 Sol追踪乘积字典序降维。Sol看的则是两个量P 所有数的乘积K 大于1的数的个数。每步操作如果gcd(m,n) d 1新的两个数的乘积是mn/d比原来小全局乘积P严格变小。如果d 1P不变但K减少1。(P, K)这个二元组在字典序下严格递减要么P变小要么P不变但K变小。正整数的字典序不可能无限递减。终止。两条截然不同的路径攻克了同一个问题的(a)部分。到了(b)部分三个模型殊途同归都证明了对每个素数p黑板上所有数被p整除次数的最大公约数在操作中不变。最终公式也是一模一样——回到例子验算12和18。对p2v₂(12) 2v₂(18) 1gcd 1贡献2¹。对p3v₃(12) 1v₃(18) 2gcd 1贡献3¹。M 2 × 3 6和手算分毫不差。全场最廉价的白卷P6这道数论题是Day 2的压轴它要求证明递推序列最终具有周期性。去年IMO 2025全球只有6个人类解出P6。Claude Fable 526分钟两轮满分。GPT-5.6 Sol60分钟两轮满分。KimiK3381分钟四轮满分。Grok 4.5在P6上只挤出7053个token全场垫底。提交文件里赫然写着一句Full proof: (Not yet complete.)$0.18全场最廉价的白卷。Grok的毛病不止于此。整个测试中它反复陷入一种诡异的幻觉信誓旦旦地声称「证明已经写入文件」后台却连写入工具都没碰一下。这不是数学能力问题是agent能力问题。模型知道应该写文件也声称自己写了但在工具调用层面没有动手。三年三级跳硅基大脑的恐怖进化2024年DeepMind的AlphaProof首次在IMO级别摸到银牌门槛。2025年OpenAI和DeepMind同时出手。OpenAI未公开模型解5题拿下35分金牌Gemini Deep Think达到同等段位。2026年三个通用大模型直接拿下满分。这次不仅没有经过任何专项数学训练而且所有人都能用上。甚至还有一个是开源的。写下机器战书的人整场测试的起点是一家叫Axiom Math的公司。他们将IMO 2026的全部6道考题逐字逐句翻译成了机器能够理解的Lean 4形式化题面。有了这套机器可读的题目AI才能直接输出Lean证明、由编译器自动判分不再需要人类评委阅卷。拿到题面后Deedy Das迅速搭建起全自动化的测试框架。各大模型在赛道上各自狂奔跑完了全部6道关卡。AxiomProver也独立斩获了满分。值得一提的是Axiom Math的创始人洪乐彤年仅25岁。她出生于广州仅用三年便横扫MIT数学与物理双学位更是Morgan Prize的得主。去年底她一手打造的AxiomProver拿下了Putnam数学竞赛的满分。这是该项赛事98年历史上的第6个满分奇迹。今年3月这家公司完成了2亿美元A轮融资。估值直冲16亿美元。普通人的生活将被如何重构能写4229行严格证明的模型手里握着的不只是解数学题的能力。它真正掌控的是长链条逻辑推导每一步不能跳、不能错、不能含糊。合同条款有没有漏洞、保险理赔条件满不满足、税务方案合不合规剥开表象都是同一类问题答案不能「差不多对」。过去这种逐条核验只有专业人士能做按小时计费。如今随着这个能力铺进消费级产品遇到棘手问题只需打开手机就行了。原文链接刚刚全球三大AI包揽IMO满分击败99%人类-36氪