思维对撞机 · 第一期
当数学遭遇神谕机：从力学系宿命到格罗滕迪克的涨潮法
当 AI 在形式化系统上展现出超越人类的算力，纯数学象牙塔是否会重蹈力学系的宿命？在解题变得廉价的时代，重估格罗滕迪克的概念涨潮与人类心智尊严。
“数学中的理解，就像海水缓缓上涨。最初什么也没有发生，水面静谧而平稳；但在不知不觉中，坚硬的岩石已被完全淹没，不知不觉地软化、消解。”
—— 亚历山大·格罗滕迪克（Alexander Grothendieck），《收获与播种》
一、 消失的王冠：力学系的二十世纪宿命
在今天任何一所综合性研究型大学的理工科大楼里，你几乎都能捕捉到一个充满历史反讽的学科地景：百年前曾代表人类最高理性荣耀的理论力学，如今大多隐身在工学院的某个角落，或者退化为商业有限元仿真软件的底层参数配置。
回顾十九世纪末与二十世纪初，从牛顿、拉格朗日、哈密顿到庞加莱，力学曾是整个自然哲学皇冠上最璀璨的明珠。古典力学学者们不仅在黑板上勾勒天体轨道，更确立了人类理解因果律、守恒律与动力系统的哲学根基。
然而，二十世纪中叶计算机与有限元算法（FEM）的爆发，彻底终结了这一范式。当数以千万维度的刚度矩阵能够在服务器集群中数秒内求解，当湍流边界层可以用网格离散化暴力逼近时，传统力学系不可逆转地走向了工程化与工具箱化。人类不再需要冥思苦想一个偏微分方程的闭式解析解（Analytical Solution），计算的冗余吞噬了洞见的尊严。力学从一门探索宇宙本质的本体论科学，变成了一套极其好用、但也极其冰冷的计算管道。
Warning
历史的镜像与范式危机
今天，在 AI for Math 与交互式自动定理证明（Lean / Isabelle / Coq）席卷而来的黄昏，一个让所有纯数学家脊背发凉的幽灵正在浮现：纯数学——这一人类思维最抽象、最纯粹、拒绝任何功利目的的最后圣殿，是否正在重蹈力学系的宿命？
二、 两次受挫：四色定理与开普勒猜想的“神谕机”幽灵
纯数学对机器计算的警惕与创伤，并非始于今日的大语言模型，而是深植于半个世纪以来的两次标志性公案。
1. 1976 年四色定理：失去美感的初夜
1976 年，肯尼斯·阿佩尔（Kenneth Appel）与沃尔夫冈·哈肯（Wolfgang Haken）宣布证明了沉寂百年的“四色猜想”。然而，这一证明并未在数学界引发狂欢，反而激起了巨大的沮丧与哲学震荡。他们将平面地图的无限种可能拓扑归结为 1,936 种不可约配置，随后调用伊利诺伊大学的超级计算机，运行了超过 1,200 个小时进行暴力穷举检验。
这是人类数学史上第一次无法由人类同行用纸笔完成验算的著名定理。著名数学家保罗·哈尔莫斯（Paul Halmos）曾对此发出哀叹：“这是一个计算机的证明，而不是一个数学家的证明。” 它给出了“是”的冷酷判决，却没有给人类大脑留下哪怕一丝对拓扑对称本质的审美愉悦。
2. 1998 年开普勒猜想：审稿人的集体投降
二十二年后的 1998 年，托马斯·黑尔斯（Thomas Hales）对开普勒猜想（三维空间中最致密堆积球体的方式为面心立方或六方密堆积）给出了计算机辅助证明。这个由 250 页论文和超过 3GB 程序代码与数据组成的庞然大物，被提交给了数学界顶尖期刊《数学年刊》（Annals of Mathematics）。
由普林斯顿高等研究院领衔的 12 位世界级审稿专家委员会，在长达四年的闭门研读后宣布集体投降。评审团主席罗伯特·麦克弗森（Robert MacPherson）最终发表了一份前所未有的官方声明：
Important
审稿专家团的划时代声明（1998）
“审稿团队确认黑尔斯的策略在方向上是正确的，且对其正确性抱有 99% 的确定性；但由于机器代码与离散分支的不可穿透性，人类数学家无法担保其中不存在细微漏洞。”
这一空前危机最终逼迫黑尔斯发起了著名的“Flyspeck 计划”，花费整整十二年，将全部推导翻译为计算机形式化检验系统（HOL Light 和 Isabelle）。猜想确实被证实了，但在这一过程中，传统的同行评议机制宣告实质性破产。
三、 现代神谕机：陶哲轩的折中与理解的断崖
进入 2020 年代，以菲尔兹奖得主陶哲轩（Terence Tao）为代表的先锋数学家，正极力倡导将 Lean 等交互式形式化工具融入日常研究。陶哲轩指出，面对现代数学大厦越来越庞大、子分支高度隔绝、论文动辄数百页的现状，人类大脑的生化工作记忆（Working Memory）已经逼近生理极限。
形式化证明像是一套“工业外骨骼”，它能够接管极其繁琐的引理验证，防止人类因漏看一个退化边界而全盘崩溃。
但这里潜藏着图灵（Alan Turing）早在 1939 年就提出的致命概念——神谕机（Oracle Machine）。
神谕机是一个黑盒，你向它输入一个命题，它能以绝对确定性输出答案：真，或者假。
Note
维特根斯坦式“认知停滞”（Cognitive Stagnation）
假若未来十到二十年内，基于强化学习与形式化内核的混合智能系统，在数秒内输出了黎曼猜想（Riemann Hypothesis）的证明，但输出的是长达一千万行的非结构化 Lean 代码——其中充斥着数亿次人类无法追溯的拓扑微扰。此时：
- 命题被证明了吗？ —— 毫无疑问，逻辑与语法无懈可击；
- 人类理解了这个命题吗？ —— 完全没有。
如果真理的获得不再需要洞见（Insight），那么数学探索就彻底退化为了机械的数据挖掘。数学家将不再是普罗米修斯式的真理盗火者，而沦为神谕机终端前的仪表盘抄表员。
四、 涨潮之海：格罗滕迪克的遗嘱与数学的尊严
面对计算暴力与神谕机的步步紧逼，二十世纪最伟大的代数几何学家亚历山大·格罗滕迪克（Alexander Grothendieck）在《收获与播种》中留下的隐喻，成为了人类数学精神最坚固的灯塔。
格罗滕迪克曾将数学攻坚分为两种截然相反的哲学态度：
“面对一个坚硬的坚果，一种做法是拿一把锤子和凿子，对准外壳猛烈敲击，直到把它砸得粉碎；
但我的方式是让海水慢慢上涨。海水包围着坚果，不知不觉中，海平面上升了几米、几十米。坚果在海水长时间的浸润下自然软化。终有一天，当微风拂过，坚果的外壳会自己脱落，核心就那么安静地躺在那里。”
格罗滕迪克创造概形（Schemes）、层（Sheaves）、意象（Topos）与基模（Motives）的宏伟世界，绝非为了快速求出某一个具体方程的数值解，而是为了建构概念的宏大框架。在他的视野里，一个真正高贵的数学证明，应当像日出一样自然：当你把周围的代数拓扑空间理解得足够透彻时，那个原本被视为天堑的猜想，不过是这个高维世界里一条显而易见的平坦小径。
神谕机永远擅长“锤子与凿子”——它拥有人类无法企及的算力和极快的敲击频率，它能在几微秒内敲击数十亿次，把最坚硬的胡桃砸个稀巴烂。
但神谕机不懂得涨潮。 它无法体会概念之间那种如同诗歌般的和谐感，无法感知一个范畴到另一个范畴之间对偶性的崇高之美，更无法理解人类在洞悉宇宙结构时那一瞬间的顿悟与战栗。
五、 结语：在神谕降临的黄昏，重估人类的“无用之用”
如果数学最终也像力学一样，其计算与推导职能被机械完全剥离，人类数学家究竟还剩下什么？
答案或许正是庄子所言的：
Tip
思想的锚点：无用之用，方为大用
在工科与应用科学的视界里，有用的才是真理；但在人类纯粹理性的疆域里，只有超越功利的目的，才能定义文明的高度。
我们推导数论、探寻可数与不可数无穷大、构建高维奇异流形，从最初就不是为了造出更快的主干网路由器，或者更高效的机翼流场。我们之所以做数学，是因为这项智力活动是人类意识与浩瀚宇宙之间唯一共通的语法。
神谕机可以赐予我们无尽的定理，但唯有人类才能赋予这些定理以意义。只要人类还在渴望理解而非仅仅渴望答案，格罗滕迪克的那片潮汐，就永远不会在数学的海岸线上褪去。