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 的完整解題過程，除非你真想跟著做一遍這道題。