AI 解不出的最后一道 IMO 题，价值不在答案
2025 年 IMO 第六题只有不到 1% 的选手拿满分，所有 AI 都卡在这题上。它难的不是计算，是必须先理解、先有审美，再动笔——而这恰恰是强化学习最难训练的东西。
核心论点 · 点时间戳可跳到原声
AI 卡住的不是计算，是耐心
2025 年 IMO 第六题，全球 600 多名顶尖选手，拿满分的不到 1%。到 2025 年，多个机构的模型已经能答对所有其他题目，唯独卡在这一题。DeepMind 研究总监 Thang Luong 给的解释是：模型没有耐心，它不肯花时间去理解问题、去对问题产生感觉，而是直接开始解。Karpathy 补充了第二个原因：模型对「什么让一个问题或一个策略漂亮」没有感觉，而这道题的解法恰恰依赖审美判断。
天才其实是经验的残留物
面对这道题，最直观的构造是把所有 X 放在对角线上，用水平瓷砖覆盖剩余区域，得到 2(n-1) 块。但这个构造太显然，不可能是 IMO 要的答案。Karpathy 在这里插入了一个看似无关的立方体切割脑筋急转弯：3x3x3 的立方体切成 27 个小立方体，允许每次切完重新排列，最少几刀？答案是 6 刀，理由是最中间那个小立方体的 6 个面，每一面都需要一刀单独切开。这个证明思路——盯住内部结构的一个面——正是后面瓷砖问题的关键。
最有效的铺法让每块砖碰四个 X
把每个 X 的四条边高亮，每放一块瓷砖就关掉它碰到的边。低效的铺法里，瓷砖只碰到 1 个甚至 0 个 X；高效的铺法里，每块瓷砖碰到 4 个 X。由此得到一个猜想：最优铺法应该让尽可能多的瓷砖碰到 4 个不同的 X。但进一步看，X 不能落在瓷砖边的中间——那样上下两块瓷砖会在左边产生冲突，因为同一列不能有两个 X。X 必须落在瓷砖的角上，四块瓷砖像风车一样围着它。用边长 k 的正方形瓷砖，可以铺出边长 k² 的大网格。2025 恰好是 45²，这个巧合让构造显得极有希望。
只高亮一个方向，证明会漏掉一侧的砖
把所有 X 的边高亮，共 4k² 条，每块瓷砖最多碰 4 条，减去边界上不需要被碰的 4 条，得到下界 k²-1。但目标下界是 k²+2k-3，差了一个正比于 k 的项。问题出在只高亮右边缘：这样得到的对应关系在图的右侧很紧，但会漏掉大量集中在左侧的瓷砖。换任何一个单一方向都一样，漏掉的瓷砖总是聚在一侧。Karpathy 说，数学奖励你尊重对称性，也会惩罚你不尊重它——选一个任意方向，弱点就体现在不等式里。
把网格切成四块，每条边只高亮一次
解法是画两条路径：一条沿 X 向右上走，一条向右下走，把整个图分成四个区域。X 在右侧区域就高亮它的右边缘，在上方区域就高亮上边缘，左右上下各管一块。落在边界上的 X 高亮两条边。这样既补上了缺失的那些高亮边，又保证每块瓷砖最多只碰到一条高亮边——因为一块瓷砖坐在左侧区域时，它上方的 X 不可能高亮下边缘，下方的 X 不可能高亮上边缘，左侧的 X 不可能高亮右边缘。这个图就是整个证明的核心。
问题化归成一个纯排列问题
给每个 X 标上它所在的行号，因为每行恰好一个 X，这些标号构成 1 到 k² 的一个排列。向右上的路径对应一个递增子序列，向右下的路径对应一个递减子序列。设最长递增子序列长度为 LIS，最长递减子序列长度为 LDS，高亮边总数就是 k² + LIS + LDS - 4（两条路径相交时再 +1，变成 -3）。要证明目标下界 k²+2k-3，只需证明 LIS + LDS ≥ 2k，也就是两者的平均值至少是 k。到这里，网格已经完全消失，剩下的是一个关于排列的纯事实。
Erdős-Szekeres 定理的证明本身就是个宝石
这个纯排列事实就是 Erdős-Szekeres 定理：任何排列中，最长递增子序列与最长递减子序列的长度之积至少等于排列长度 n。IMO 选手可以直接引用定理收尾，但 Karpathy 选择把证明也讲完。做法是给每个位置标注一对数：以它结尾的最长递增子序列长度，和以它结尾的最长递减子序列长度。因为排列中数字互不相同，任意两个位置的这两对标签必然不同——如果后一个数更大，第一个标签至少加一；如果更小，第二个标签至少加一。把这些标签对画成坐标点，最长递增子序列就是包围盒的宽，最长递减子序列就是高，宽乘高等于格点数，也就是排列长度。
证明之外还有一层：让人感觉证明是显然的
Karpathy 说，知道一个证明只是深度理解数学的很小一部分。他和 Nishad Dulkhar 做这个视频时，看原证明的第一反应是「我知道它成立，但怎么会有人想出这个」。他们想贡献的不是新证明，而是一种叙事，让观众在走到证明时不再觉得它是凭空冒出来的。他给这种东西起了个名字：motivated explanation。这直接关系到 AI 与数学：如果机器能生成证明但不带来人类理解，那就完全失去了意义。而学术界一直用「证明」作为衡量进步的代理指标，这暴露出一个迫切需求——需要一种新的、独立的方式来衡量一份发表物是否真的推进了人类理解。
原话 · 已逐字校验
It also seems likely to be the last IMO problem to be solved. No problem that AI could not solve.
它很可能也是最后一道被解出的 IMO 题——最后一道 AI 解不出的题。
we didn't really have a way to teach the model to be patient. It didn't take the time to understand the problem, to get a feel for the problem, to not try to solve the problem.
我们其实没有办法教模型变得有耐心。它不肯花时间去理解问题、去对问题产生感觉、去先别急着解题。
Thang Luong3:06
what can look like genius is usually the residue of experience.
看起来像天才的东西，通常只是经验的残留物。
math rewards you when your respected symmetries, and what we're seeing right now is how it punishes you if you don't.
数学会在你尊重对称性时奖励你，而我们现在看到的，是你不尊重它时它怎么惩罚你。
I just think that's really lovely, too beautiful not to share.
我就是觉得这太美了，美到不能不分享。
if you're able to generate proofs that don't necessarily come with human understanding, that kind of completely defeats the point.
如果你能生成证明，但这些证明不必然带来人类的理解，那基本上就完全失去了意义。
the value of this question lies in the fact that it warmed my heart when I solved it, and it still warms my heart more than a year later; like a good book or a touching song the value here is human.
这道题的价值在于，我解出它时它温暖了我的心，一年多以后它依然温暖着我的心；就像一本好书或一首动人的歌，它的价值是人的价值。
数字与实体
| 2025 年 IMO 参赛人数 | 600 多名青少年 | 0:00 |
| IMO 第六题满分率 | 不到 1% | 0:00 |
| 2025 年 IMO 第六题满分人数 | 6 人 | 23:32 |
| 2024 年 AlphaProof 答对题数 | 6 题中的 4 题 | 1:00 |
| 2025 网格边长 | 2025，即 45² | 16:23 |
术语
- LeanLean
- 一种编程语言，数学证明在其中被写成程序，可被机器验证。
- Erdős-Szekeres theoremErdős-Szekeres 定理
- 任何排列中，最长递增子序列与最长递减子序列长度之积至少等于排列长度。
- motivated explanation有动机的解释
- Karpathy 造的词：一种叙事，让读者觉得一个证明几乎是显然的，而不只是能跟着步骤走。
- LIS / LDS最长递增子序列 / 最长递减子序列
- 排列中长度最大的递增（递减）子序列的长度。
收听指南
对 AI 与数学交叉、以及「理解」这件事本身感兴趣的工程师和研究者；想看清模型能力边界的人。
06:11 到 45:06 的完整解题过程，除非你真想跟着做一遍这道题。