AI 解不出的最后一道 IMO 题

2025 年，六百多名少年聚集在澳大利亚阳光海岸，参加国际数学奥林匹克。比赛共六题，第 6 题难出一截。尽管每位选手都是本国顶尖，满分的人还不到 1%。它也很可能是 AI 解不出的最后一道 IMO 题——哪怕再往前推五年，懂竞赛数学的人听了都会觉得荒唐。

如果你不在这个圈子里，需要知道的是：这些题本来就是要考想象力和创造力的。不是死记硬背，也不是计算。解出来并不等于给出一个数字。它意味着写出一份完整、严格的证明；竞赛的精神是，找到这份证明，应该需要对某个具体设定有细腻而深入的理解。

先退回到 2021 年。那时 AI 在游戏里已经有了令人印象深刻的成绩，自然语言的缩放定律也已经清楚，但仍有很多人觉得 IMO 是另一回事。它把严谨和创造搅在一起，写证明时逻辑步骤的搜索空间实际上是无穷的。

2023 年，Dwarkesh Patel 的播客里有一个问题：能拿 IMO 金牌的 AI，是不是就是 AGI？就在第二年，Google DeepMind 的 AlphaProof 团队交出了一个模型，解出了当年六题里的四题。有一个注脚：人还得把题目从英文翻成 Lean——一种把数学证明写成程序的语言。即便如此，找证明这件事的实质是 AlphaProof 在做，单这一点已经让很多人吃惊。

2025 年，多家机构都来试这套卷，有的用 Lean，有的纯用自然语言。从头到尾，模型解出了除这道第 6 题以外的每一题。到了 2026 年，只需给公开可用的推理模型下提示，六题就都能答对。这还低估了模型走了多远：IMO 作为基准几乎像上古史了，过去一年里，一切都已经速通进了研究级数学。

Sanderson 会在结尾再谈 AI 和数学。眼下这支视频多半不是讲 AI 的。它是对一道漂亮题目的深入剖析。沿着解题路径走下去时，值得问一句：当机器都做不出来时，是什么让几位出色的学生找到了答案。

他把这个问题问了 Thang Luong，Google DeepMind 那年那套推理模型团队的一位研究主管。Luong 说，他们其实没有办法教模型耐心：它不会先花时间理解题目、摸清手感、先不急着解。这里确实需要耐心，Sanderson 还想补一句：至少就他跟模型打交道的经验来看，它们似乎不太能感觉到一道题或一种策略美在哪里，而找到这个解法，恰恰得益于对美的欣赏。

题目是这样开始的：考虑一个 2025×2025 的单位方格棋盘。画起来太笨重，动画就从小一点的 10×10 开始。Matilda 想铺上矩形砖，大小可以不同，每块砖的每条边都落在网格线上，每个单位方格至多落在一块砖里。砖与砖不重叠。

问题问的是，在一条关键规则下，最少要用多少块砖：每一行恰好有一个单位方格没有任何砖盖住。这些空隙标成 X。同样，每一列也恰好有一个未覆盖的方格。在 10×10 上就是十个空隙；真正的棋盘上会有 2,025 个。

第一个 10×10 的例子用了 21 块砖，规则也满足——没有两个 X 在同一行或同一列——但不是最少的。换一组空隙能降到 17。再试一次到了 16。因为这是 IMO，任务不只是一个数字，也不只是展示一种构造。构造是一部分。真正的难处，是证明你找到的这个最小值确实就是最好的。

就连想出砖该放在哪里的可推广描述，都很难。最容易的做法是把所有 X 放在对角线上，其余用横向砖盖住。边长为 n 的棋盘，右边用 n − 1 块，左边用 n − 1 块，一共 2n − 1。这种构造一目了然，不太可能是 IMO 想要的。你要的是另一种一般方法，把 X 和周围的砖摆出来，让砖的数量作为 n 的函数更小。

从哪儿下手？解题的一条普遍教训是：看似天才，多半是经验的沉淀。洞见不是凭空来的。跳进第 6 题之前，Sanderson 希望你先耐心看一个看起来不相干的切立方体脑筋急转弯——比 IMO 题简单，很好玩，而这种过往经验，也许能提示铺砖谜题的第一步。

想象一个 3×3×3 的立方体，你想把它切成 27 个单位立方，刀数越少越好。每一刀都沿着一个平面切：不能拐弯。有一种显然的切法，六刀就够：沿每个坐标方向各切两刀平行的，把每条棱三等分，整个立方体就成了 27 个小立方。

有意思的变体是：每切一刀之后，你可以重新摆放碎块，把它们叠起来，让下一刀穿过更多材料。现在最少要用几刀？对任意形状来说，假设你能把所有东西都排进这一刀的平面里，每一刀最多把块数翻倍。四刀最多 16 块，所以切不出 27 个立方。

五刀原则上能切出 32 块，但这些块必须是 1×1×1 的立方，怎样重排才能做到，并不显然。要是你从没见过这道谜题，值得先停一下。拿它出来的原因是：答案恰好点出第 6 题的洞见。

窍门是盯住最里面那个单位立方。要把它切出来，六个面各需要一刀。一刀永远解不开超过一个面。所以，哪怕你把重排和叠放玩得再花，也不能少于六刀。洞见不是少切几刀的巧妙策略，而是怎么证明六刀就是最优：盯住那个内立方的各个面。

你能看出这和铺砖谜题有什么关系。找出一种砖数很少的铺法已经不容易；最终目标是证明你找到的就是最好的。要是你见过切立方体，它也许会把你引向打了 X 的方格的边。那些边每一条都得对应到一块砖。

反过来也有一条匹配约束。因为没有两个 X 在同一列，一块砖的左边或右边至多碰到一个 X，上下同理。砖的四条边，每条至多碰到一个 X。

看两种铺法，右边那种砖明显更少。它为什么更高效？先放 X；没有两个共享一行或一列，等价于放不能互相攻击的车。把每个空隙的四条边标亮。每加一块砖，就关掉它碰到的那些高亮边。

有的砖能关掉多条边，有时多达四条；有的只关一条，甚至一条都不关。最终每条高亮边都得关掉——几乎是这样。有四个例外：已经挨着棋盘外边界的那些边。这把左边那张图的浪费说得很干净：那些砖只碰到一个 X，或者一个都不碰。

右边，标出来的每块砖都碰到四个 X。如果一块砖的本职是盖住空隙的边，这些砖已经做到了最有效率。这个直觉足够根本，可以写成一条猜想：最有效的铺法，应该让尽可能多的砖各碰到四个不同的 X。一块砖要是碰到的更少，就感觉浪费了它的潜力。

先把网格抽掉，想象这些砖自由漂着，每块边界上某处都碰到四个 X。目标是像拼图一样把它们拼起来。盯住一块砖，试着在它右侧那个 X 的上下再塞两块。马上就要变得低效了。你希望每块砖都碰到四个 X，但那两块新砖会在左边冲突：左边对齐了，又不能有两个 X 在同一列，它们不可能都在左边碰到一个 X。总得有一块放弃。

只要 X 碰到砖的边中央，就会出同样的问题。把那个 X 滑到角上，你就能舒舒服服地用风车式样围上四块砖，而不强迫冲突。这是下一块直觉：砖不但要各碰四个 X，而且要想和谐共事，那些 X 必须坐在角上。

你仍然可以选任意矩形，但从正方形开始很自然。正方形对称，数学往往奖赏你尊重它的对称。同样周长下它们盖住的面积也更大，想用尽量少的砖盖满棋盘时，这感觉很高效。

一旦你假设最优铺法用正方形砖、X 在角上排成风车，把它们拼起来就真成了实物谜题。这些块叠得很好。从 5×5 正方形开始是任意的：拼了四块之后，再加一块会让两个 X 落在同一列，于是下一块错开接上，继续往下搭。

这样继续下去，会得到一个略微倾斜的 4×4 正方形砖图案，每块都带着一圈风车式的 X，一共用了 25 个空隙。这些 X 各占不同的行和列，所以外面套一个大棋盘就符合题意。边缘还得补几块砖填缝，所以并不是每块砖都碰到四个 X——但内部的都碰到了，这感觉很高效。

从 5×5 开始是任意的。4×4 正方形给出更小的布置，16 个洞；3×3 正方形给出九个。一般地，若 k 是那些正方形砖的边长，这个图案能铺满边长为 k² 的大棋盘。如果你要去参加 2025 年 IMO，你知道 2025 是个平方数，具体是 45²。令 k = 45，就得到原棋盘上一种漂亮的铺法，以及最少砖数的一条猜想。用上 2025 是平方数这件事，感觉就像 IMO 可能想要的那种构造。

还是那句「天才是经验的沉淀」：2025 年的选手还有另一条路可能把他们引向这个图案——他们降落的澳大利亚阳光海岸机场，地板就是同样错开的方砖。我们现在有了一种猜想中的最优铺法。继续用 k 表示小正方形的边长，k² 表示大棋盘的边长。

k = 5 时，内部用 16 块正方形砖，也就是 (k − 1)²。边界每边四块，一般化成每边 k − 1，再加 4(k − 1)。展开后，砖数是 k² + 2k − 3。这是一条摸得着的猜想。我们还远没完，因为现在的目标是证明这个表达式就是最小值：其他任何 X 和砖的布置至少要用这么多，至少在棋盘边长是平方数时如此。

这种事怎么证？所有可能的空隙布置，以及它们周围所有可能的铺法，集合起来复杂得可怕。要在覆盖所有这些图案的严格论断上踩稳一脚，才是真正的难处——本来就该如此。这是 IMO 上最难的一题。没有任何一个世界里它会容易。

我们确实有一个优势：引导构造的同一条直觉——砖需要盖住 X 的每一条边——也给证明找到了落脚点。X 的总数是 k²，屏幕上的小例子是九个。把它们所有的边都标亮，得到 4k² 条高亮边，每块砖至多碰到其中四条，所以至少需要 k² 块砖。

这不完全对：整张图外边界上那四条高亮边，并不需要任何砖去碰。所以相关的边是 4k² − 4，每块砖仍至多碰四条，意味着至少 k² − 1 块砖。一方面，我们证明了某种下界。另一方面，它比我们需要的弱。猜想中的构造还有一项与 k 成正比，也就是棋盘边长的平方根。

多出来的那一项说得通：在我们希望最优的布置里，并非每块砖都碰到四个 X。边界附近的只碰到两个。Sanderson 在笔记本里花了很长时间，想找一个漂亮的论证，给必须待在边上的砖数一个界。要是老老实实把死胡同都演一遍，这支视频会变成九小时。没什么真正管用，而这有一个根本原因——但这不等于我们不能继续拿高亮边做文章。

回想立方体。关键是内立方的各个面和刀锋之间的一一对应。到目前为止，铺砖的论证更像空隙边和砖之间的 4 对 1 对应。有一种更简单的办法，用 1 对 1 的关联得到同样的 k² − 1 下界：不要把每条边都标亮，只标打了 X 的方格的右边。

那些右边每一条都必须碰到一块砖，而任意一块砖至多碰到其中一条，因为没有两个 X 在同一列。同样有一个边界例外：最右边那条不必碰到砖。所以你再次至少需要 k² − 1 块砖。这种说法更有产出，因为你能看出它低效在哪儿。你漏掉了图左边整整一簇砖。

如果改成只标上边，你就会漏掉底部附近许多砖。任意一个方向，漏掉的砖都挤在一侧。数学奖赏你尊重它的对称，这里则惩罚你不尊重。选一个任意方向，关联里就露出明显的弱点，而这个弱点也反映在不等式的弱上：至少 k² − 1，而我们要的是 k² + 2k − 3。

那个 k² + 2k − 3 来自我们希望最优的布置。对想证明更紧的界的老练选手来说，现在正好停一下。这是 IMO 的 P6。当场只有六名学生拿了满分，也是所有 AI 都绊倒的唯一一题。我们要写的任何证明，都会是很难找到的东西。

盘点一下。策略是标出边的某个特定子集，论证每条这样的边都碰到一块独一无二的砖，于是砖数至少等于高亮边的条数。单方向版本在图的一侧很紧，另一侧却漏掉一簇。目标是把 k² − 1 加强到 k² + 2k − 3。自然要问：怎样改同一套策略来补这个弱点。

能不能再多标几条边——最好恰好 k² + 2k − 3 条——同时避开死盯一个方向的低效？你得小心。策略要成立，问一块砖碰到几条高亮边，答案必须始终至多是一。整个前提是每条高亮边至少对应一块砖，所以不能重复计数。

这个目标有一点怪。看 k 变大时的 k² + 2k − 3。如果这就是最终的高亮边条数，那么在大情形里，大多数但不是全部的 X 各得到一条高亮边，大约 2√n 个会得到不止一条。这几乎像是在跟一种漂亮的对称构造作对。下一步是整套论证里最难给出动机的，所以先从整体草图开始会有帮助。

把所有 X 的右边标亮，在右侧附近感觉更高效。那如果只在 X 落进棋盘某个朝右的区域时，才标它的右边呢？同样，只在朝上的区域标上边，朝左的区域标左边，朝下的区域标下边。眼下这四个区域以及它们之间的边界可以先模糊着。这张草图只是为了避开一次只盯一个方向的弱点。

同一条直觉也提示多出来的高亮边可能从哪来。我们需要的砖比 X 多，所以无论四个区域怎么定义，坐在它们边界上的 X 都可以得到多条高亮边，因为它同时属于两个区域。

说具体一点，把尺度缩小。出于把图分成四个区域的动机，画一条往右上走、串起一串 X 的路径，再画一条往右下走的，整张棋盘上就留下一个歪歪扭扭的大十字。穿过 X 的原因是我们希望它们在边界上，好给这些 X 标多条边，把计数抬高。

选定两条路径之后，区域就能精确定义。若一个 X 在两条路径的右边，标它的右边。若它在两条路径上方，标它的上边，左边和下边同理。边界上的任何 X，按它所在的象限标两条边。这正是我们想要的：最终需要的高亮边比 X 略多。

记住目标。我们要论证：无论 X 怎么排，无论剩下的方格用什么砖铺，砖数至少等于我们标亮的边数。只要每条高亮边碰到一块砖、每块砖至多碰到一条高亮边，这就成立。屏幕上的例子里，给每块砖写上它碰到几条高亮边，你永远只得到 0 或 1。没有砖碰到两条。

在这套设定下，为什么一块砖碰不到两条高亮边？整套论证就靠这个。盯住坐在左区域的一块砖。它也许碰到四个 X，但其中只有一个有高亮边贴着这块砖。它上方的 X 只可能标左边或上边——按区域定义，下边标不了。它下方的 X 标不了上边。左边的 X 标不了右边，那会要求它坐在朝右的区域里。

把棋盘分成四个区域，不但让高亮边和砖的关联更紧，还保住了关键性质：没有两条高亮边能碰到同一块砖。这张图是证明的核心。剩下的是说明为什么这套设定给出那个具体的紧界 k² + 2k − 3，这归结为数我们标亮了多少条边，而这又归结为有多少个 X 落在图上交叉的两条边界线上。

到这一步，给 X 贴上标签会有帮助，而不只是纯看图。在每个 X 上方写下它所在的行号。因为每一行恰好一个 X，这些标签就是从 1 到 k² 的每一个数，只是顺序打乱了：一个排列。往右上走的路径对应标签严格递增的序列——排列的一个递增子序列。往右下走的路径则是递减子序列。

把递增子序列的长度叫 A，递减子序列的长度叫 B。来数高亮边：k² 个 X 每个至少得到一条，或者说几乎每个都得到。应该有四个例外，就是碰到棋盘边界的那些 X，因为它们不必碰到砖。把这四个减掉。然后有额外的：递增子序列上的每个 X 得到第二条边，加上 A；递减子序列上的每个再加一条 B。

如果我们抠细节——而这是必须的——还有另一种可能：一个 X 同时落在两条路径上。那时它的四条边都会标亮，但按目前的计数它只算了三次——一次因为它存在，一次因为递增子序列，一次因为递减。这个特例里还得再加一。这个表达式现在离我们要的已经近得让人着急。

我们实际上证明了：对任何由 1 到 k² 的排列描述的 X 布置，如果你选出长度为 A 的递增子序列和长度为 B 的递减子序列，砖数至少有这么大。对照猜想，自然希望论证 A + B ≥ 2k，也就是棋盘边长平方根的两倍。很接近，又有点怪：你怎么保证，无论 X 长什么样，总能选出一条递增子序列和一条递减子序列，长度之和至少是棋盘边长平方根的两倍？

先规定 A 不是任意递增子序列，而是最长的那条，并改名为 LIS。同样取最长的递减子序列，LDS。稍微整理一下，证明的最后一步是说明这两个长度的平均始终至少是 k，也就是排列大小的平方根。这件事已经跟棋盘无关了。它是关于排列的一条纯粹事实。

画面可以从棋盘抽离，把每个数画成一根高度等于该数的柱。递减子序列都很短的排列，往往有一条很长的递增子序列；反过来，递增子序列都很短的排列，会有一条很长的递减子序列。要完成证明，得把这种权衡量化：无论什么排列，LIS 和 LDS 的平均至少是 n 的平方根。

这话说起来拗口，而我们已经走了很长的路。证明里再套一个证明，也许会把观众能合理付出的注意力绷得太紧，但最后一步是一块宝石。要是如实描绘一个走到这一步的奥赛学生，他们会引用训练里见过的东西：Erdős–Szekeres 定理。Sanderson 不想凭空抛出一个事实。他希望它感觉像是你自己也能发现的，哪怕这会给已经很长的旅途再加几分钟。

为了建立直觉，先看极端。把 1 到 n 按顺序列出的平凡排列，LIS 长度为 n，每条递减子序列长度为 1。先按顺序列出所有偶数再列出所有奇数，LIS 至少是 n/2——说「至少」，因为 n 可能是奇数——LDS 等于 2。按三的步长往上数，LIS 至少 n/3，LDS 等于 3。

琢磨这一族例子，你也许会猜想这两个数的乘积始终至少是 n。族里有一个例子看起来非常眼熟。若 n 是平方数 k²，你恰好得到最优棋盘上 X 的那种图案。最长递增子序列有很多选法，但长度都是 k，LDS 同样是 k。这个特例里乘积是 k²，正好是排列的大小。

基于这些例子的猜想是：对任意排列，乘积 LIS · LDS 至少是 n。对照目标——两者的平均至少是 √n。对奥赛学生来说，乘积界能给出我们需要的东西，这一点立刻就清楚。他们熟得不能再熟的一条常见不等式是：(a + b)/2，算术平均，始终至少是 √(ab)，几何平均。

用在这里，LIS 和 LDS 的算术平均至少是它们乘积的平方根；若猜想成立，整个表达式至少是 √n。记住我们为什么在乎：带两条路径的高亮边论证，给出了一个用这两个长度表示的式子。我们希望它至少等于最优构造的砖数，而这归结为路径长度之和至少是 2k。由 AM-GM，只要两个长度的乘积始终至少是 n，这就成立。

要是这感觉脑子里装不下，这本来就是一道难题。现在一切都收成了一条猜想。退回来反思之前，还有最后一公里：为什么这个不等式成立。我们不是第一个猜到它的。它在排列研究里很有名，叫做 Erdős–Szekeres 定理。

在真正的奥赛里，学生直接引用这条定理就可以收工。Sanderson 也可以省下你的脑力，照样做，也许链到 Wikipedia 就结束。这个事实的证明本身就很漂亮，只为剪掉两分钟片长而把它抢走，会很可惜。在我们退回来之前，这是一个让人愉快的收尾。

想法是：看到列表中间某处，问在这一点结束的最长递增和最长递减子序列是多长。屏幕上标亮的那根柱，这两个长度是 2 和 3。把它写成柱下的一对数字，排列里每一项都这样做。再拉一个例子：某根柱在此结束的 LIS 长度可能是 3，因为左边有两根递增的柱，而在此结束的最长递减子序列长度是 2。

巧妙之处是：这些对必须全部互不相同。盯住两根柱，假设左边那根标成 (x, y)。这是一个排列，所以所有数都互不相同，一根柱比另一根高。如果第二根更高，你可以取在第一根结束、长度为 x 的最长递增子序列，再延长一项，于是在第二根结束的最长递增子序列至少是 x + 1。

类似地，如果第二根更矮，你可以延长在第一根结束、长度为 y 的最长递减子序列，于是第二根柱的第二个标签至少是 y + 1。无论哪种，第二对里总有一个数比第一对里对应的那个更大。这些标签确实互不相同。

写下这么多对之后，很难不把它们画成坐标网格上的点。整体最长递增子序列是最大的 x 坐标，也就是包住这些点的包围盒的宽。整体最长递减子序列是最大的 y 坐标，也就是盒子的高。盒子的面积，宽乘高，等价于数盒子里的格点。

因为排列的每个元素都对应一个独一无二的格点，这两个数的乘积必须至少是排列的元素个数。这就是那条猜想。它很可爱，美得不该不分享。

作为收尾，退回来总结一下，因为内容很多。题目问的是：每列一个空隙、每行一个空隙，最少要用多少块砖。论断是：最小砖数来自边长为 k 的正方形砖那种特殊网格图案，一共 k² + 2k − 3 块。视频前半大部分都在铺垫到一张图；你真正会写下来的证明，从那里才开始。

对任意铺法，看空隙，画两条路径：一条连接最长递增子序列，一条连接最长递减子序列。这两条路径把图分成四个区域，由此定义打了 X 的方格上该标亮的那一组边——右区域标右边，上区域标上边，边界上标两条。每条这样的高亮边对应一块独一无二的砖，所以砖数至少等于高亮边的条数。

高亮边的条数算出来是 k² 加 LIS 加 LDS，再减 4。如果路径相交，你可以再加 1，−4 就变成 −3。到目前为止有一处略过的细处：即使路径并不在某个打了 X 的方格上相交，你仍然可以安全地加 1，因为那时它们相交在一块砖上，而那块中间的砖碰不到任何高亮边。所以无论哪种，你都可以给计数加 1。这个表达式确实是砖数的一个下界。

这反过来就证明了我们想要的界，也就是最优铺法的 k² + 2k − 3，只要两条路径长度之和至少是 2k——上一节证的就是这个，把 AM-GM 和 Erdős–Szekeres 合在一起。代入 k = 45，就得到原题的数字答案。数字答案只是要点里很小的一部分。真正的要点是构造，以及它最优的严格证明。也许花了不少时间，也需要相当的耐心。我们恰好做到了这一点。

意义何在？看清怎样解这样一道题，我们学到了什么？Sanderson 切到面对面的收尾。他介绍这道题时说它是 AI 解不出的最后一道 IMO 题，这也许会让人想到 Lee Sedol 对 AlphaGo 的第四局那种收束：人类的最后一搏，此后机器就全面更好了。

很多观众大概一直在问，这道题对 AI 为什么这么难。猜测很自然。大量工作是视觉直觉，比纯符号推理更难训练。更微妙的一点是 Thang Luong 说的：这种题你没法立刻动手写解答。你得先理解它、摸清手感。这种结构对强化学习环境来说本质上更难。

Sanderson 自己和这道题的关系，指向另一个地方，在 AI 与数学的更大故事里更重要，而且跟 AI 何时能解、何时解不出这类题无关。他和 Nishad Deulkar 一起写了这支视频。他们动手时，目标并不是给一道未解题找新证明。证明已经存在。它甚至已经在 YouTube 上：一个叫 Dedekind Cuts 的频道覆盖了很多 IMO 题，包括这一道。

那为什么还要做这支视频？有什么新东西可以贡献？知道一个证明，只是深入理解一块数学时那种感觉的很小一部分。这份证明尤其如此：Deulkar 和 Sanderson 看着它会说，我看出这能行，但你到底是怎么想到的？你定义一条最长递增子序列、一条最长递减子序列、边和砖之间某种对应——没有铺垫的上下文，你可以跟着步骤走，最后觉得它完全是晴天霹雳。

视频里他谈过找到构造和把证明讲清楚之间质的差别。他没提的是还有另一层投入，感觉上也有质的不同：造出一种叙事，让观众觉得那份证明几乎是显然的。我们知道它并不显然。只有六名学生解出来。难度是摆明的。但如果他们把工作做对了，等到证明本身讲出来时，它就不像晴天霹雳了。

找到那种叙事，回报极深，也非常有创造性。他每次出来，对一块数学的理解都远好过仅仅看懂证明。给另一件事起个名字会有帮助。暂时没有更好的词，他称之为「有动机的解释」。

从这道玩具题走到更广阔的世界，机器正在给出著名未解题的证明，你会看到数学家在反思：按他们对这门实践的理解，做数学的目的从来都是推进人类的理解。证明和开放问题的角色是一盏引路灯，指出该把理解往哪里、怎样往前推。解几乎从来不是你塞进一个应用就能拿到效用的东西。它比那更微妙。

人要找到这些证明，必须摸清思维模式、构作和新的数学对象，把理解抬高到足以让证明出现。有用的不是证明，甚至也不是结果。有用的是周围的理解，以及它可能溢进工程世界的那些效应。如果你生成的证明并不带着人类的理解，那就完全把意义给消解了。

这提出了一个严肃问题：我们怎样衡量学术进展。把证明当作代理，已经深嵌进我们给学术功劳的方式里，以至于暴露出一种鲜明的需要：用一种新的、不同的办法，衡量某人发表的东西是否真的推进了人类理解。Sanderson 认为，「有动机的解释」这个想法可以在很大程度上填上这个空缺。共同体应该试着把它的含义形式化，再把它抬到证明在历史上拥有的同等地位——以及同等的学术功劳。

他对这个话题还有更多想法。他为此给 Terence Tao 的博客写过一篇客座文章，并在这个频道录成了视频。他猜这会是他想表达的、关于 AI 与数学的许多想法里的第一则。今天，回到这道 2025 年的 IMO 题，他用 Patreon 评论里的一段心情作结——他会在那里给支持者提前放视频。其中一位留下了一段引语，来自解出这道题的一位朋友。

「这道题并不贡献对数学的深刻理解，跟数学研究比也并不特别难。相反，它的价值在于：我解出来的时候，心里是暖的。一年多以后，它仍然暖着我的心。像一本好书或一首动人的歌，这里的价值是人的。就当我是人文主义者吧，但我真心相信，这道题作为一项数学发现的价值，超过普通的博士论文。」