我不同意陶哲轩
最近，OpenAI 用内部尖端模型连放大招，证明了许多数学和计算机领域的前沿难题，证明的方法是将各种数学问题形式化1成 LEAN 语言，这种计算机语言可以自动证明复杂的逻辑关系。如果 AI 能够成功地用 LEAN 语言搭建一连串的逻辑桥梁，把原来的数学问题的起点和终点连接起来，那么这个数学问题就被严格证明了。
其实数学一直就是这么发展的。人们用 AM-GM 不等式证明了 Young 不等式，用 Young 不等式证明了 Hölder 不等式，用 Hölder 不等式证明了 Minkowski 不等式……每一步都是某几个人发现了现有积木的某种特定组合，组成了更大更好用的积木。
但是这一次不太一样，AI 为了在 LEAN 里证明一个数学结论，用 LEAN 编写了很多的中间步骤（就是上面说的逻辑桥梁），这些中间步骤的意义人们压根看不懂，而且很可能只有在解某道特定的题目里才有用。但无论如何，最后路走通了，于是数学问题被宣告解决。
这就好比 AI 造出了一辆新汽车，但是拆开一看，全部的零件都奇形怪状、目的不明，看起来也无法重用，但车的确能开得飞快。这算是汽车技术的进步吗？
如果我没理解错的话，以陶哲轩为首的「人类数学家协会」反对的就是这种暴力破解数学问题的方法。但是，他挑了一个远不及我给的很不恰当的比喻：
如果 AI 开发了一种治疗癌症的药物，临床实验证明非常有效，但是没有人懂得它的药物机理，你会选择注射到你的身体里吗？
……当然会啊！
为什么举例偏偏要选「癌症」、「药物机理」？在马斯洛需求金字塔上，数学是塔尖，生命是塔基。为了人命，「药物机理」恰恰是人最不在乎的东西。
那么刨去这个举例的瑕疵，我能不能支持陶哲轩的主张呢？作为一个拿了数学硕士，博士又是应用数学方向的人，我大概是能八成同理陶哲轩的感受。但是作为一个离开了学术界的人，不从既得利益的动机去揣测的话，我认为陶哲轩的主张非常荒谬2。国际象棋届没有抗议 Deep Blue 摧毁象棋，围棋届没有抗议 AlphaGo 摧毁围棋。数学的地位可能远高于棋类，但是性质是完全相同的。这点我觉得没必要反复捶打了，大家靠常识就能得出结论。菜农在菜地里插一块「禁止害虫」的牌子会有什么实际意义吗？
阻止 AI 涉足数学既然没有意义，那么 OpenAI 大规模扫题，把数学里许多的开放问题一下子解决了，这种做法是不是真的就会像陶哲轩说的那样严重影响数学的健康发展，让人们的认知断层呢？
我觉得就像历史上许多的范式转换（Paradigm Shift）一样，这类是非命题本身会变得无关紧要。数学领域一定不会被消灭，但是它本身的定义和游戏规会发生重大改变，以至于「明天的数学」可能与「昨天的数学」大相径庭，单说「数学发展」也会变得模糊不清。
数学家毕生追求的东西，说得俗一些，就是能够留下以自己名字命名的定理、理论。这是一个用智力赚取名声，顺便收获美的体验的行业。3因此，我们不妨就来分析一下 AI 对这两者的冲击到底有多大。
名声永远是一个人与人相比较的产物，与 AI 的存在无关。没有人类能够在棋类游戏中打败计算机，但人类的棋王仍然收获名声。挖掘机力大无穷，但人们看大力士比赛还是津津有味。同理，一个定理首先被 AI 证明，也并不表示没有数学家能够因此出名。第一个给出富有洞见的人类可读解释的人，也可能被后人冠名，只不过「诺特定理」这样的纪念碑在明天会变成「诺特解释」。我完全不担心数学家会找不到青史留名的途径。
再说数学之美，如果说 AI 给出的证明方法不可理喻，毫无美感，不就表示数学家想要开拓的数学之美仍未被挖掘出来吗？我以前做的数学习题，许多都是证明题，既然印在了书本上，那还没动笔就能知道肯定是真的，但这并不妨碍我认为有些结论非常优美。真和美在数学上既然是两回事，让 AI 处理真假，人类发掘美感，各尽其职，有何不妥呢？
最后想提一句，我很不喜欢「人类数学家协会」这样的组织，因为我认为他们试图代表的并不是「数学家」，而是「人类」。OpenAI 给出的 LEAN 形式证明，数学家觉得看不懂，不予接受，那 Poincaré 猜想的证明我也看不懂啊。凭什么某些数学家认为能看懂，就代表是人类可接受的——为什么数学家就能代表人类？我寻思着我也没投票派他们代表人类大战 AI 啊？如果说为什么陶哲轩的一句话引起我如此大的反感，就是这种自以为有资格代表人类的高傲吧。
不过想了想，我就一应用数学硕士，居然敢说陶哲轩没资格，简直太不要脸了。不过既然打了这么多字，删掉有点可惜，还是发出来吧。反正这就是我的随笔而已，不怕贻笑大方。