从一道 IMO 题看 AI 数学能力的边界与追赶

2025 年国际数学奥林匹克在澳大利亚阳光海岸举行。六道题里，第 6 题最难，拿到满分的选手不到百分之一。它后来成了一个很短暂却很醒目的标记。当时许多 AI 系统已经能解同届试题中的其余题目，偏偏停在了这道平铺题前面。

视频发布时，这个标记已经快失效了。3Blue1Brown 提到，到 2026 年，普通人可以直接调用的推理模型已经能正确处理那套题的全部六题。把这期视频当成一份“人类最后胜利”的纪念册，会错过它最有价值的部分。Grant Sanderson 借一道题追问的，是解出答案之外还有哪些数学活动值得珍视。

一张很大的方格纸

题目看上去像平铺游戏。给一张 2025×2025 的单位方格纸，放进若干个边平行于网格的矩形砖块。砖块不能重叠。每一行恰好留下一个没有被覆盖的小格，每一列也恰好留下一个。题目要问，最少要用多少块砖。

每行一个空格、每列一个空格，意味着这些空格的位置组成了一个排列。小一点的棋盘上，人可以随便把空格排到对角线，再用横向长方形补齐两边。这样容易做，却不够省砖。真正难的部分也不在于猜一个数字。IMO 要求的是完整证明。你得给出一种最省的摆法，还得说明所有别的摆法都不可能更省。

视频把大棋盘先缩到小棋盘，让人看清两件事。空格的位置会决定砖块是否高效。一块砖如果能同时贴住多个空格的边缘，它就替更多局部约束干了活。相反，若一块砖只处理一个边缘，甚至碰不到任何空格，它很快就会把总数推高。

这种说法听起来朴素，却带出了整道题的入口。人先从图上看见了“边缘”这个对象，才有可能把难题改写成计数问题。计算机当然也能枚举许多图案，但在巨大的搜索空间里，哪个对象值得盯住，往往比后续计算更早决定方向。

好构造先让砖块忙起来

最优构造的图形很漂亮。把 2025 看成 45 的平方，把每行和每列分成 45 组。空格按一种块状的排列分布，砖块围绕它们形成边长为 45 的方形结构。数出来，所需砖块数是 45²+2×45−3，也就是 2112 块。

这个数字本身没有太多戏剧性。构造被看见的过程才有意思。视频先让观众给每个空格的四条边做标记，再去观察一块砖最多能碰到多少条标记边。高效的砖块能同时碰到四个空格的边。构造里的方砖大量实现了这件事，边界处的砖块则承担剩下的缺口。

这里有一个常见的误会。很多人把数学创造力想成突然跳到答案。视频刻意放慢了这个过程。它展示了一连串不够好的尝试，展示一条显然成立却过弱的下界，也展示作者在笔记本上盯着棋盘边界很久而没有找到合适论证的时刻。

这些绕路没有被剪掉，因为它们说明了构造的来源。看见一块砖“最多服务四条边”，还不足以完成证明。人接着要问，哪些边该被计数，怎样计数才不会让同一块砖重复承担两个标记。这一步把一个视觉感觉变成了可以落笔的约束。

弱下界告诉你漏在了哪里

最直接的计数法会得到 k²−1 的下界。把棋盘边长写成 k²，所有空格的某一侧边，比如右边，逐一标出来。每条这样的边都要贴着一块砖；由于每列只有一个空格，一块砖又不可能贴住两条被标出的右边。除去最右侧边界的例外，至少需要 k²−1 块砖。

这已经是一个正确证明，但距离目标还差大约 2k 块。弱下界的价值常被低估。它没有告诉你答案，却精确暴露了失败位置。只标右边，会让棋盘左侧的一批砖完全失去踪影。若改标上边，漏掉的又会集中到下方。

Sanderson 在这里说了一句很有用的话，数学会奖励你尊重对称性，也会惩罚你忽略它。这里的对称性不是一句美学口号。四个方向在题目里地位相同，证明若只偏爱一个方向，遗漏就会集中出现。下界之所以弱，原因已经写在图上。

接下来要让四个方向各自负责一片区域。问题随之变成，区域的分界线怎样画，才能让每块砖至多碰到一条被标记的边。这个限制很苛刻。多标一条边的冲动必须克制住，证明里只要有一块砖碰到两条标记边，一一对应的计数就塌了。

两条路径把图形接到排列上

视频选择了两条穿过空格的单调路径。一条从左到右向上走，一条从左到右向下走。它们像一个歪十字，把棋盘分成四个区域。右侧区域的空格标右边，上方区域标上边，左侧和下方也按相应方向处理。落在路径上的空格会获得两条边的标记。

这套安排看似奇怪，作用却很直接。每块砖即使接触到四个空格，也至多碰到一条标记边。区域的方向规则把其他可能的边排除了。于是，标记边的总数就是砖块数的下界。路径上的空格多出来的一条标记边，正好补回单方向计数法漏掉的那一截。

走到这里，几何图像仍然在场，可问题已经换了语言。按从左到右的顺序读空格，把它们所在的行号写下来，会得到 1 到 k² 的一个排列。向上走的路径对应这个排列的一条递增子序列，向下走的路径对应一条递减子序列。

一张棋盘里的两条线，变成了排列中的最长递增子序列和最长递减子序列。这种换语言的动作，是整份解答里最容易显得像魔法的地方。视频没有把它当作无缘无故的技巧，而是把前面的计数失败、四方向的需求和路径边界一点点接起来。读者看懂之后会发现，路径并非凭空出现，它们是在替区域规则找一个不会冲突的边界。

一条老定理把最后的缺口补上

设最长递增子序列的长度为 LIS，最长递减子序列的长度为 LDS。前面的边缘计数把砖块数压到了一个含有 LIS 和 LDS 的式子上。要得到目标下界，只需要说明这两条路径的长度加起来足够大。

这里用到了 Erdős和Szekeres 定理。对任何长度为 n 的排列，最长递增子序列长度与最长递减子序列长度的乘积至少是 n。因为算术平均数不小于几何平均数，当 n=k² 时，LIS 与 LDS 的平均长度至少为 k，它们的和至少为 2k。

视频还给了这个定理的简洁证明。给排列里的每个数标一个有序对。第一个数字表示以它结尾的最长递增子序列长度，第二个数字表示以它结尾的最长递减子序列长度。任取前后两个元素，后面的元素要么更大，要么更小，于是它的两个标签中总有一个会严格变大。每个元素的标签对都不同。

把这些不同的标签点放进一个矩形格子里，矩形的宽由 LIS 控制，高由 LDS 控制。既然 n 个元素对应 n 个不同格点，矩形面积至少是 n，乘积下界就出来了。到这一步，最初的大棋盘、方砖和空格都暂时消失了。留下的是排列里递增与递减之间的不可兼得。

这也是竞赛数学迷人的地方。一道平铺题不只靠一个领域的技巧。几何直觉把人引到边缘，计数给出下界，排列定理补上缺口。最终写在答卷上的证明可以很短。那几页文字压缩了几次换对象、几次发现旧办法漏在哪里的过程。

一道题里有三种不同的工作

这期视频把三种常被混在一起的能力拆开了。第一种是找到构造。面对巨大的网格，人需要猜到空格应当如何分组，砖块为何会呈现那样的方形结构。第二种是验证构造。你知道 2112 块能铺出来以后，还要排除 2111 块甚至更少的可能。第三种是解释构造。讲述者要带读者从空格的边缘出发，穿过弱下界，再看见两条路径如何把问题送进排列理论。

竞赛评分主要看第二种工作。答卷上给出严谨证明，阅卷者便能判定对错。训练却离不开第一种。学生做题时总会积累一些很难写进最后答案的经验。看到一张格子图，他知道先找局部对象。发现一个计数只差线性项，他会去看漏掉的对象集中在哪。图形有四个对称方向时，他会警惕自己是否只选了其中一个。这些经验不会保证成功，但会让下一次猜测比盲目搜索更有方向。

第三种工作经常最容易被忽略。一个成熟的讲解会把已经完成的证明拆开，找回它原本解决的疑问。视频用立方体切割题解释为何要盯住空格边缘，用单方向标边的失败解释为何要画四块区域，再让排列的递增和递减路径自然承担分界线。观众最后看到的是一条连续的路线，而非一串必须记住的技巧。

这三件事对应着 AI 时代里不同的任务。模型生成一份形式正确的证明，解决的是第二件事的一部分。它也可能参与第一件事，提出构造、举反例、快速检查小规模情形。可第三件事没有自动发生。解释要求取舍。讲述者要判断哪个失败尝试能帮助读者，哪个形式化细节会遮住核心，哪个已有定理该在何处出现。它接近教学，也接近研究里的概念整理。

数学界过去把证明当成重要的信用凭证，有很充分的理由。证明可审查，能被他人接续，错误也能被定位。AI 让这个凭证的含义发生了变化。若机器能够以极低成本给出大量候选证明，稀缺的东西会逐渐移到别处。人们需要分辨哪些结论带来了可复用的概念，哪些只是完成了一次搜索，哪些解释能让后来者少走很多弯路。

这不会让严格性退场。恰好相反。数学解释如果脱离严格性，只会变成好听的故事。视频的高明之处在于，它没有用“直觉”替代证明。每一次视觉判断都被接到可检查的陈述上。每块砖最多触碰一条标记边，路径的长度怎样计入，标签对为何互不相同，这些地方都要经得起逐步核验。人类理解和形式验证在这里分工不同，却需要彼此托住。

当竞赛题不再是能力终点

IMO 一直是一个特殊的测试场。题目短，定义清楚，答案可以被严格判定，还专门考察参赛者在有限时间里调动已有知识、组织新想法的能力。它曾经很适合用来观察 AI 是否能越过符号操作和模板解法。模型在这类题目上的进展，也确实提供了一个直观的刻度。

可刻度一旦被跨过，就要换问题。公开模型能解一套往年试题，说明它在训练、搜索和推理上取得了实质进步；它不等于模型已经拥有成熟研究者面对陌生问题时的全部能力。研究中的题目没有固定长度，定义有时需要自己发明，证明还会和实验、反例、已有文献缠在一起。更棘手的是，很多方向根本没有标准答案可以立刻验收。

反过来，人类也不该把“模型已经会做题”听成数学教育失去价值。学生学竞赛题，当然希望最后能写出正确答案。可更长久的收获往往来自中间的训练。看见一个构造后，能复述它为何合理；拿到一条定理后，能判断它填补的是哪处缺口；走不通时，能说清自己卡在猜构造、证下界，还是缺少一条连接不同领域的桥。这些能力会让人更善于与 AI 合作，而不是只等一个答案出现。

对工具设计者来说，视频也给了一个朴素的产品方向。解题界面可以保存多种构造、展示小规模反例、把一条过弱的下界标出它漏掉的区域，并让用户回溯某个定理为何在此处被调用。若工具只把最终证明压缩成一段流畅文字，使用者很容易误以为理解已经发生。把试错和选择暴露出来，会慢一点，却更接近学习本身。

AI 的追赶已经改变了这道题的新闻性。它仍然保留了另一层价值。2112 这个答案会被新模型很快算出，空格边缘、单调路径和排列标签之间那条由浅入深的路，仍然值得一遍遍讲。数学从来不只是把一个命题盖上“已证”的印章。人靠它训练自己怎样看见关系，怎样承认旧办法不够，怎样把后来的人带到同一处风景前。

这也解释了为什么一部五十多分钟的数学视频愿意花那么多时间讲一条已经存在的证明。它没有宣布新定理。它做的是另一种劳动，把别人写下的答案重新组织成可感受的推理过程。观众在中途停下来画图、猜测、怀疑那条弱下界，最后才会明白一份成熟解答所省略的东西有多少。这样的讲解不会降低数学的门槛，它让门槛旁多了一盏灯。

AI 缺过的，可能是等待

DeepMind 研究负责人 Thang Luong 给过一个判断，团队当时很难教模型耐心。他说的耐心不是让模型在同一条推理链上多吐一些字。它指的是暂时不写答案，先熟悉问题，去感受哪些图案反复出现，哪种不对称让计数失效，哪个看似无关的旧题会提供入口。

这正是视频开头拿切立方体谜题做铺垫的原因。把一个 3×3×3 立方体切成 27 个小立方体，允许每刀之后重新摆放碎块。人很容易先想怎样用更少的切割达成目标。关键洞察却在内部小立方体的六个面。每个面都要由独立切面切出，少于六刀不可能。这个小题没有给出平铺题的答案，却训练了一个习惯。最优性证明常常要从一个局部对象的必要代价入手。

这种经验很难被缩成一条提示词。它也不必被神秘化。模型已经在追赶，而且追赶得极快。2024 年，DeepMind 的 AlphaProof 解出了当年 IMO 六题中的四题；2025 年，不同团队的系统能解出除本题外的全部题目；到 2026 年，公开可用的推理模型已能解完整套题。把某个题目暂时做不出，当成永久的人类堡垒，没有意义。

更值得关心的是，训练目标会奖励什么。若系统主要因为快速给出可验证答案而获得回报，它自然会偏向尽快开始写证明。可许多难题的第一步恰好是延迟输出。人需要把一堆不成熟的图像、反例和感觉留在脑中，允许它们彼此碰撞一会儿。这种过程难以记录，也不容易在标准答案里留下痕迹。

证明之后，还要把路讲出来

视频末尾提出了一个更大也更实际的主张。证明只是理解数学的一小部分。一个人可以逐行核对证明，确认每一步都成立，仍然不知道为什么有人会想到画那两条路径，为什么会转去看递增子序列，为什么那条弱下界反而值得保留。

Sanderson 把后一种工作称为“有动机的解释”。这个说法值得认真对待。它不是把严谨证明配上几张更漂亮的动画，也不是把结论翻译得更浅。它要求讲述者重新走一遍发现的路线，从众多可能的定义和定理里找出真正推动理解的那几块，再按读者能接住的顺序放回来。

AI 能生成证明后，数学共同体会越来越常遇到这个问题。一个新结论是否有价值，不能只看机器能否给出形式上无误的推导。人还要知道它引入了什么对象，改写了什么旧问题，能否迁移到别处，谁能因此多看懂一点东西。学术评价若只奖励最后那份证明，会把这些工作继续当成附属品。

这道 IMO 题没有提供一条关于人类与 AI 的终局结论。它提供了一个更细的切面。模型会越来越会做题，人类也会越来越需要说明什么叫做理解。对学生来说，这意味着别把没立刻想到解法当成失败。对做工具的人来说，这意味着系统不该只会产出答案，还该能暴露假设、保存尝试、解释选择。对写数学的人来说，证明正确之后，故事还没结束。

内容来源："The last IMO problem AI could not solve"丨3Blue1Brown