上海的七月热浪滚滚。第67届国际数学奥林匹克刚刚落下帷幕，中国队以232分的高分摘得桂冠，三名中国少年更是全员拿下42分的满分。然而，现场掌声尚未散去，GitHub上却悄然浮现出另一份令人瞩目的成绩单。前Google工程师Deedy Das发起了一场AI横评：七个前沿大模型全自主挑战IMO 2026的全部6道题目。
结果令人咋舌：Claude Fable 5狂揽42分满分，耗时仅2.5小时，成本51美元；GPT-5.6 Sol的xhigh版本也拿下满分，用时3.8小时，成本仅20美元；Kimi K3紧随其后，耗时17.4小时，花费31美元。再加上独立交卷的AxiomProver，四方势力全部登顶满分。作为参照，过去七届IMO共有4347名人类选手参赛，仅有30人拿到满分，比例仅为0.69%。AI的表现呈现出断层式的碾压。
满分与第四名（28分）之间横亘着14分的鸿沟，而三个满分模型的解题路径也截然不同。Claude Fable 5打得干净利落，9轮对话中6轮有效输出，全程输出70万token，单趟最长耗时73分钟（P3题）。GPT-5.6 Sol则显得有些坎坷，P2题上耗时106分钟跑4轮，中途还因网络故障中断两次，但其算力控制堪称恐怖，总输出仅23万token，是三个满分模型中最省的。Kimi K3则像一头不知疲倦的巨兽，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)。反复操作直到无法继续。证明：过程一定会终止，最终恰好剩一个大于1的数M；以及M的值不依赖于操作顺序。为便于理解，我们先做一个微缩实验：黑板只有12和18。12等于2的平方乘以3，18等于2乘以3的平方。第一步：gcd(12,18)等于6，lcm(12,18)除以6等于6，黑板变成[6,6]。第二步：gcd(6,6)等于6，lcm(6,6)除以6等于1，黑板变成[6,1]。只剩一个大于1的数，游戏终止，M等于6。无论操作顺序如何打乱，M永远是6。为什么？答案藏在素因子里。对每个素数p，取所有数被p整除次数的最大公约数，再把这些素数幂乘起来——这个值从第一步到最后一步都一直不变。
Claude Fable 5直接生造了一个每步必定缩水的计数器。它定义了一个量Phi等于T加N。T是黑板上所有数的素因子个数之和（重复计），N是大于1的数的个数。比如黑板[12,18]，12的素因子是2、2、3共3个，18的是2、3、3共3个，T等于6，N等于2，Phi等于8。然后它证明了：每执行一步操作，Phi至少减少1。分两种情况——如果gcd(m,n)大于1，素因子总数T会减少；如果gcd(m,n)等于1，T不变但大于1的数少了一个，N减1。Phi是正整数，每步至少减1，过程必须在有限步内终止。单一计数器，一刀斩断。
GPT-5.6 Sol则采取追踪乘积、字典序降维的策略。Sol看的则是两个量：P等于所有数的乘积，K等于大于1的数的个数。每步操作，如果gcd(m,n)等于d大于1，新的两个数的乘积是mn除以d，比原来小，全局乘积P严格变小。如果d等于1，P不变，但K减少1。(P,K)这个二元组在字典序下严格递减：要么P变小，要么P不变但K变小。正整数的字典序不可能无限递减，因此终止。两条截然不同的路径攻克了同一个问题的第一部分。到了第二部分，三个模型殊途同归：都证明了对每个素数p，黑板上所有数被p整除次数的最大公约数在操作中不变。最终公式也是一模一样。回到例子验算：12和18。对p等于2，v2(12)等于2，v2(18)等于1，gcd等于1，贡献2的1次方。对p等于3，v3(12)等于1，v3(18)等于2，gcd等于1，贡献3的1次方。M等于2乘以3等于6，和手算分毫不差。
P6题是Day 2的压轴，要求证明递推序列最终具有周期性。去年IMO 2025全球仅有6人解出。Claude Fable 5：26分钟，两轮，满分。GPT-5.6 Sol：60分钟，两轮，满分。Kimi K3：381分钟，四轮，满分。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行严格证明的模型，手里握着的不只是解数学题的能力。它真正掌控的是长链条逻辑推导，每一步不能跳、不能错、不能含糊。合同条款有没有漏洞、保险理赔条件满不满足、税务方案合不合规，剥开表象都是同一类问题：答案不能差不多对。过去这种逐条核验只有专业人士能做，按小时计费。如今，随着这个能力铺进消费级产品，遇到棘手问题，只需打开手机就行了。