若全宇宙只有 AI 懂证明，数学便毫无意义——当机器接管推演与代码

一位数学研究者花了几个月琢磨难题，好不容易理出一套向同行讲透的优美逻辑；另一位借助 AI，几杯咖啡的工夫就导出了全套形式化推导。对于在高校搞过科研、如今置身工业界 AI 工程一线的同行来说，这种反差毫不陌生：一边是资深架构师反复推敲并发模型、手撕底层核心状态机（在机器学习中则是死磕数据质量与显存边界）；另一边是用 AI 生成数千行代码、单元测试瞬间全绿的狂飙突进。如果两套结果在本地都挑不出毛病，后者在交付效率上无疑大获全胜。

但如果我们接着追问：谁能解释推演背后的机理？线上系统突发高并发死锁或模型异常时，谁敢去触碰那堆无人理解的逻辑？在过去，“解题”与“理解”是天然绑定的；然而生成式 AI 正在强行切断这种对应关系：系统可以先交出毫无瑕疵的符号或代码，人类却必须花几个月甚至几年去反向猜解机理——这种反差，恰如传统工匠数年如一日打磨深厚内功，与黑盒流水线追求秒级交付的戏剧性碰撞。

大家更关心的是：当答案与代码的生产速度远远甩开了人类消化吸收的速度，我们究竟该用什么来衡量知识与技术的真正进步？若全宇宙最终只有一台黑盒机器看得懂证明、排得清故障，这项成果究竟是在拓展人类的文明疆域，还是在制造空心化的数字遗迹？

一、 从生成到交付：为什么表面提速变成了核验灾难？ #

讨论 AI 在数学与工程中的介入时，我们需要理清三个完全不同的动作：生成结果、核验推导、理解机制。它们环环相扣，却绝不能相互替代。

模型可以生成一段看起来无懈可击的高维推演；数学家或形式化工具可以逐行检查每一步是否符合公理；但研究者真正的核心工作，是提炼这套方法背后的思想骨架，解释它为什么有效，以及它如何嵌入人类已有的理论体系。

自然语言写出的证明，常常把最致命的逻辑漏洞伪装成“显而易见，同理可得”。形式化验证（formal verification）固然能在机器规则下保证逻辑链条严丝合缝，但工程师和研究者都明白： “编译通过、测试全绿”和“业务逻辑正确”完全是两码事。 我们依然要追问：形式化之后的命题，有没有悄悄偏离最初的问题本质？边界条件有没有被悄悄放宽？这就好比机器向你证明了“大象完全可以装进冰箱”，程序员仔细审视底层代码，才发现它为了让单元测试通过，在底层把冰箱的体积偷偷定义成了无穷大，甚至顺手把运行超时和报错全部静默吞掉了。

数学家邓煜曾提出了极具洞察力的 “数学双重边界理论”（Dual Boundary Theory of Mathematics） [2]。在人类探索未知的坐标系中，始终存在着两道分明的边界：

• 第一道边界是 “客观上存在严格逻辑证明或可行实现的问题” ；
• 第二道边界是 “人类心智能够真正理解其背后机理的问题” 。

在古典科研与传统工程时代，这两道边界高度重合——一项难题被宣告解决，必然伴随着人类直觉对系统全链路的透彻掌握。然而，高阶生成式 AI 的介入，正在这两道边界之间粗暴地撕开一道深不见底的断裂带[2]。算法可以在高维空间中进行海量试错与符号拼接，将“已被证明/已生成”的第一道边界以惊人的速度向外推移；但如果这些复杂的符号序列无法被人类消化，第二道“被理解”的边界就会停滞不前。

正如陶哲轩与邓煜在访谈中所直击的核心命题：科学探索与架构创新的终极价值，从来不是孤立地搜集由黑盒判定的“真命题切片”或堆积无人敢改的代码黑盒，而是增进人类对抽象世界与物理现实的深刻理解[2]。若全宇宙只有一台冰冷的机器知晓推导逻辑与系统底细，而整个人类文明对其机制一无所知，这无异于全天下学者与工程师沦为只能点按回车键的符号搬运工，所谓的“技术突破”对人类心智并无实质意义。

面对 AI 的角色定位，菲尔兹奖得主陶哲轩打过一个精妙的比方： AI 就像汽车 [2]。汽车的时速固然远超人类的双腿，但汽车的发明绝不意味着人类应当放弃行走。我们依然需要用双脚去丈量大地、保持生理肌体的强健，并在徒步中保持对风景的敏锐感知与审美体验。数学研究与系统设计同样如此：我们可以坐上算力的快车去往更远的目的地，但概念的深耕、架构手感的打磨与对本质之美的体会，必须由人类心智亲自完成[1][2]。在健康的人机协同中，邓煜将 AI 定位为 “计算的脚手架”（computational scaffolding） [2]——人类核心设计者统领宏观蓝图与路线，把局部繁琐、耗时的代数暴力推演交给 AI 完成，大厦落成之后，真正挺立的是建筑本身的力学平衡与空间审美，脚手架绝不能喧宾夺主。

做模型研发与 MLOps 的工程师同样深谙此道。假设 AI 助手为你生成了一套端到端的多模态表征或时间序列预测管道，离线评估指标全面秒杀历史基线。有经验的工程师绝不会直接欢呼推向生产，而是会立刻警惕起来：特征库（Feature Store）里有没有混进包含未来答案的时间戳从而发生隐蔽的数据穿越（data leakage）？样本分布中是否潜藏着严峻的过拟合与对齐失真？线上离线一致性（train-serve skew）是否经得起真实流量检验？模型在长尾极端场景（edge cases）下是否暗藏灾难性遗忘？

然而，一个人在生成端省下的时间，往往会成倍放大为后续整个团队和学术共同体的核验负担。一篇论文不是扔进预印本平台（preprint servers）就万事大吉了，它需要同行读懂脉络、寻找反例；一段业务代码也不是 git push 到仓库就算完事了，它需要经过严格的架构审查、容灾演练，并长期接受生产环境的考验。

2026 年 10 月 6 日，OpenAI 在其公开仓库中批量发布了多达 722 篇由内部前沿模型生成的数学手稿（涵盖 370 多个结果家族），瞬间引爆了学术界的震动[2]。商业机构为了展示其通用推理与 AGI 突破，在极短时间内向学术界抛出海量未经同行评议的半成品证明[2]。这些手稿乍看公式密布、符号严谨，细究之下却漏洞百出：不仅存在大量正负号颠倒、关键引理偷换的低级错误，甚至还出现了正文自然语言推导与配套形式化验证代码（如 Lean 代码）严重脱节的荒诞乱象，部分预印本在发布后数十小时内便因硬伤不得不撤回[2]。

这在软件工程界有一个人人恨得咬牙切齿的对标物： “甩手掌柜式代码提交” （Dump-and-Run PR）。有人用 AI 一键生成了数千行缺乏架构设计、未处理并发边界的代码，然后在群里提醒所有人：“我今天产出了 5000 行核心代码，大家抓紧 Review 一下”。在 AI 工程中也有类似的身影：用 AI 一键拼凑出一套端到端的复杂训练脚本，在小规模 Demo 上跑出亮眼指标就急着宣称 SOTA，随后把线上高延迟、显存溢出与不可复现的维护重担全部甩给工程团队。

陶哲轩在访谈中尖锐地指责这种做法宛如向公共学术生态倾倒 “有毒副产物”（toxic waste） ——商业机构仅仅将攻关未解难题当作测试通用大模型能力的训练靶场，却把全球顶尖数学家与资深工程师强行降级为给黑盒产物筛查排毒、收拾残局的“免费 Debug 质检员”[1][2]。更深层的危机，还在于对“唯答案论”（answers-only metric）的单一指标崇拜，以及斩断引文链导致的知识产权与学术伦理争议[2]。一个必须确立的行业共识是： 谁利用 AI 获得了高速交付的红利，谁就必须承担起让别人能验证、能读懂、能维护的连带责任。 “这是模型跑出来的”，绝不能成为免责甩锅的护身符。

二、 没有发明新范式，机器的“野路子”算不算知识？ #

面对铺天盖地的机器产出，一种常见的防御性姿态是：AI 只不过是在人类划定的规则迷宫里做暴力搜索，只有人类才能创造概念与知识范式。

这种想拼命守护人类智慧尊严的心情可以理解，但这种反驳把“创造知识与技术突破”的门槛定得实在太脱离现实了。

如果我们要求每一项科研产出都必须开天辟地、颠覆既有范式，那就像要求每个进厨房的厨师都必须先从“重新定义热力学定律和人工合成蛋白质”开始，否则煎个蛋都不配叫烹饪。科学大厦与工业软件的大多数进展，本来就是在既有框架里修修补补——找到一个关键反例、将某个不等式的常数界限再收窄一点点、优化一个局部算子的锁竞争、设计出一套更精妙的离散算法构造。如果人类学者与工程师做这些工作被称为推动技术进步，我们就没理由仅仅因为推导路径来自算法搜索，就酸溜溜地全盘否认其价值。

DeepMind 的 FunSearch 就是一个极具说服力的切口。研究人员将大语言模型（Large Language Models，LLMs）与程序评估器（program evaluator）拼在一起，模型负责疯狂试错写代码，评估器负责打分筛选淘汰。在经典的 cap set 问题（cap set problem）中，它在极其逼仄的空间里找到了前人未能构想出的点集排布；在在线装箱（online bin packing）中，它同样找到了全面超越通用基线的高效启发式算法（heuristic algorithms）[3]。

在准黎曼猜想（quasi-Riemann hypothesis）的推进中，OpenAI 在其 10 月手稿中声称给出了实部大于 \(7/8\) 的无零点半平面（尽管正文论文与目录索引在 \(7/8\) 与 \(11/12\) 之间存在数字出入）。虽然学界目前仅将其作为“假设其成立”的未独立核实前提出发点，但陶哲轩依然务实地指出，\(7/8\) 距离黎曼猜想真正的核心死穴 \(1/2\) 仍有很长距离，现存方法也撞上了明显的理论天花板[1]。

这些进展结结实实地证明：在人类既定的规则空间里搜索，同样能砸出货真价实的科学与工程增量。在 SAIR 的深度对话中，邓煜由衷赞叹道：单看这些机器输出的推演，它们“非常了不起，里面包含着很美的新想法，而且我们确实能读懂”；陶哲轩也坦言其中有约十个悬而未决的问题引起了他本人的强烈兴趣，后续会专门研读[2]。

正是在这种既充满惊喜又伴随困惑的交织中，一个极其传神、也耐人寻味的视角浮出水面： AI 搞数学与底层算法研究，总让人联想起“文盲修仙”的野路子。

所谓 “文盲修仙” ，是指它大字不识一个，根本不懂高维流形、分布式共识协议背后的深邃心法，更谈不上对宇宙真理或系统美感有什么直觉共鸣。然而它架不住力大砖飞、蛮力通神——凭借天文数字级的参数与高维概率统计，照着形式化公理规则一通疯狂比划试错，居然真在万仞绝壁之上摸索出了一条反直觉的悬崖野路，每一步都险象环生却奇迹般地没掉下去，硬生生轰出了连名门正派宗师与资深架构师都未曾设想过的神来之笔！

工程师对此绝不陌生：当你排查一个深不见底的并发死锁时，有人直接向 AI 盲猜求得了一个神秘的补丁（比如把某个线程池队列长度调成了一个奇怪的固定参数，或者加了一行微秒级延迟），线上报警瞬间消停，测试全部跑通！在如今的大模型微调与工程调优中同样如此：随手从网上抓来一段神秘参数或魔改的配置，报警看似没了，但谁也说不清机理何在。这就是典型的“工程版文盲修仙”——知其然而不知其所以然。一旦流量翻倍、环境变化或上下文拉长，这个未被真正理解的野路子补丁就会化身为更致命的午夜 P0 级特大事故。

“文盲修仙”最大的死穴，在于它自己无法传道，更开创不出通用心法。如果名门宗师跑过去问它：“道友，你刚才这记精妙绝伦的连招到底暗合了哪门天地法则？引气脉络是什么？”它只能交出一堆毫无生命的浮点数权重，本质上脑中一片空白。

这时，人类数学家与核心工程师真正的硬核价值就无可替代地显现出来了： 他们必须充当那群给“文盲修士”整理正统心法的大宗师。 专家学者拿着放大镜和显微镜，将机器误打误撞轰出的野路子逐帧反向工程，破译其中暗藏的数学机制与系统深层对称性，最终将这套反直觉的泥泞小道，拓宽成天下学者与开发者皆可通行、皆可继承的康庄大道。

成熟的学术与工程讨论必须重返务实尺度：结果对不对？增量新不新？它是否拓宽了我们解决具体问题的边界？更关键的是，我们能否从机器探出的灌木丛里，修剪出人类智慧可以继承的通用方法？人类的理解往往滞后于机器的发现，我们不必苛求每一个机器输出在落地的第一天就具备教科书般的从容优雅，但也绝不能将高维搜索撞大运的命中本身，误认为是知识生产与工程智慧的全部。

三、 面对商业黑盒垄断，学术界如何展开制度自救？ #

面对商业大模型未经审慎核验的成果涌入、引文溯源困难与黑盒垄断风险，数学共同体并没有止步于道义谴责，而是迅速掀起了一场深具历史眼光的制度性自救。

对于广大工程师而言，这场自救再亲切不过了——它几乎完美重演了软件工程史上最波澜壮阔的开源反抗史：当年商业 Unix 的闭源垄断激发了 Linux 与 GNU 自由软件运动；商业专有工具 BitKeeper 授权的收回与集中式管理的困境促成了 Git 的诞生；公有云巨头的专有 API 绑架催生了 Kubernetes 与开放的云原生基金会（CNCF）；如今面对闭源商业大模型的垄断，PyTorch、vLLM 等开源 AI 生态也同样挺身而出。开源社区永远的信条是： “Talk is cheap, show me the code / proof.” 基础科学与通用计算的底层协议，决不能被任何商业寡头的黑盒暗箱所永久劫持。

科学从四百年前诞生之日起，其基石就是“可公开检验、可自由复现、可透明继承”的开源哲学。正是在这种学术公地危机的触动下，早于 2025 年创立的 SAIR 基金会（Foundation for Science and AI Research） [2]，联合全球顶尖高校与独立学者，加速推进了学者自主的开放数学体系。陶哲轩指出，10 月份的大模型手稿风波并未让他们从零起步，而是促使学界将原本规划在数月后发布的 Open Math OS 操作系统脚手架紧急提前[2]。

既然要探索未知，驱动工具的内核就必须向全天下公开。SAIR 打造的科研协作网络，核心在于构建去中心化、透明可溯的开放研究基础设施：

• 基于开源权重的透明推理系统 ：打破商业黑盒的暗箱机制，让模型的推理逻辑在阳光下接受同行评议，消除科研人员输入未发表构想时的版权与安全焦虑[2]。
• 形式化验证环境（如 Lean）的原生融合目标 ：将大模型的高维发散与形式化系统的冷酷严谨深度绑定，从源头上杜绝“正文写一套、代码挂羊头卖狗肉”的虚假繁荣[2]。
• 全流程透明溯源与引文追踪倡议 ：面对大模型统计混合导致的句子级引理归因难题，学界并非盲目要求模型承诺完全精确的逐行归因，而是推动在算法底层建立起包括工具调用记录、检索追踪日志、形式化证明产物在内的全流程可复现标准[2]。

平心而论，开源权重本身并不能自动解决可复现性或审计难题，商业闭源模型在算力规模、系统级安全沙箱与企业保障上亦有其不可替代的工程优势。学界自救的核心，并非对商业生态的全盘否定，而是要捍卫基础科学与开放研究的透明底座，避免科学真理的解释权与工具链被单一封闭暗箱所垄断。

四、 算法会让人变钝吗？未来探索者的心智与训练 #

知识生产与系统工程还有一个经常被效率数字遮蔽的隐形使命： 它在产出论文与系统交付的同时，顺带完成了对下一代探索者与工程师的打磨。

一个年轻学生在台灯下推导经典公式，绝不是为了向人类知识宝库再塞进一条早已盖棺定论的定理。他可能会把充分条件和必要条件搞混，沿着死胡同硬推了两整页草稿，最后才懊恼地发现假设用反了。这两页废纸没有任何发表价值，但正是在这一次次撞墙的狼狈过程中，他建立起了对逻辑边界的敏锐警觉。工程师愿意花几天时间手写一个成熟开源库早已存在的底层轮子（比如手写内存池、手撕 B+ 树索引，或手推一遍反向传播、手写注意力计算），从来不是为了重复发明，而是为了在大型分布式系统突发故障或模型训练遭遇诡异异常时，能凭借肌肉记忆和直觉秒级锁定病灶。

在传统学术传授或工程传承中，一个新手如果连最基础的推导与原理都没搞明白，一上来就直接依赖黑盒工具一键生成，看似一日千里，实则根基虚浮。Ben Antieau 在陶哲轩博客发表的客座文章《Fast math/slow math》中深刻指出：慢思考与反复咀嚼是科研不可或缺的灵魂，AI 辅助研究的终极目的应当是增进人类的理解，而不只是拼命冲刺论文产能[4]。陶哲轩也直言其隐忧：难度适中的“中等练习题”是青年学者与初级工程师成长的黄金摇篮，如果学者们一遇到有点挑战的小问题就转手丢给大模型并把答案秒级公开，年轻一代将失去大批用来积攒手感、建立自信的练兵场[1]。

更值得警惕的是工具对成熟心智的重塑。一项发表于 CHI 2025、覆盖 319 名知识工作者与 936 个真实任务的实证研究表明：在剔除任务难度与用户差异后，使用者对 AI 的信任度越高，其自我报告的批判性思考（critical thinking）频率就越低；脑力往往从底层的深度构思，悄悄挪向了核对信息、拼凑答案和监督进度等事务性环节[5]。

现代软件工程本就建立在层层抽象之上——很少有工程师能完全背出硬件微架构的乱序执行细节、编译器的极致优化路径或操作系统底层的锁竞争实现。但工程文明之所以没有崩塌，是因为我们在每一层抽象之间都保留了清晰的规范契约、可审计性、可干预性与故障隔离边界。算法可以在既定的轨道里凭借惊人的算力跑出超乎想象的距离，但它缺乏人类对真实世界风险与系统健壮性的审美直觉与责任担当[2]。 提出直击现实核心的高维新命题、设计跨越数个学科的宏观蓝图、在复杂的商业变局中权衡技术取舍并坚守架构底线——这些战略层面的审美品味与宏观判断，依然是人类心智独占的圣殿[2]。

这正如车里的 GPS 导航：心中有路网格局与地形感知的人，用它实时避开拥堵路段；而彻底放弃记忆与方位感知的人，哪怕导航语音叫他立刻右拐开进人工湖，他也会毫不犹豫地把方向盘打死。

一个行之有效的自省标尺或许是： 如果突然拔掉网线、关掉 AI 助手，只留下一块黑板和一支粉笔（或者一个纯文本终端），我们能否向讲台下的学生把刚才推导中最精妙的逻辑转折解释得一清二楚？能否向工程团队清晰阐明整个系统的数据流向与并发边界、讲透模型在什么边界下会失效？一旦外部环境或输入参数发生微调，能否一眼看穿原有的结论将在哪里失效？ 如果答案是否定的，那么眼前的工具只是制造了一场高产的假象，真正的判断力，其实从来没有被真正掌握。保护训练的土壤，真正需要重构的是考核靶心——考核失效条件、单点故障与机理解释，而非仅仅评估最后格式工整的文本或代码 PR[2]。

五、 走出产量狂欢之后，我们究竟该用什么衡量进步？ #

当 AI 能够以远超人类的速度生成证明、代码和模型时，真正的进步不能再仅由“是否得到答案”来衡量。一项成果值得被接纳，至少应满足四个条件：它提供了经得起逻辑检验或生产环境考验的有效增量；它能够被解释、复现并沉淀为他人可复用的方法；其从生成、验证、审查到维护的全周期成本是可核算的；参与者在过程中形成了独立判断力，而不是把理解外包给工具。

换言之，AI 可以扩展我们能证明和能实现的范围，却不能自动扩展我们能理解与传承的范围。若一个证明只有机器能检查，一段代码只有原作者敢改动，一个模型只有离线指标漂亮却无人能说明其失效边界，那么它带来的更可能是短期产出，而非长期知识资产。

因此，问题不是要不要使用 AI，而是我们是否仍愿意为理解付出成本：能否脱离工具解释关键推理，能否识别系统在何种条件下失效，能否把一次偶然的成功转化为可教授、可审计、可继承的方法。答案可以由模型快速生成；但判断其价值、界定其边界，并将其纳入人类知识体系的责任，仍然必须由人来承担。

参考文献 #

[1] Numberphile. No More Heroes - Terence Tao Talks to Numberphile About AI. YouTube, 2026-10-15. https://www.youtube.com/watch?v=bAnwMdfcMVw

[2] SAIR. Terence Tao & Yu Deng: Why We Build Open Math Model. YouTube, 2026-10-19. https://www.youtube.com/watch?v=TjeCcDkuyao

[3] Romera-Paredes, B., et al. Mathematical discoveries from program search with large language models. Nature, 625, 468–475, 2024（2023 年在线发表）. https://doi.org/10.1038/s41586-023-06924-6

[4] Antieau, B. Fast math/slow math. What’s new, 2026-09-15. 陶哲轩博客客座文章. https://terrytao.wordpress.com/2026/09/15/fast-math-slow-math/

[5] Lee, H.-P., et al. The Impact of Generative AI on Critical Thinking: Self-Reported Reductions in Cognitive Effort and Confidence Effects From a Survey of Knowledge Workers. CHI 2025, Article 1121, 1–22. https://doi.org/10.1145/3706598.3713778

[6] 深度解读与访谈. 若全宇宙只有AI懂证明，数学便毫无意义. YouTube, 2026. https://www.youtube.com/watch?v=jFAo9vRV2dE