2026年10月9日夜里,加州理工学院贝克曼礼堂涌进了上千名听众。这所学校的网页上至今仍列着一年前敲定的旧题目——《机器辅助证明》(Machine Assisted Proof)。可当当今数学界公认的旗手、菲尔兹奖得主陶哲轩(Terence Tao)登上讲台,他并没有照着稿子讲下去,而是把准备好的幻灯片整个推翻。屏幕亮出的新标题只有寥寥几个字,却透着对峙气味:Math 2.0。
台下所有人都明白,这位数学大家临时改题,与三天前刚刚震动整个数学圈的突袭直接相关。
72小时前的突袭:超700个开放难题、722份手稿被一次性抛出
时间往回拨到2026年10月6日。OpenAI事先没有发出任何预告,就在公开仓库里向外界倾倒出由模型自行生成的庞大成果。各家机构给出的统计互有差异,但都说体量惊人:被一次性作答的长期未解开放数学问题超过700个,随附722份学术文稿和大约372组前沿结果。

更关键的是其中很大一部分成果同时提供了Lean形式化语言写就的证明草稿,机器可以逐行核验推理步骤,并直接判定为“逻辑成立”。技术圈因此沸腾,有人喊出这是人类数学的“阿波罗时刻”。然而在纯数学圈子内部,弥漫开的是一种几乎让人喘不过气的压力。
几天之内,代表全球数学学者的人类数学协会(AHM)发表措辞尖锐的声明,强调数学家从未请求外界用这种方式去“解决”数学,把上百份机器生成文稿一口气送进学界,本质只是展示技术力量,与学术进展相去甚远。陶哲轩很快在自己博客上全文转载了这份抗议。
AI给出正确答案,数学家为何反而忧心?关键在于证明从稀缺变过剩
要看懂这场对抗,绕不开一个前提:纯数学恰好是算法最理想的游乐场。现实里的医学要靠漫长临床试验,社会学离不开抽样调查,自动驾驶得让雷达应付真实路面,而纯数学握有其他学科罕见的可客观验证属性——一份证明不是对就是错,它又高度数字化,完全由逻辑符号组成。
一旦资本与算力朝这个方向加力,陶哲轩所说的历史转折便轰然而至:人类结束了“证明稀缺”的岁月,被推进了“证明过剩”(Proof Abundance)的阶段。过去要攻下一道猜想,往往要赔上好几代人的青春与头发;现在只需把题目丢进算力黑箱,前沿模型就能批量生产出能被机器核验的定理。

但也正因如此,陶哲轩在幻灯片里打出一行让人警觉的话:“进一步只对解题做盲目优化,如今正在主动伤害数学的长期健康。”对于习惯唯分数、唯产出的人来说,这话近乎不可理喻,连一些硅谷人士也觉得,答案都已经给出,数学家难道是在闹脾气?其实他献出的比喻很简明:开放问题就像海面上的灯塔,它的价值是指路,而非抵达后便沦为终点。
这条推理有几百年例证作支撑。费马大定理出自十七世纪费马在书页留白处的猜测,其答案远谈不上惊世骇俗,但迫于求解它,此后三个世纪的学者不得不另造工具,硬是发展出现代代数数论、椭圆曲线理论以及模形式体系。那些摸黑走过的弯路、屡试屡败的挫折、半途中搜出的新概念,本身就是点燃文明的火把,最后那份答案只是被火把擦亮的一盏灯。
陶哲轩给出的警示是:要是今天人类靠机器直接乘着超音速直升机飞越整片迷雾、精确降落在灯塔之上,答案的确到手,可沿途原本会冒出来的新思想、深联结与人的直觉,将永不降临。过早依赖自动化抵达某一处,连带的后果是“让周围的整片领域变得贫瘠”(sterilize the surrounding field)。在Math 1.0中,解题原本是人们加深理解所用的代理指标;到了Math 2.0,当解题沦为廉价的算力消耗,这项指标就与研究的核心目标断开了。
他设计的思想实验:若AI配出一剂抗癌药却无人懂其原理,你敢静脉注射吗?
为了让非数学专业听众也能体会到那种悖论的恐惧,陶哲轩在演讲中描绘了一个假设:有一天,某顶级模型接到一句指令——“找出一种能通过三期临床试验的癌症疗法,并且绝不能出错。”消耗掉海量算力后,这个模型调制出一种此前闻所未闻的化学组合,它随附了缜密完整的形式证明,而临床上也如奇迹般通过了三期试验,的确杀灭癌细胞。

可现场没有一位人类科学家说得清它为何起效。模型给出的逻辑链错综冗长,没有人能看懂它作用的底层生理机制。陶哲轩追问在座者:假如此刻你被查出早期癌症,机器把这剂药送到你面前,在药液真正进入静脉之前,你难道不希望有位医生至少略懂它的药理?你怎能不怀疑,训练它的人只是在统计模型上寻得数学漏洞?
这张幻灯片流出后,社交平台上顿时炸开了锅。科技博主Andrew Curran当即反驳说:如果药真的有效,每个晚期癌症患者都会告诉你,他们根本不关心人类懂不懂机制。另有激进的AI追随者发帖嘲讽,称陶哲轩等人只是恐惧自己不再被视为世界上最聪明的人,是精英阶层的面子问题。而冷静的回击也随后登场,网友@_everythingism一针见血地指出:在黑箱语境下,就连潜在的长期副作用是什么都摸不透,贸然应用连安全使用的边界都合不拢。
纯数学这边还有严格编译器可以兜底,一旦这类“答案过剩、解释空缺”的范式扩散到医药、金融、军事跟工程中,一只不需要人类理解背书的“正确之手”,很可能正牵着某种看不见的系统风险。
“无信任协作”实验:33页手稿三周收工,德布罗因因子从20倍跌向1
需要说明的是,陶哲轩绝非抱残守缺的反对派。相反,他是全世界数学圈里拥抱AI最早、也跑得最前的人之一。在加州大学洛杉矶分校(UCLA)的一次访谈中,他用了很好懂的流体力学科比:人类传统做数学就像拧开水龙头,淌出一条细细的纯净可饮用水;机器更像一根消防员手里的高压水枪,在一瞬间喷射出大量无法直接饮用的浑水。形式化验证工具(例如Lean)就是滤水装置,负责挑掉杂质、只留可安全饮用的部分。

不仅构想如此,他早把想法投入实战。2023年年底,陶哲轩策划了一轮可以写进现代数学教科书的战役,主攻对象是多项式弗莱曼-鲁沙猜想(PFR)。按照传统学术圈的常规,顶级学者间的合作很难超过5人。这是因数学思考极为幽深,同伴间必须具备很长时间建立的互信,还得贴着原稿逐行验证校对对方内容。
陶哲轩打破了这条规则:他把一篇33页、艰深到一般人难以深入的论文,通过网络有向图拆成好几百条彼此独立的细碎引理;随后20多位分散在世界各地、以前从未见过面、水平高低不齐的数学家和程序员不声不响地自主申报任意代码分支。只要有人把代码写完,就直接送进编译器;Lean没有给出逻辑错误提示的话,那部分便会并入主干。陶哲轩无须评估提交者学术履历,甚至不必认识对方。这便是所谓“无信任协作”(Trustless Participation)。整个过程下来,一份足以被誉为世界级突破的33页成果,在三周内便被像工厂流水线一样拆解并验证完毕。
要是在以往,把纸面论文翻译为机器可读代码还要承受“德布罗因因子”(代码行数与论文篇幅之比)高达20倍的沉重负担;但现在搭载神经符号工具,这笔翻译成本正急剧滑落,已朝向比值为1靠拢。这恰是陶哲轩想像中的Math 2.0:数学领域要抛弃学者独立在象牙塔里的困守岁月,转型为像当代开源软件工程那样分布式分工的高效链条。
陶哲轩的路线图:脏活累活全交出去,但阐释可理解性不能外包
前沿学术机构和相关科研经费管理部门,其实已看到上述动向。跟着这场主题演讲,加州大学洛杉矶分校方面立即透露一项校级重点合作:在一项专项基金的扶持下,正式展开了规模达500万美元的联合攻关项目——ALPHA,由加州大学洛杉矶分校计算机系主任王伟领衔,联合陶哲轩等多位顶尖教授致力于神经符号自动化形式证明开发。这股重量较量的入场,意在给AI时代的人类科学建立一套无法被偷偷篡改、经得住验证的“事实基底”,相比较早期算出某一个学术命题,该项目本身的重要性要深远得多。

临收尾时,陶哲轩拿出一份务实又突破的演进时间表。他将研究方向分为两(及以上)等份的形式化:那种全无美感、繁琐演算沉重无比的粗活(如数论里枯燥单调的常系数推断),就大胆丢给模型进行一次性消费,人不必再把青春用来填坑;“公共库”如Mathlib并还属于人类精心打磨,应该保留那些带着审美趣味、能触发后续启迪的概念维度。与之相配合的,数学的职业激励制度也该随之动手术:奖励侧重从现在调向“开放阐释问题”(Open exposition problems),提高将深奥严格定理转化为直观漂亮的演绎展现奖格外。
幻灯最新的页脚一行给了一个有分量的宣言:要想赶向Math 2.0,最关键的不是算力和组织机构,也不是治学规章,归根结底在于人类能得有多远,能想到什么。
科学无论如何找出的都没法成某一无所不用其不知、人只需要低头服帖跪求的结果的“神谕”(Oracle)。穷极推理就是整个脆弱无用的人类天性也得凭着极狭小的大脑皮层面对无边寒冷的宇宙时,不回过头勾画出一个我们对这些所有一切的解释。而就答案填到能失去就丢放堆起在半间地时,“提问与研究探索”的追问相托。那么这里面最大半斤的话,谁可以替我门手里切切握出猜通的尊严的恰好唯有理解。
小结:OpenAI一次性公开的超700个开放问题的解法、722份手稿与跨域通过Lean机器核验的约372组结果,把数学系终归问押入“证明过剩”中;而陶哲轩借推翻原有胶片并提出Math 2.0以示警告:倘若只盲目把优化目标用在寻解上,再这样来系统性地推动会损伤数学全身。AI来助人往高攀的解释重要,但用明白的机制拿到沿途即所收获的视野才稍不觉缺席人类探求中那不可让度的部分。
