第 67 届国际数学奥林匹克刚刚结束，中国队以 232 分夺冠，3 名选手拿到 42 分满分。几乎同时，GitHub 上出现了另一份成绩单：在一场针对 IMO 2026 全部 6 道题的 AI 横向测试中，3 个通用大模型和 1 个独立系统拿到满分。
这场测试由前 Google 工程师 Deedy Das 公布，参与对象为 7 个前沿大模型，全部以自主方式完成 IMO 2026 题目。结果显示，Claude Fable 5、GPT-5.6 Sol 的 xhigh 版本、Kimi K3 均拿到 42 分，AxiomProver 也独立拿下满分。
三大模型与 AxiomProver 同时登顶
在已披露的成绩中，Claude Fable 5 用时 2.5 小时，成本 51 美元，得到 42 分满分。GPT-5.6 Sol xhigh 版本同样获得 42 分，用时 3.8 小时，成本 20 美元。Kimi K3 也拿到 42 分，但耗时达到 17.4 小时，花费 31 美元。
如果把独立交卷的 AxiomProver 计算在内，这次共有四方获得满分。
作为对照，过去 7 年 IMO 共计有 4347 名人类选手参赛，其中只有 30 人拿过满分，占比 0.69%。
分差明显，三种满分路径并不相同
从结果看，满分 42 分与第 4 名 28 分之间相差 14 分。更关键的是，3 个满分模型的解题过程并不一样。
Claude Fable 5 的过程最为干脆。它一共进行了 9 轮对话，其中 6 轮产生有效输出，单次最长用时为 P3 题的 73 分钟，全程输出 70 万 token。
GPT-5.6 Sol 在过程上更波折一些。它在 P2 上进行了 4 轮尝试，用时 106 分钟，期间还两次遭遇网络故障中断。不过它的总输出只有 23 万 token，是 3 个满分模型中最省的一个。
Kimi K3 的风格则完全不同。这个 2.8 万亿参数的 MoE 模型总共输出了 154 万 token，约为 Sol 的 6.5 倍。仅 P3 一题，它就发起了 6 次尝试，持续 491 分钟。
P1：不同思路解同一题
P1 是整套试题中相对温和的一题。题目要求：黑板上写有 2026 个大于 1 的正整数。每一步从中选出两个数 m 和 n，擦掉后换成 gcd(m,n) 和 lcm(m,n)/gcd(m,n)，重复操作直到无法继续。需要证明两点：
- (a) 过程一定终止，最终恰好只剩下一个大于 1 的数 M；
- (b) 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。
围绕同一道题，Claude Fable 5 和 GPT-5.6 Sol 走出了两条不同路线。
Claude Fable 5 构造了一个计数器 Φ = T + N，其中 T 表示黑板上所有数的素因子总数（按重数计算），N 表示大于 1 的数的个数。以 [12,18] 为例，12 的素因子数为 3，18 的素因子数也为 3，因此 T = 6，N = 2，Φ = 8。它证明每一步操作都会让 Φ 至少减少 1：若 gcd(m,n) > 1，则 T 减少；若 gcd(m,n) = 1，则 T 不变但 N 减少 1。由于 Φ 是正整数且每步至少减 1，过程必须在有限步内终止。
GPT-5.6 Sol 则跟踪两个量：P，也就是所有数的乘积；以及 K，也就是大于 1 的数的个数。若 gcd(m,n) = d > 1，则替换后两个新数的乘积为 mn/d，比原来更小，因此全局乘积 P 严格变小；若 d = 1，则 P 不变，但 K 减少 1。于是二元组 (P, K) 在字典序下严格递减，终止性由此得到证明。
在题目的 (b) 部分，3 个模型最终采用了同一方向：证明对每个素数 p，黑板上所有数被 p 整除次数的最大公约数在整个操作过程中保持不变，最终的 M 也可据此唯一确定。
文中的 12 和 18 例子继续验证了这一点。对 p = 2，v₂(12) = 2，v₂(18) = 1，其最大公约数为 1，对应贡献 2¹；对 p = 3，v₃(12) = 1，v₃(18) = 2，其最大公约数也是 1，对应贡献 3¹，因此 M = 2 × 3 = 6。
P6：低成本失败样本与 agent 问题
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 年，3 个通用大模型直接拿到满分。文中强调，这次成绩并非建立在专项数学训练之上，而且相关能力已不再局限于实验室使用场景，其中还有一个模型是开源的。
Axiom Math 提供了机器可读题面
整场测试的基础来自 Axiom Math。该公司把 IMO 2026 全部 6 道题逐字逐句转写成机器能够理解的 Lean 4 形式化题面。
有了这套机器可读题目，AI 才能直接输出 Lean 证明，再由编译器自动判分，不再依赖人类评委阅卷。拿到题面之后，Deedy Das 搭建了自动化测试框架，让各个模型依次跑完整套 6 道题。AxiomProver 也在这套体系下独立获得满分。
文中还提到，Axiom Math 创始人洪乐彤现年 25 岁，出生于广州，用 3 年完成 MIT 数学与物理双学位，也是 Morgan Prize 得主。去年底，她主导打造的 AxiomProver 在 Putnam 数学竞赛中获得满分，这被称为该赛事 98 年历史上的第 6 次满分。到今年 3 月，Axiom Math 已完成 2 亿美元 A 轮融资，估值达到 16 亿美元。
从数学证明到日常决策
文章最后把这类能力指向更广泛的使用场景。能写出 4229 行严格证明的模型，体现的不只是单道数学题求解能力，而是长链条逻辑推导能力：过程不能跳步，结果不能含糊，也不能“差不多对”。
文中列举了合同条款漏洞、保险理赔条件、税务方案合规性等问题，认为它们在结构上都属于需要逐条核验的任务。过去，这类工作通常依赖专业人士按小时收费完成；而随着这种能力进入消费级产品，普通用户在手机上就可能直接调用它来处理复杂问题。
参考资料为 Deedy Das 在 X 平台发布的内容。原文来自微信公众号“新智元”，作者为“ASI 启示录”，编辑为“摩西”。