假设明天早上，你醒来，发现黎曼猜想被证明了。
没有数学家闭关十年，没有几百页手稿。只有一条消息：某个 AI 跑了三天，生成了一份证明，Lean 检查通过。
下午，另一个猜想也被解决了。
晚上，系统提醒：今日新增定理 114,514 条。
你甚至懒得点开。
这当然是一个思想实验，不是对当前 AI 能力的新闻播报。但它让我有点不舒服的地方，并不只是“数学家是不是要失业了”，而是一个更根本的问题：如果正确的定理可以无限供应，我们究竟还想从数学里得到什么？
我一直有一个观点：数学研究的本质是 intuition + motivation。
这句话需要稍微展开，否则很容易变成“机器负责算，人类负责灵感”那种听起来很舒服、细想又没说什么的话。
我的意思是：
Proof 问：Is it true?——它成立吗？
Intuition 问：Why should it be true?——为什么事情应该如此？
Motivation 问：Why do we care?——为什么这个问题值得问？
数学研究当然需要证明。但如果只用“产出了多少条经过证明的命题”来描述数学研究，我觉得最重要的东西反而被漏掉了。
我们想要的不只是更多正确的句子，而是更有力量的理解：看见结构，知道该问什么，并且明白答案为什么长成这个样子。
说这件事之前，我想先讲一只钟。
一门数学系开的课，居然在讲造钟
大学的时候，我上过清华数学系郑绍远教授的一门文化素质课，印象里就叫《经度》。主要内容是带着大家读 Dava Sobel 的那本《经度》。
很多细节已经忘了，但有一个感受一直记得：原来造一只准确的钟这么难。
《经度》讲的是海上定位。船开到大洋中央，怎么知道自己在东西方向上走到了哪里？
先把实际观测的细节放在一边，用理想化的太阳时来理解。地球一天转一圈：
$$ \frac{360^\circ}{24,\mathrm{h}}=15^\circ/\mathrm{h}. $$
所以，两地的时间差可以换算成经度差。如果船所在地正午时，参考地点已经是下午两点，那么船就在参考地点以西 30 度。
原理讲完了。
剩下的问题是：你怎么在几个月后的大洋中央，知道参考地点现在几点？
今天听起来：带块表啊。
十八世纪听起来：你说得轻巧。
陆地上的钟可以很准，但船会摇晃，温度会变化，金属会热胀冷缩，摩擦和润滑也不肯老实待着。每天差几秒，看起来屁大点事，累积一个多月，再换算成海上的位置，就不是“这表走得不太准”，而是“这礁石怎么在这里”。
John Harrison 为这个问题折腾了几十年。从 H1、H2 到 H3，再到 H4。其中 H3 就花了约十九年，却仍没达到他需要的效果。后来完成于 1759 年的 H4，已经转向一只大型怀表的形态，而不是继续沿着前三台大型海上钟的形态做下去。格林尼治皇家博物馆对这段过程有详细介绍。
当然，H4 也不是一出场，全世界航海问题就自动清零。成功的样机、可复制的制造工艺和普遍可用的工具之间，还隔着很多工作。
但这里已经有一个非常鲜明的反差：计算经度差只需要一行式子，把这行式子变成可靠的海上定位方法，却需要几十年的技术探索。
问题没变，方法可以换
现在回头想，这门课给我的启发，不是“数学没用，工程才有用”。恰恰相反，是我们很容易把某个环节的完成，误认成整个问题的完成。
写出关系式，是一种完成。造出钟，是另一种完成。让船员真的能靠它航行，又是另一种。
而研究最容易发生的错位，是做着做着，忘了自己最初到底想完成什么。
数学里也有这种体验：为了证明一个 lemma，推了三十页，各种 estimate 越来越变态，每一个 $\epsilon$ 都被压榨得奄奄一息。
这时候你满脑子都是“怎么把这个不等式再压紧一点”，很少再问：“我为什么非得证明这个 lemma？”
也许它太强了。也许坐标选错了。也许换一个定义，这三十页根本没有存在的必要。
Harrison 的故事让我想到的是：对问题的坚持，不等于对当前解法的忠诚。
当然，换方法不是凭空跳跃。旧路线的失败，会告诉你哪些障碍是偶然的，哪些是结构性的。十九年不是按下删除键就消失了，它们也参与塑造了后来那个判断。
这已经很接近我说的 intuition 和 motivation：一个帮助你判断“这里真正起作用的是什么”，另一个不断提醒你“我们究竟为什么在做这件事”。
Intuition：还没证明，为什么已经觉得它该成立？
我更愿意把 intuition 翻成“对结构的直觉”，而不只是“灵感”。
灵感听起来像天降一道闪电。数学直觉往往没那么戏剧化。它可能来自你算过的十几个例子、试过的几个极端情形、一个总是出现的对称性，或者某个怎么也绕不过去的不变量。
你还没有证明，但已经觉得：如果这件事不成立，背后一定有某个机制出了问题。
所以它更接近 Why should it be true?，而不只是拿到证明以后再解释一遍。
举一个很初等的例子：
$$ 1+3+5+\cdots+(2n-1)=n^2. $$
当然可以用归纳法。检验初始情形，再把下一项加上去，等式就出来了。
但如果你把一个点扩成 $2\times2$ 的正方形，再扩成 $3\times3$ 的正方形，会发现每次补上的都是一条 L 形的边。把边长从 $n-1$ 增加到 $n$，恰好需要 $2n-1$ 个点。
奇数不是碰巧加出了平方。它们就是正方形逐层长大时，每一层的大小。
这个图像既可以给你直觉，也可以组织成严格证明。它的价值不在于“比归纳法更不严谨但更好看”，而在于让式子里的对象发生了联系。你甚至会继续问：立方体逐层长大时，每层又有多少个小方块？
好的直觉不只解释一个答案，还会产生下一批问题。
不过，直觉会错。你看见的模式可能只活在低维里，你熟悉的有限情形可能根本不能推广到无限情形。证明的价值之一，正是逼你查清：哪些直觉是真的，哪些只是你太喜欢那个画面。
因此我说 intuition + motivation，绝不是说 proof 可以省略。证明不只是最后盖章的手续；寻找证明的过程，本身就在改造直觉。
Motivation：为什么偏偏问这个？
相较于“怎么证明”，我越来越觉得“为什么研究这个”更难教。
教科书往往先给定义，再给定理，再给证明。整齐得让人以为数学就是从第一行自然地滑到最后一行。
但研究现场经常反过来：先有一堆不太协调的例子，一个现有语言解释不好的现象，或者两套理论之间隐约相似的动作。然后你才开始摸索，到底应该定义什么。
为什么保留这个条件，扔掉那个条件？为什么要把这两个对象视为同一种东西？为什么要证明这个版本，而不是一个更容易、但什么也没说明的版本？
这些都属于 motivation。
这里的“值得问”，也不等于“能拿来干什么”。一个问题可能值得研究，是因为它暴露了现有理论的边界，连接了原本分开的领域，或者迫使我们发明一种更好的语言。
抽象就是一个典型例子。群的意义，不是把若干具体运算换成一套更吓人的符号，而是抽出共同的运算规则，让不同地方的对称性可以被放到同一种语言里讨论。
有些细节被丢掉了，反而有些联系第一次变得清楚。
所以问题选择、定义和抽象，并不是证明之前顺手完成的准备工作。它们本身就是研究。
一条定理证明了一个问题的答案；一个好定义，有时会改变我们接下来十年能问出哪些问题。
数学是一种压缩
如果只想增加真命题的数量，其实没那么难。
你可以不断写出具体的加法等式，也可以给一个已有定理添上不必要的条件，再宣布获得了新版本。数据库会越来越大，但没有人因此更理解数学。
数学里更有价值的进展，常常朝相反方向走：用更少的概念，组织更多的事实。
本来需要分别记住的几十种现象，忽然变成同一个结构的不同表现。本来只能逐题处理的计算，有了一套可以迁移的方法。
我说的“压缩”，不是论文页数更少，更不是越抽象越高级。把十页计算藏进一个看不懂的定义，未必压缩了任何人的理解。
真正有力量的压缩，应当让你更容易解释旧现象、预测新情形，也更容易看出方法会在哪里失效。
直觉给这种压缩一个可以操作的形状，动机决定我们为什么要压缩这些事实，证明则保证我们没有为了一个漂亮故事偷偷牺牲正确性。
三者是互相咬合的。这里的 intuition + motivation，是我想突出数学研究的重心，不是一份把 proof 开除出去的成分表。
Lean 改变了什么？
讨论 AI 做数学，有一个区别不能糊弄过去：生成一段看起来像证明的文字，和生成一份可以形式验证的证明，是两回事。
大模型完全可以很自信地写出“显然”，然后在这个词后面埋一颗雷。读的时候顺得要命，真去检查，发现它把最难的部分显然掉了。
Lean 这样的证明助手，提供了另一种工作方式：把定义、命题和证明放进形式语言，由内核检查证明项是否符合逻辑规则。人写的证明脚本，以及自动化策略，都要落实到可检查的证明对象上。Lean 官方 FAQ 解释了这一机制。
AI 可以提出候选步骤，调用现有引理，根据报错修改，再继续搜索。最终证明的接受，不需要取决于它说话有多像教授。
这条路线已经有实际成果。例如 2024 年的 AlphaProof，就在 Lean 中搜索证明，解决了当年 IMO 的三道非几何题。这是明确的能力进展，但竞赛题上的成功并不等于开放式数学研究已经被自动化。相关研究介绍见 Google Research。
形式验证也有它回答的问题范围。我们仍需要检查形式化的陈述是否忠实于原问题、使用了哪些假设，以及证明是否完整。验证器能检查的是：在给定形式系统和假设下，这个结论是否被证明了。它不会顺带认证“这个问题很重要”。
这不是 Lean 的缺点。它本来就不是一个数学品味检测器。
但它确实让一个设想变得具体：如果搜索能力持续增强，我们可能拥有越来越廉价、越来越可靠的定理生产能力。
那以后呢？
定理越便宜，理解越稀缺？
先把开头的思想实验说准确一点。我们不需要假设 AI 能证明字面意义上的“所有数学真理”，也不需要假设每个问题都能在某套固定公理下解决。
只需要假设：对大量人类关心、也确实可证的问题，寻找证明的成本大幅下降。
仅仅这样，数学研究的组织方式就可能发生很大的变化。
有些今天很值钱的技巧会贬值。有些人花几年才能清理完的技术障碍，可能变成一次调用。定理数量也会越来越难代表研究贡献。
这并不意味着那些证明没有价值。一个长期悬而未决的问题得到可靠答案，本身就是重大进展。哪怕证明很难理解，它也可能排除一条错误路线，成为后续研究可以放心使用的工具。
但“现在知道它成立了”和“现在理解它为什么成立了”，仍然可能相距很远。
如果 AI 给出一个极长的证明，我们接下来可能更想知道：真正关键的假设是哪一个？有没有更统一的表述？这个机制能不能迁移？原先那些零散的例子，是否终于有了共同解释？
这时候，数学工作的重心可能更多地转向问题选择、概念组织和证明的理解。
注意，我说的是这些工作会更突出，不是“这些工作一定归人类”。
前者是关于数学价值的判断。后者是关于未来能力分工的预测。两件事不能偷偷换着说。
别急着把直觉划成人类保留地
最容易写的结尾是：AI 只能证明，人类才有 intuition 和 motivation，所以人类永远不可替代。
可惜我不太相信这种保证。
人类的数学直觉也不是凭空出现的。它来自大量例子、反例、类比、失败经验，以及长期形成的结构判断。至少没有明显理由说明，机器原则上永远无法形成这些能力。
如果一个 AI 能发现新的结构，提出有解释力的定义，在陌生问题里迁移方法，还能准确预判某种推广为什么会失败，那么仅仅因为它是 AI，就说“这不算直觉”，多少有点临时修改评分标准。
Motivation 也一样。AI 完全可能学会判断哪些问题能够连接理论、澄清障碍、打开后续工作。这种研究判断，与它是否像人一样主观地“感到好奇”，不是同一个问题。
而且，人类的研究动机也没那么纯。好奇心、导师的方向、学界的风向、毕业要求，有时候还包括“这个估计比较容易发”。我们不必先把人类美化成一种只由求知欲驱动的生物，才能讨论机器。
当然，能写一段漂亮的动机介绍，不代表真的完成了这些工作。说“本研究建立了深刻联系”很容易，真正建立联系很难。评价应该看它提出的概念和问题能否经受后续检验。
所以，我不会把 intuition + motivation 当成人类最后两块永不失守的领土。
这是我对数学研究价值的判断，不是我对人类能力优势的担保。
即使 AI 理解了，我为什么还要理解？
再往前推一步。假设 AI 不但能证明，而且比我们更会选问题、更会抽象、更能看见结构。
那数学研究当然没有失去意义。它甚至可能发展得更快。
真正受到挑战的是：人类在其中做什么？
这里有两个经常混在一起的目标：让世界拥有某个知识，以及让我理解某个知识。
它们不是一回事。
世界上早就有人理解了微积分，这并没有自动让我理解微积分。一份证明已经躺在书上，也不等于我已经知道怎么用它、什么时候不能用它、该怎样把它和别的东西联系起来。
AI 拥有某种理解，同样不会让这种理解自动出现在我的脑子里。
如果我只需要一个结果，调用工具当然足够。没必要把每次查询都升级成精神修行。船员也不需要会制造航海钟，才能使用它。
但如果我想自己判断一个问题的表述是否合理、一个模型遗漏了什么，或者两个答案为什么冲突，就仍然需要足够的理解。这里的“自己”，也不是拒绝工具，而是能够参与判断，而非只能接收结论。
甚至在没有现实用途的时候，理解本身也可以是目标。那一刻发生的变化很具体：原本只能背下来的东西，现在可以推出来了；原本互不相干的现象，现在能看出联系了。
这不是安慰奖。但它也不能反过来保证，职业数学家的数量、评价体系和社会位置会维持原样。人类仍然有理由学数学，与人类仍然保有同样的研究竞争力，需要分开讨论。
真正值得期待的可能是：AI 不只把答案递过来，也帮助我们获得原本很难抵达的理解。它可以提供更合适的例子、把漫长证明整理成关键机制，或者把一种超出我们现有语言的结构，逐步翻译成我们能掌握的概念。
但这需要被当成一个目标来追求。“系统知道答案”不会自动等于“人类因此懂了”。
QED 之后，还有什么？
回头看《经度》，我不觉得那只钟能替我们回答 AI 与数学的一切问题。
工程实现和数学理解毕竟是不同的事情。但它们都提醒我：一个环节的成功，不会自动完成我们全部的目的。
知道时间差可以算经度，不等于已经造出了可靠的航海钟。验证一份证明，不等于已经看清它背后的结构。而即使某个系统看清了结构，也不等于我们已经理解。
所以，我说数学研究的本质是 intuition + motivation，最终想强调的是：
我们为什么问这个问题，以及我们如何理解它的答案，本来就是数学的一部分。
Proof 让判断站得住；intuition 让事实之间出现结构；motivation 让探索有方向。它们一起决定，一条正确的命题能否成为有意义的数学。
如果 AI 将来能把这些都做好，我愿意承认它在做真正的数学。没有必要为了保住人类的特殊性，一次次把“真正的数学”搬到机器暂时还够不到的地方。
但对我来说，数学里最想要的那个时刻，仍然不是屏幕上跳出一句“验证通过”。
而是看着一个原本完全不明白的东西，突然发现：
哦，原来它应该是这样。