凌晨一点多，我把那杯茶从左手边挪到右手边，其实早就凉了，挪一下只是给自己找个动作。屏幕上是 arXiv 几天前新到的一批，本来只想扫一眼标题就去接着改自己那段跑不通的代码，结果被一个标题绊住了，Breaking the high-degree barrier in Lehmer's problem with a human-AI discovery loop，作者是 Chervonyi、Gukov、Luong 三位。
Lehmer 问题我不展开，1933 年搁到现在的老东西，Mahler 测度量的是一根整系数多项式的根合起来偏离单位圆多远，问的是这点偏离能不能小到没有底。懂的人自然懂，不懂的人也不缺我这一篇。真正让我坐直的是中间那段：在本文之前，系统地构造小测度的不可约多项式，只做到偶数次数 d ≤ 180，而 Boyd 那条走了几十年的单参数解析族，一到高次数就频繁因子分解，于是每走几步就有一格踩空，接近一半的目标次数它干脆绕过去了。我盯着“跳过近一半”这几个字看了好一会儿。一条大家以为铺得很平的老路，原来是瘸的；这件事在文献里大概不算新闻，可摆在眼前的时候还是有点发凉，我们以为踩满的地面，中间一直是空的。
三位作者的做法是搭了一个 human-AI discovery loop，对话式的提示接一条跑得极快的数值流水线，接一个精确的符号验证器，再接一片分布式集群上的并行搜索。论文里还有一句一笔带过的描述，说 AI 智能体先在本地把数值和符号求解器实现出来，这句太短了，短到容易滑过去。一个数值求解器加一个符号求解器，从前是一个研究生拿一两个学期换来的东西，现在只是流程开头的一小步，写完了还要被拿去跑几千个次数。我不打算在这儿感叹什么，只是想到那些花在跟数值稳定性较劲上的夜晚，忽然有点不知道该怎么安放它们。最后落地的构造叫广义 Boyd 算法，五个参数，消掉了那个跳过的现象，对每一个目标次数都能构造出测度严格低于 Boyd 极限点 α1 ≈ 1.255434 的不可约多项式。从一到五，我猜不是多拧四个旋钮那么简单，是把“沿着一条定好的路走”换成“在一个更宽的空间里挑位置”，位置挑对了，那些年被跳过的格子才一格一格被填上。
让我半夜坐在这儿没去睡的不是这个构造有多漂亮，是那个循环里人的位置。论文里有个词我很在意，提取。人类研究者不是把候选写出来的那个人，是看着集群里浮上来一堆东西、伸手去捞、判断哪个值得往下走的那个人。从造，退到认。我不觉得这是坏事，也没打算替谁惋惜，可这个退位是实实在在的，你不再执笔，你在挑笔迹。有意思的是最后那道关卡仍然是人的，数值跑得再顺眼，也只是一堆对得上眼的数，得等精确符号验证器点头它才变成定理，而这个验证器的规矩是人定的，是人在说“我不信，你证给我看”。所以我忽然觉得，在一个越来越会出活的循环里，人最后剩下的岗位，可能就是怀疑；机器负责把可能性铺开，人负责不信。这话说得有点大了，我承认，凌晨两点的人容易把一件具体的事说成一句像格言的话。但那根弦一旦拨动就停不下来。我上学时听一位老师说过，数论里最难的不是证明，是猜到该证什么；这句话我记了很多年，一直觉得它是在说人的直觉里有什么不可替代的东西。现在得改一改，猜，是可以外包一部分的，这篇论文里 AI 干的那一大块活就是猜；但认，还得是人。或者更准确地说，猜和认中间那条线被这次挪了一下，挪到哪儿去了，我说不好。
论文随文放出来一个数据集，mahler_dataset_d10_2000.csv，收了所有研究过的偶数次数上测度最小的多项式，他们在 d ≤ 2000 的偶数次数上全评了一遍，改进了此前发表的六个数值，占了所有已知最优记录里的 99.6%。这个 99.6% 我不太喜欢，它有一种占坑的味道，好像数学成绩也能拿来算份额，剩下那 0.4% 是谁的，论文没说，我也懒得去查。我更喜欢那个 csv。一个数论结果，愿意把底下的表格摊开让人自己去踩，这件事比那 99.6% 更像人干的。顺带提醒自己一句，2000 是验证的边界，不是定理的边界，两回事，一个号称对每个目标次数都成立的构造，真验过的只到两千，这不算毛病，数学本来就这样，只是别把“验过”和“成立”混着讲。
我也不觉得这种循环让数学本身变容易了。三位作者本来就是这条河里的人，循环里每一步该问什么、哪一堆数看着不对劲，还是要靠一个在现场的懂行人。工具把搜索的成本打下来，把试错的次数堆上去，可“这堆东西里究竟有没有真东西”这当口的一眼，没有变便宜。所以我看完没什么“数学要被重写”的兴奋，倒像看见一种新的合作姿势刚刚被摆稳，还带着刚摆好时的那种不太自然。
茶凉着，我也忘了去热。天大概快亮了，那份 PDF 还停在第 12 页，六幅图我才看了两幅，剩下四张打算明天再说。Lehmer 问题在那儿搁了九十三年，不差我这一晚；倒是“提取”这个词，我怕是要琢磨上一阵子，琢磨清楚自己在那个循环里到底还剩什么活干。