ARTICLE · 1128613
数学家心声:《定理经济的陨落:AI何以几乎毫发无损地摧毁数学》by David Bessis 2026-4-21
“数学的成果是明晰与理解，而非单单那些定理本身。”
——比尔·瑟斯顿
亚历山大·格罗滕迪克的手写示意图
我最出色的一条定理，我从来没有正式写出来过。在瑞士洛桑，一个明朗的清晨，当时我正在准备自己最后一场受邀会议报告，这个想法彻底成型。这条定理的证明看上去无比显然，结论又十分有说服力，于是我冒失地在最后一刻修改了幻灯片。时间已经很紧张，我只能把这条结果作为一句非正式的备注，写在最后一页幻灯片底部，而不是把它写成一条规范完整的定理¹。
彼时我已经离开学术界，创办了一家机器学习初创公司。我心里清楚自己会忙得抽不出时间整理一份干净的证明并正式发表。这就成了我敷衍了事的借口。我只写下那句备注，把这份幻灯片文稿弃置一旁，如同往大海中投出一只漂流瓶。
我曾经期盼，未来会有某位才华横溢的年轻数学家发掘它，把这条结果形式化，纳入一套更宏大的理论框架。如果运气好，在学术归属的种种偶然之下，它或许还会被后人称作“贝西斯胞分解定理”。
但这种想法实在幼稚。我一旦对外宣告了这个结果，其他人动笔整理成文的动力就荡然无存了。
如果要选出我第二满意的成果，那就是我旧预印本里加尔赛德范畴（Garside categories）下的定理0.5。我对这篇文章寄予很高期待，可我最终没有把它投给任何期刊。整个创作过程耗尽了我的精力，还没鼓起勇气把预备部分打磨完善，我就已经离开了一线研究。
作为第二出色的结果，这条定理证明起来却出奇简单。只要把预备铺垫工作处理妥当，只需要寥寥数页十分常规的群论推导即可完成。
至于那些预备铺垫，难度甚至更低。你只需要研读十几篇冷门子领域加尔赛德理论的经典论文，把原有公理体系替换成一套略具一般性的公理。只要你清楚目标要做什么，几乎不会遇到实质性阻碍，本质就是一次大规模概念层面的查找替换编辑。但这一点你只能相信我的一面之词，我实在不愿动笔写出那几百页必需的细节内容。
如果你觉得数学家的核心工作就是证明定理，那这个例子恰恰可以反驳这种看法。从我构思出定理0.5那一刻起，我就知道它是成立的，证明过程也会顺理成章。
那么真正的难点究竟是什么？是猜想出精确的命题并把它写下来吗？也并不是。在这个例子里，这一步同样并不困难。
真正的难点，是凭直觉意识到应当存在“类似定理0.5这样的东西”，并且搭建出一套概念框架，让这个命题可以简洁地表达出来。一旦定义设置妥当，其余内容就会自然而然地随之生成。
数学研究并不总是如此，但的确会有灵光迸发的日子：就好比你踩上滑雪板，转眼间就顺着山坡飞速向下。
让‑皮埃尔·塞尔（Jean-Pierre Serre）有一句广为流传的话：撰写那篇关于凝聚层的开创性论文时，他几乎不需要苦思冥想；一切都顺理成章，仿佛打字机自己就输出了上百页文稿，仿佛这篇文章本就早已存在。
可我不是让‑皮埃尔·塞尔，他也不肯把打字机借我用。这就是为什么我最闪光的数学想法始终没能正式发表。
我会为此感到难过吗？倒也不会。我的预印本依旧公开挂在arXiv上，已经被几十篇文献引用，其中不乏不少高水平论文。真正的创新点并不是定理0.5本身，而是支撑它的那套语言体系，尤其是定义2.4与定义9.3。这套概念语言后来被写进一部七百多页的加尔赛德理论专著，书中补足了大量缺失的预备内容。
说实话，我搁置这份最具创新性的预印本，也有一点私心。这样我就可以把精力投入另一篇更加繁琐的预印本工作：借助定义9.3作为关键工具，解决我所在领域的经典猜想——有限复反射群的𝐾(π,1)猜想。这件事极大抬高了我作为一名数学家的学术声望。
但说实话，那个解决了𝐾(π,1)猜想的大卫，只是那个创造出定义2.4、定义9.3的更加优秀的大卫，所衍生出的一个社会符号。
打破不成文荣誉准则
过去几个月，面对AI与数学交织的飞速变局，我的内心产生了远超自己预想的困扰。
理论层面，我本应当感到理直气壮、满心欣喜。可现实中，我同时充满疑惑、忧虑与怅然。欣喜的那部分自我，真切看到一场变革正在发生，为之激动；理直气壮的那部分自我相信，我早已从科学与认识论层面预见到这一切；困惑的那部分自我，对变化到来之迅速与随之而来的狂热感到错愕；怅然的那部分自我，怀念那个自己曾经投身、如今或许即将消逝的工作方式与价值体系。
而忧虑的那部分自我，把所有感受融合在一起。我一直知道，普通大众对数学存在诸多误解，但我从未料到，这种误解会演变成对整个学科生存的威胁。
在我的著作《数学：直觉与好奇心的隐秘世界》当中，我把这种误解描述为两套数学观念之间的矛盾：官方数学和隐秘数学。
官方数学表现为一套形式化演绎体系：从公理出发，机械推导出一条条定理。这是极客眼中的理想国度，真理非真即假，推理要么有效、要么无效，理论上不存在胡说八道的空间。
而隐秘数学则是属于人的那一面：官方数学这套体系因何诞生，人类如何与它交互，它对我们大脑带来怎样的影响，以及数学家依靠哪些奇特的心智技巧不断拓展数学的边界。
隐秘数学从来不会进入课程大纲，因为它不具备官方数学那种确定的特质，看上去也只是次要内容。官方数学冰冷、严谨、逻辑完备、客观，被传为宇宙的语言。与之对照，隐秘数学柔软、模糊、主观，看上去仅仅是廉价的教学背景故事。
也难怪职业数学家对自己的工作有着割裂的认知。
“直觉俱乐部第一条规矩：不许谈论直觉俱乐部。第二条规矩：如果你非要谈及直觉，就要说得轻描淡写，仿佛只是附属点缀，毕竟我们又不是心理学系。第三条规矩：定义一文不值，阐释性工作还要倒扣印象分，最好的岗位永远留给证明了最难定理的人。”
如果你觉得我言过其实，不妨看看G·H·哈代在那本知名却又令人不快的《一个数学家的辩白》当中写下的话：
“没有哪种轻蔑，会比创造者对于阐释者的鄙夷更加深刻，大体而言也更加理所应当。阐释、批判、鉴赏，这些都只是二流头脑做的事。”
这正是割裂心态的极致表现。关起门，数学家们会纷纷抱怨哈代这套“诅咒”。他们会强调教学的价值，哪怕只是为了自己理解知识本身；他们哀叹这套体系病态般执着于定理证明的优先权，可所有人都清楚，大量真正艰难的工作恰恰发生在证明之外，发生在努力理解已有结果的过程当中。然而在公开场合，大家依旧被数学家的荣誉准则束缚：去证明定理，少多言！
不过有一个例外：拿到菲尔兹奖章之后，你就可以畅所欲言。
1982年菲尔兹奖章得主比尔·瑟斯顿就是一位极具反叛精神的人。离世两年前，在MathOverflow上，一位缺乏自信的本科生提出一个问题，瑟斯顿参与了那场精彩讨论。
本科生提问：像我这样的人，可以为数学做出什么贡献？在我看来，数学是高斯、欧拉这类人创造出来的。即便我可以研读、理解他们的成果，也不会诞生任何新东西。我可以把他们的著作改写为现代语言符号，或是引导其他人学习，但我从不认为这是数学家工作最重要的部分——真正重要的是创造全新的数学。现实中无数聪慧的人奋力耕耘，会不会已经没有留给像我这样普通人的空间？难道我的价值只能充当炮灰？大量人前赴后继，总能冲破某些难关。
瑟斯顿如此回复：
你需要贡献的对象，并不单单是数学本身。这件事的意义还要更加深远：从事数学，你可以怎样回馈人类，更进一步，怎样造福世界？这个问题无法只靠纯粹理智回答，我们行为带来的后果远远超出我们的理解范围。人类是深度社会性、深度受本能驱动的生物，我们的幸福仰赖很多难以用理智解释的事物。所以遵从你的本心与热爱才是正确的选择。纯粹理性很有可能将你引向歧途²。我们之中，没有人拥有足够的聪慧与智慧，仅凭思考就能把一切看透。
数学的成果是明晰与理解，而不是单单那些定理本身。举个例子，即便像费马大定理、庞加莱猜想这样赫赫有名的结果，它们真正的意义何在？其价值并不在于命题本身，而在于它们对人类理解提出的挑战；这些挑战催生数学发展，提升了我们的认知……
数学只能存活于数学家鲜活的社群之中：社群传播理解，为新旧思想赋予生命力。从事数学真正的满足感，来自互相学习、彼此分享。我们所有人，都可以对少数事物拥有透彻理解，对更多概念依旧模棱两可。永远不会缺少有待厘清的想法……
这里我们要短暂做一番形而上的思考，因为人们很容易把瑟斯顿这番话贬低成鸡汤或者迎合潮流的说辞。
在我的第一篇Substack博文当中，我半开玩笑地写道，两千三百年来我们都误解了数学，深陷形式主义（“数学是一套无意义形式符号游戏”）与柏拉图主义（“数学捕捉理念世界真实实体的性质”）的虚假二元对立。
我提出的概念论解读，正是对瑟斯顿观点的重述：数学确实会玩这套无意义的形式符号游戏，但我们之所以要玩这套游戏，是因为我们向符号投射了意义。
意义是一种认知现象，是我们神经架构的产物，并不是对超验实在的直接触碰。
当我们“做数学”，我们操作形式表达式，慢慢建立起对符号所代表事物的直觉，仿佛这些符号指向柏拉图理念世界真实存在的对象。柏拉图主义者把这种神经可塑性带来的副效应当作事实本身；形式主义者把它视作无关紧要的附属品。而我这样的概念论者认为，数学是人类至关重要的认知基础设施。
一个很自然的问题是，为什么概念论视角迟迟才出现。一部分原因在于它和盛行的唯灵论世界观相冲突，后者拒绝从物理层面解读数学。
它同样和数学家的荣誉准则相悖。哈代的诅咒力量强大，就连瑟斯顿都难以完全挣脱。当MathOverflow众多用户感谢他的见解时，他回复道：
“感谢各位留言。我试着写下内心真实的感受。到了这个年纪，我已经不再畏惧别人如何评判我，所以讲出来会轻松很多。如果我的所思所想对其他人有价值，那会令我感到欣慰。”
可这套极具负面影响的荣誉准则为何可以存续如此之久？
答案很简单：对于学术领域而言，这套准则曾经发挥过作用。正如我书的后记写的那样：
“这套体系自有它的长处。它减少主观武断，让数学家警惕自满与任人唯亲。当学科研究的是永恒真理，这套准则提供了一套简洁的职业评价标尺。”
这套荣誉准则同样为研究者评估新思路、新方向提供指引。2018菲尔兹奖得主彼得·舒尔茨（Peter Scholze）谈到，概念构建与问题求解，这数学的两个侧面，是共生的关系³：
“我最看重的就是定义。人类依靠语言描述数学，永远需要精准的词汇来清晰表达想法……可惜，仅仅依靠沉思，你不可能找到合适的定义；你要找到那些问题，只有隔离出新的关键概念，才能取得进展。”
数千年来学科就是这样运转：数学家依靠引入新概念创造价值，可现实规则是，只有定理，才可以换取安身立命的面包。过去这套模式行得通，因为两件事几乎总是相伴而生。那个解决了𝐾(π,1)猜想、收获声望的大卫，恰恰也就是那个创造定义2.4、定义9.3的大卫。
攻克重大猜想这件事，就相当于一份密码学意义上的证明：证明你做出了真正的概念创新。
我之所以要用过去时态讲述，是因为这套模式已经不再成立。数学家这套荣誉准则存在结构性漏洞，而AI已经开始系统性利用这个漏洞。
围棋与象棋的类比
触发我写下本文的是杰弗里·辛顿的一段演讲，让我始料未及：
“我很认同DeepMind负责人德米斯·哈萨比斯多年以来的观点：AI将会极大推动科学进步……有一个领域会格外容易实现突破，那就是数学，因为数学是封闭系统……我认为，大约十年之内，AI做数学的能力会远超人类。数学很像围棋、象棋这类拥有固定规则的封闭系统……”
我本就知道普通大众对数学本质存在巨大误解。但我万万没有想到，一位图灵奖、诺贝尔奖得主，会把数学拿来和围棋、象棋相提并论。
我在X平台简短写了回复，本打算翻篇，但这件事一直在心头萦绕。
大约一年前，一位和我同领域取得博士学位的年轻数学家朋友找到我。他打算创业，做面向纯数学的AI业务，我给他提供过一段时间指导。
和他、和辛顿、哈萨比斯一样，我完全相信AI将会重塑数学乃至整个科学。但我始终想不通它的商业模式与最小可行产品究竟是什么。
数学家看上去像卢德分子，但其实很少是。他们热爱纸笔、黑板粉笔，但当年也欣然拥抱TeX排版系统。一个世纪之前，大家选择把整套知识体系重建在集合论这套新“操作系统”之上，只为换取更高可靠性与可拓展性。
几十年之后，人们意识到柯里‑霍华德对应（计算机程序与数学证明之间深层的结构性等价关系，也被称为“命题为类型”或“程序即证明”），由此着手建造最早一批计算机。深度学习大量依托线性代数、随机梯度下降，它本身就是数学的产物。
1970年代，肯尼斯·阿佩尔与沃尔夫冈·哈肯借助计算机证明四色定理，在同行评审期刊圈内，掀起一场关于计算机辅助证明认识论地位的激烈争论。说实话结局并没有太多悬念：“野蛮者”取得胜利，因为论战两边都不乏“野蛮者”。
计算机早已是我数学生涯的一部分⁴，AI与自动形式化带来的前景一直令我无比向往。所以朋友来找我寻求建议的时候，我兴致很高。
我开始研究“AI做数学”这个赛道，百思不得其解：为什么这些初创企业可以拿到巨额融资？纯数学本身市场体量极小，投资规模显得完全不成比例。
我原本倾向的方案，是打造AI时代版本的Wolfram研究院。赋能科学技术的数学，市场远比纯数学广阔。就像Wolfram证明的那样，我们可以简化人与数学对象交互的体验，做成产品。用户会喜爱产品，用户粘性也很强。
但我的朋友坚持，他只想聚焦纯数学领域。
我一时无言。我能想到的可用产品，就只有文献检索工具、交互式证明助手；它们很难封装，很难定价，更难售卖。我能看到一条长期商业路径，但我避之唯恐不及：那就是成为AI时代的爱思唯尔，科学圈最招人痛恨的垄断巨头，把公共数学知识重新打包，强制所有人使用。
不过还存在第三种方案，风险同样不小，也需要相当程度的犬儒心态。我把它叫做“奢侈收购创业套路”：
造出足够博眼球、但实际用处有限的产品； 营造出已经解决重大科学难题的假象； 祈祷科技巨头、大型AI实验室快速并购收购。
即便如此，融资数字依旧说不通。传闻这些AI数学初创企业拿到数亿美元投资，背后一定存在一套我没能看懂的投资逻辑⁵。
后来听说谷歌投入巨大资源，想要攻克纳维‑斯托克斯方程解的存在性与光滑性——这是千禧年大奖难题。我心想，哦，我懂了，目标是千禧年大奖。但等等，奖金不过区区一百万美元，实在微不足道。一位杰出数学家跟我说，谷歌投入这件事动用的智力资源，或许已经超过整个学界历史上投入的总和。
直到听完辛顿的演讲，一切才豁然开朗。
如果数学真的是封闭系统，或者说，如果所有相关利益方愿意相信这一点，那么投资宣讲话术就变得无比简单直白：“DeepMind搞定了围棋象棋，我们要来搞定数学！”
各大AI实验室押下万亿级别赌注，认定人类很快会被淘汰。而攻克数学——人类皇冠上的明珠，这件事对他们拥有难以抗拒的诱惑力。
拿卡尺上战场
2月5日，十一位顶尖数学家（包括2014菲尔兹奖得主马丁·海尔）对外发布First Proof项目（First Proof首轮验证项目：数学家们组团出题考验AI（10个研究级数学问题拷问最先进AI，问题答案2月13日公布）），在arXiv放出稿件：
“本文是我们初步的成果，意在建立一套客观、现实的评估方法，衡量AI独立解决研究级数学问题的能力。在社群内部充分沉淀想法之后，我们希望数月之后产出一套结构更加完备的基准测试集。
我们核心目标之一，是深入理解AI工具在职业数学家工作流中扮演的角色。商用AI系统无疑已经可以作为数学家的得力工具。但目前我们依旧不清楚，脱离人类专家参与，AI独立解决研究级别数学问题究竟能达到什么水平。”
纯粹从科学角度看，无可指摘。这群绝顶聪明的人，直面真实争议，思路开放，富于创造力。
First Proof团队做的一切都无可挑剔，可恰恰是这件事，让我感到恐慌。
先声明：我对这个项目评价很高。团队代表了数学社群最优秀的一批人，充满好奇心与职业操守，愿意跳出舒适区做实验，也确实产出了真正有价值的想法。
丹尼尔·利特写过一篇非常出色的文章《巴别图书馆中的数学》（巴别图书馆中的数学——多伦多大学数学家丹尼尔・利特（Daniel Litt）再谈AI人工智能与数学研究的未来），剖析First Proof项目，分享自己对AI数学领域的一手观察。他是坚定的非卢德派纯数学家，多年使用大语言模型，对近期进展印象深刻。
他惊讶地发现，谷歌、OpenAI等多家机构，解决了First Proof当中相当多的开放问题。按照他统计：把各家结果汇总，十个问题里面大约六到八个得到正确解答。数学研究智能体Aletheia自主求解FirstProof挑战成绩6/10——由Google Gemini 3 Deep Think驱动
但这里存在重大警示：模型以及监督模型的人类产出大量无效垃圾，其中不乏宣称已经在Lean完成形式化、实则错误的解答。即便是表现最好的模型与辅助框架，也无法可靠识别自己什么时候在输出无意义内容。
就算AI数学系统真的做到自主运行——现在绝大多数还做不到——依旧需要人类在前后环节介入，至少要评估结果，筛除垃圾。这不是道听途说：AI实验室在这些项目投入的人力，远超任何一位现实数学家可以调动的资源，人与机器的边界因此变得模糊。最有说服力的例子：
OpenAI自己都分不清，他们提交给First Proof的解答哪些是正确的。
换言之，如果没有学界无偿付出，他们永远无从知晓真相。（利特本人也参与过评审。）
诚然，人类写出的证明同样会出错。但二者存在本质差别。人类做数学的时候，定理证明与概念构建相伴相生，这就迫使证明本身必须具备可理解性（至少对作者本人要可以读懂）。
形而上学层面的矛盾在此显现。倘若数学仅仅是一套无意义符号的形式游戏，那么“可理解性”这个概念本身就是空洞的。但真实的数学实践给出完全相反的答案。诚然已发表论文充满bug，但这些bug大多有限、可以修复；恰恰因为人类写出的证明具备意义，几乎总是方向正确。这两点，和形式主义世界观无法兼容。
这并不是细枝末节，而是数学作为一项可持续事业得以存续的必要条件。
正如利特指出，First Proof给出的AI解答，缺失了“求真”这一内核特质：
“不少正确解答行文极其糟糕，正确性极难核验……在人类的解答当中，核心想法、需要克服的障碍通常清晰可辨；而AI输出的内容，关键点往往模糊不清。人类作者在写证明的过程中，经常会提炼新的对象、术语来描述自己的工作；但模型只会一味向前推导。”
于是AI数学革命的第二块拼图登场：自动形式化。把人类略非正式风格的证明，还有大语言模型的输出，转化为Lean这类专用语言书写、机器可以完整核验、无懈可击的逻辑推导。
纸面之上，自动形式化仿佛可以解决正确性问题，不再需要人工核验。但利特也写道：“所有问题当中，仅有一份可信的形式化解答，还是由Tom de Groot耗费大量人力手动完成。”
当然，事态还在持续演变，赌注巨大，投入资源海量。大模型、辅助框架、自动形式化技术都在稳步进步。
设想一年之后，First Proof团队放出又一套同等难度的十道问题，会发生什么？利特没有直接回答，但他预期未来几年，AI就可以自主产出水平媲美顶尖期刊论文的结果。
我也抱有同样观感。在我看来，届时头部AI实验室很可能拿到满分，全自动给出全部十道题目的正确解答。
难道到2027年初，就意味着AI“攻克了数学”？
当然不是。有三点关键提醒，业内人士一眼就能看懂，但普通读者很容易忽略。
警示一：重重汪洋
第一点很直白：First Proof的这些“研究级问题”，谈不上多么深刻，难度有限。它们更偏向技术引理，也就是证明大定理过程中出现的、几页篇幅就可以处理好的中间子问题。
从一条技术引理到一篇正经论文，隔着一重汪洋；从论文到重大突破，又是一重汪洋；从重大突破到菲尔兹奖级别的成果，更是汪洋重重。在此之上还有更高的境界。
First Proof第二批次题目正在筹备，预计会选用难度更高的问题。
从技术角度，第一批选择这个难度档位是合理的，这也是事后才看清：最终得分介于0‑10之间，刚好落在它预设目标的甜蜜点——建立客观现实的评估手段。
但发布一套不含真正高深度难题的基准测试，风险极大。普通大众不会去读小字备注，很多人连什么是引理都不知道。如果谷歌或者OpenAI拿到满分，新闻头条就会写成：
“游戏结束：顶尖数学家向AI抛出十道研究级难题，AI全部横扫。”
社交媒体上类似的歪曲每天都在上演，恰恰助长First Proof本想要消解的误解。
警示二：可积累性
第二点要深刻得多，微妙，很难向普通大众讲明白。
不可读的证明，问题远远不止正确性；单凭自动形式化，无法解决这个困境。就算证明本身正确，一份不可读懂的证明，无法为数学知识体系做出可积累的贡献。
听上去很离经叛道，我举个例子。几周之前，资金雄厚的AI数学初创企业Math Inc，完成了玛丽娜·维亚佐夫斯卡关于8维、24维球体堆积结果的Lean形式化。AI与人类协作在数学领域迎来里程碑时刻 ——21世纪菲尔兹奖获奖证明首次完成形式化验证——IEEE Spectrum这套成果帮助维亚佐夫斯卡拿到菲尔兹奖。
这件事本身相当震撼：菲尔兹奖级别的定理，第一次被自动形式化。2026.5数学未来研讨会系列——球体堆积问题的形式化by 玛丽娜·维亚佐夫斯卡（Maryna Viazovska，2022年菲尔兹奖得主）——斯坦福FMS可这件壮举，却遭到形式化学界内部强烈抵制——恰恰就是那批致力于把人类数学移植进机器可核验代码的人。
难道他们是卢德分子？
事情远比这复杂，Zulip聊天记录可以看出来⁶。自动形式化不等于完整的形式化数学解决方案，就好比特斯拉完全自动驾驶不等于完整的自动驾驶解决方案。
听起来反直觉，所以圈外人很容易把抵制解读成抗拒新技术。亚历克斯·康托罗维奇写过一篇很好的讲座笔记解释这件事。简单说：Mathlib，主流Lean库，是人类整理出来的形式化数学库，拥有干净的应用程序接口与抽象层；没有这些，任何自动形式化都无从谈起。与之对照，Math Inc产出的维亚佐夫斯卡证明，没有暴露出任何可供使用、可以读懂的接口。心智正常的人，谁愿意把二十万行未经审计、凭感觉生成的庞大代码合并进全人类科学的主分支？
康托罗维奇提出一个绝妙的词：规范化（canonization）。
“规范化，指的是把一次性的局部形式化结果，改造为库级别的数学：通用、可复用、自洽、高效，并且可以和其余体系兼容……规范化往往会改动体系本身：定义、抽象、接口，甚至命题陈述……这件事极度耗费精力与时间。”
但这一点很容易被贴上卢德分子的标签。“通用、可复用、自洽、高效……难道这些只是眼界狭隘的人类编造出来的保守说辞？AGI为什么要在乎这些？难道自动形式化按定义不就已经解决凭感觉写代码的全部问题？”
经过证明的代码，难道不满足软件最高标准？为什么你们总在不断移动球门柱？
软件领域的类比可以帮我们看清核心矛盾。普通软件，质量首先看实用性：可以编译、线上稳定运行、满足用户需求。但是Lean代码永远不会被“运行”。它只是存放在代码库，未来不知道什么时候别的定理形式化会导入调用。你不能做“持续部署”，因为它唯一的用户，就是未来的数学研究者。所以从欧几里得《几何原本》，到策梅洛‑弗伦克尔集合论，再到布尔巴基，规范化一直都是形式主义学派的核心关切。
我们又回到形而上层面。不可读懂的数学，问题不在于它可能出错。真正的问题在于：从字面意义上讲，它失去了意义。因为它无法在当下唯一能够理解、欣赏它价值的硬件——人类大脑上面“编译运行”。
当然，未来情况可以改变。人脑并没有什么魔法。将来必然会诞生人工的意义生成、求真的架构，在数学创造包括形式证明规范化方方面面全面超越人类。但那绝对不是我们当下所处的现实，也不是现有趋势简单外推就可以抵达；开展富有成效的辩论的条件尚不具备。
不管怎样，只要人类还存在，我们依旧会渴望理解世界，这份渴望会持续驱动我们研究数学。
没有人知道通用人工智能什么时候到来。而当下顶尖模型的自动规范化能力几乎为零。Math Inc那套维亚佐夫斯卡二十万行证明，就变成一份孤悬在外、无人维护的代码块。
这就是Mathlib社群愤怒的根源。他们多年团队协作，本来就在做维亚佐夫斯卡成果的形式化工作。Math Inc介入进来，利用前人积累，大肆宣传自己的成果。
这件事就一定是坏事吗？既然暴力自动形式化已经做完，为什么Mathlib社群不能转而去做有价值的规范化工作？
因为哈代的诅咒、数学家的荣誉准则依旧生效。Math Inc已经摘走“首个完成菲尔兹级别定理形式化”的荣誉，清理后续工作再也得不到任何学术回报。形式化数学专家帕特里克·马索特（Patrick Massot）写下这样的看法：
“现状已经很清楚：AI公司，尤其是Math Inc，会彻底把这片领域炸成一片放射性荒原，再也无法孕育新的成果。我们永远得不到形式化本该带来的收益：理解提升，知识可及。我强烈建议年轻人去投身那些不容易被这样摧毁的项目。”
即便不能对整体知识库做出积累，不可读懂的形式证明依旧可以具备残余价值。
说实话，这个问题早在AI出现之前就已经存在：四色定理、有限单群分类，还有汤姆·黑尔斯庞大的开普勒猜想工作，都属于这个范畴，后者也促使他走上形式化证明的道路。
未来很可能会演化成两种层级并存：一层是以Mathlib为代表的可读懂层；另一层我把它叫做Mathslop，一堆正确性已知、但没有任何人读懂过证明的结果库。
警示三：悬置存量（The Overhang）
First Proof题目刚放出的时候，我最大的担忧就是各大AI实验室会轻而易举搞定全部十题，理由却并不光鲜：这些问题的答案，已经以某种形式存在于现有文献之中。
利特提到，十道题当中，两道题在已有文献中存在解答⁷，不少大模型自然就可以调用；第三道存在证明梗概，但没有模型解出来。
那剩下七道呢？它们真的是尚未解决的开放问题吗？在何种意义上算开放？
我的看法是，我们无法给出确切答案，这源于数学知识库本身的结构性特质，这个特质会在AI‑数学辩论中占据核心地位。我甚至怀疑，我们传统意义上的“创造力”“创新”概念根基就存在缺陷，AI会给我们上残酷一课。
绝大多数数学家内心隐约感知这种结构性特质，可没有人完整测绘它，学界也没有公认名字，我把它叫做悬置存量（The Overhang）。
我相信悬置存量的体量无比巨大。
我的职业生涯多次和它相遇，大多只是寻常体会，唯有一次令我无比震撼。我刚刚构思出定义9.3当中的核心概念，也就是后来的“分拆加尔赛德范畴”，我自认为这是极具原创性的构想，可以解开经典猜想。主观上，那一刻我感觉如同天才灵光一闪。
当我开始规范化这份最富创造力的构想，我震惊地发现：我引以为傲的发明，本质等价于代数K理论里面一篇晦涩文献里面已经存在的构造。
换言之，我这个所谓天才想法，早已在别处出现过。又或者，并没有？二十年过去，我依旧把那一瞬间视作职业生涯的高光时刻。我不在乎它算不算严格意义上的原创，我认为这并不是最重要的评判标准。真正打动我的，是意义涌现那超现实的一瞬。（这就是高价值成果的认知标志。）
无论如何，一个优秀大模型，在我研究尚处于早期、我自己都看不清方向的时候，就可以捕捉句法层面的相似，抢先发布结果，把我“截胡”。
不同研究领域之间存在深刻的对应关系，是数学最令人赞叹的特质之一，是喜悦与惊奇的源泉，也是数学之美的纯粹体现。笛卡尔注意到代数和几何本质相通，搭建起二者之间的桥梁，由此改变世界。一旦发明笛卡尔坐标系，一大堆老问题迎刃而解，同时立刻诞生大量有趣新问题。
但现代数学庞大复杂，大量这类对应关系始终不为人知。
有时候把碎片联系起来，得到的不是发现，反而是更深的谜团。一个经典例子就是约翰·麦凯那个著名观察：196883 + 1 = 196884。196883来自大魔群研究，196884来自模形式，两个领域原本毫不相干。猜想二者存在联系，在当时听上去荒诞，被称作“月光猜想”。理查德·博赫德斯（Richard Borcherds）凭借证明这个猜想拿到1998菲尔兹奖。
可有时候，仅仅把已有文献碎片关联起来，就足以解决重大猜想。猜想证明的最后一步，经常是意识到缺失的素材早已埋藏在过往论文中。
悬置存量，就是过去数学创造力尚未兑现的潜在价值，是把现有知识库碎片相互关联可以释放出的红利，也是规范化带来的馈赠。数学家A提出问题A；数学家B创造概念B；然后数学家Z注意到B可以直接解决A，于是Z收获这份社会认可。但在收获认可的过程当中，Z通常又会引入新概念、新开放猜想，向悬置存量注入新的潜在价值。
大语言模型训练素材可以吃下全部数学文献。凭借惊人记忆、模式匹配能力（尽管并不总能理清关联逻辑，正确标注来源），它们得天独厚，可以开采这份悬置存量。反观职业数学家，一辈子读过的论文也就几百篇，对比数百万条文献总库，占比不足0.1%。
这件事无疑会带来激动人心的重大发现。但它也会导向一种令人悲哀的新局面：人类辛辛苦苦整理积累悬置存量，AI却总是在终点线上抢先截胡人类。
当然距离这一幕还很远，这件事本身就令人迷茫。利特提出尖锐问题：人类拥有这类能力，几乎会源源不断产出惊艳定理；那为什么模型还没有做到？模型到底缺失了什么？
答案其实很明显：当今AI系统和人类处理数学的方式完全不同。AI在某些方面远超人类，也在很多方面弱于人类。
AI同时“超人类”又“亚人类”，取决于你的评判角度。这既是对AI的肯定，也是对人类的肯定。这种多维度特质，让整套基准测试体系变得脆弱，甚至近乎虚妄。完全有可能，AI在实现概念构建能力之前，就达成问题求解层面的碾压优势。那我们该叫它什么？“超级智能”？说真的？
这就是我对First Proof这套范式核心的顾虑。对于还困守在过时荣誉准则之中、想要了解AI当下能做什么的在职数学家来说，它是有价值的基准。
但为什么我们不去建立一套对人类更加公平的基准？因为我们做不到。数学真正的价值，是个人与集体层面拓展我们看待世界的眼界，这件东西定义模糊，无法量化。恰恰是这种不可量化，催生了那套荣誉准则。
格罗滕迪克就他的格罗滕迪克‑黎曼‑罗赫定理的难度大发感慨
数千年来，我们习惯只用“问题求解”来衡量人类智力，因为它是最好的客观替代指标。证明定理对我们的认知而言无比艰难，前进的必经之路，就是耐心构建概念，在脑中内化这些新概念。
可它终究只是替代指标。我们真正关心的，是另一类完全不同的东西。工业机器人力量远超人类，但我们依旧会去健身房。搅拌机咀嚼能力远超人类百年，但我们不会只依靠吸管进食。
我知道观感很糟糕。宣称数学首先关乎理解，而理解这件事难以测评，听上去像一套很取巧的借口。但我并不是临时才编造这套说辞。五年之前，AI浪潮还没兴起，我就在X上写下：
“人们通常认为数学是追寻普适真理，追寻不依附特定语境的模式。但更深层次，数学的目标，是发展出看待、思考世界的全新高级方式。数学是一场转变自我的旅程；衡量进步的标尺，是我们思考方式的改变，而非我们发掘出的外在真理。”
我在自己的书中引用过这段话。还引用过笛卡尔1628年的一段感慨：古希腊数学家怀着某种有害的机巧，“把真正的数学”（笛卡尔把它等同于内在认知方法论）给遮蔽起来，只留下一些幼稚、无意义的成果。他们只发表这套方法产出的某些贫瘠真理，精巧的证明，却不去传授方法本身⁸。
陶哲轩也有过类似表述：
“很多时候，过程本身比问题更加重要。问题只是衡量进步的替代物。”
他还做出一个引人注目的预判：
“我认为十年之内，数学家如今耗费大量时间完成的很多工作，我们论文里面大量内容，都可以交由AI完成。但到那时候，我们会发现，那些并不是我们工作当中最重要的部分。”
社交媒体上反馈绝大多数是正面的。但也出现过不寻常的反对声音，针对“单纯求解问题本身并没有那么高价值”这个观点。
对于通用人工智能的鼓吹者来说，这番话仿佛拒绝看清摆在眼前的现实，甚至不乏嘲讽。
警报并非演习
3月3日，新成立的计算机辅助数学推理研究所ICARM首任主任杰里米·阿维加德，在arXiv发布一篇五页长文 AI人工智能时代的数学家们——杰里米·阿维加德（Jeremy Avigad）。文章详细复盘Math Inc与Mathlib之间的冲突事件，阿维加德本人就是亲历者。他同样是立场开明、绝非卢德派的研究者，身处绝佳位置观察这场巨变：
“我们必须直面现实：AI很快就可以比人类更出色地证明定理……我们要牢记我们的长处：数学家是顶尖的问题解决者与理论构建者。不要抗拒AI在数学当中的使用，我们要主动驾驭它。仅仅跟上潮流、为AI研究者设计基准测试远远不够；我们要主动部署这项技术，按照我们的目标去塑造它。”
谈及First Proof项目，阿维加德写道，谷歌可以解出十题当中的六道，这件事令他“惊讶”。
读完上面所有内容，我会用“松了一口气”，而不是“惊讶”来描述感受。当然我也确实感到意外，因为我对这些题目实际难度没有直觉，也没有预判会被解出来多少道。
真正让我不安的，是阿维加德那句略带轻松的描述：“不少AI开发者上钩了。”
我不知道这句话是反讽还是天真。熟悉科技行业生态的人看得清清楚楚：这套题目一放出，必然会在各大头部AI实验室里面触发一场最高优先级的疯狂竞赛。谁愿意错过这样的机会？
OpenAI总裁格雷格·布罗克曼这样评价First Proof：
“First Proof这个概念和方案非常棒，向整个团队表示祝贺，感谢你们！”
这件事发生在2月14日，OpenAI正路演，争取史上规模最大一轮私人科技融资。更加值得玩味，在那段压力巨大的几周，OpenAI管理层不止一人分心参与这件极客向的副业。几天之前，山姆·奥特曼还抽空写过一点代码，感慨Codex让自己感觉“变得一无是处”。
但这真的算是“分心”吗？你可以解读成一条大鱼吃下诱饵；也可以解读成狐狸感谢母鸡交出鸡舍钥匙。
澄清一点：我并不认为OpenAI或者其他AI实验室在做什么邪恶的事。First Proof把题目公之于众之后，他们别无选择，必须投入全部力量参与比拼，不能接受被对手比下去。
事实上，AI实验室确实手握激动人心的技术，定理证明也确实是一个很有吸引力的应用场景。
真正的问题，来自外界对这件事的解读。
这正是辛顿的演讲令人不安的地方。他把数学贬低成唾手可得的目标，一个“格外简单”的领域，理由是“它是一套有规则的封闭系统”，“就像围棋、象棋”。但是围棋、象棋并不是普通的封闭系统；它们是有明确胜负的双人有限完全信息博弈，根据1913年的策梅洛定理，它们存在最优策略⁹。
可如果AI在“数学”这件事上面“赢了”，那么输家又会是谁？这间房间里面唯一的对手，就是人类的思想。
即便数学本就不是对抗性游戏，规则也还处在不断演变之中。但只要新闻足够耸人听闻，就值得大肆报道。
设想一个最坏的场景：一年之后，某AI实验室组建秘密顶尖团队，投入数十亿美元算力，针对黎曼猜想产出一份两百万行的Lean证明。数学家可以怎么回应？
“这份证明读不懂。”——没错，但谁在乎？绝大多数人类本就读不懂绝大部分数学。
“证明依旧离不开人类参与者。”——是，但放到这个案例，我大概率会投反对票。
“数十亿美元，相当于美国国家科学基金会整个数理科学几十年总预算。”——就算如此，又如何？万一这个猜想难度其实很低，只需要少量资源就搞定呢？
“但是猜想本身，连同它底下整套数学体系，无穷级数、复变函数、亚纯函数、解析延拓，还有把猜想解读成对素数分布的深刻命题，全部都是人类大脑创造出来；到目前为止，也只有人类真正在意这个问题。”
这个反驳深刻，也站得住脚。可一旦你看上去像输不起的失败者，就没有人愿意听你的道理。
我并不预期这个精确场景真的会发生。但在不远的将来，我们大概率会看到宣称“AI已经攻克数学”、“实现数学霸权”的言论。结合当下舆论环境，这些证据会被解读成人类智力的溃败。
如果连杰弗里·辛顿都看不透这一层，那么99.9999%的普通人更不可能看懂。
灾难真正到来的时候，无论内心多想发声，数学家都要从现在开始练习表达。想要完全避开这场冲击或许为时已晚，但至少我们还有一点时间去预判、去联合起来。
一个危险的信号，就是年轻数学家群体的动向，不少人选择入职AI实验室。坦白说，我理解他们的选择；如果我处在他们的处境，我很可能做出同样的决定。
与此同时，还没有拿到终身教职的学者流露绝望。哈佛博士后阿什温·斯瓦米纳坦，读过利特那篇文章，深表认同，他在X写下长长的帖子，谈及教学这个核心问题：
“有人会觉得，研究数学家可以依靠教学维持工作。但这忽略AI给教学领域带来的巨大冲击。现在大量学生使用AI完成作业，大学文凭很快会贬值。找我答疑、参加办公室答疑时间的学生数量暴跌。学生家庭作业成绩很好，可考试表现糟糕。很多孩子毕业，并不掌握真正的本领。”
我要强调：这件事和研究领域遇到的困境本质同源。求解问题只是达成目的的手段。纯数学真正的回报，是我们世界观在神经层面得到提升；单纯复制粘贴现成答案，无法抵达这个目标。
“数学仅仅就是证明命题、得到结果”这种错误观念，从基础教育阶段就开始荼毒所有人。
特别是那句广为流传的说法：“AI已经可以完成博士级别的研究。”就算这句话成真，它的说服力也远没有看上去那么强。博士生终究还是学生。负责任的导师给博士生的，是策略可行的问题。实际上，绝大多数已发表的研究，都落在悬置存量范畴之内；它一部分是真正意义上的研究，另一部分则是维系研究社群认知运转的维护工作。这并不是在贬低我的同行，恰恰反映前沿数学本身的艰难，前沿数学只能作为集体事业的矛头而存在，并且这件事业的根基，就是要保证内容是人类可以理解的。
如果证明定理依旧是我们这套体系唯一通行的硬通货，未来几年，所有研究数学家都面临价值被剥夺的风险。
坦诚面对现实
数学社群可以做些什么？我看不到奇迹般的解决方案，但有一些显而易见的做法，可以减轻伤害。第一件事：我们最终要坦诚讲清楚数学究竟是什么。
我引用过的那些数学家，从陶哲轩到阿维加德，从利特到康托罗维奇，都小心翼翼地指出，数学的内涵超越定理证明。但这往往只是顺带一提，而不是叙事范式的重大转变。
而这件事恰恰需要叙事范式的彻底改变。如果不把这件事讲透彻，公众只会把这番话当成借口。想要重塑一个延续数千年的认知标签，你必须清晰说明你要做什么、为什么这么做、它可以给所有人带来什么价值。这件事必然分量沉重，必然困难，留给我们的窗口期十分短暂。
这大概算得上记忆当中规模最大的一次观念“产品召回”：我们向数十亿人兜售一套关于数学的错误观念，现在账单已经摆在面前。
唯一的出路，就是把核心主张放在最前面，反复重申。我再次引用瑟斯顿的话（阿维加德也把它放在自己《论数学理解》文章卷首）：
“我们不是为了完成定义、定理、证明这些抽象生产指标。衡量成功的标准，在于我们做的事情，能不能帮助人们更加清晰、有效地理解、思考数学。”
长远来看，这会逼迫我们彻底重新思考这个行业的精神内核与评价标准。数学家必须废除那套荣誉准则，废除直觉俱乐部第二条规矩：“如果你非要谈论直觉，就要说得轻描淡写，仿佛只是附属点缀，毕竟我们又不是心理学系。”如果瑟斯顿说得对，那我们本身就该算是心理学系的一部分。
知易行难。数学社群并不是一个可以召开紧急闭门会议、产出危机应对方案的组织。
我们甚至对于数学本身都没有统一的看法。一部分人真心相信数学的全部意义就是攻克尚未解决的难题；另一部分人持有别的观点。两种观点我都不认同，但我的看法终究只是个人观点。
缺少清晰的定义与使命宣言，整个社群处处被动。
xAI与Math Inc联合创始人克里斯蒂安·塞格迪曾经预言，2026年6月之前就会出现“超级人类数学家AI”。这类声明要么是空话（机电计算器超越人类计算能力已经上百年），要么就是极致的宏大叙事。不出意外，塞格迪还表示，他认为陶哲轩“脱离正在快速到来的现实”。
问题不在于预言本身，塞格迪拥有扎实技术背景，有权提出宏大设想。真正的问题，是舆论环境，让理性的反驳很难被听见。
我脑海里面反复冒出一个想法：我们需要一套类似汽车自动驾驶分级那样的数学智能分级 / 数学自动化分级。
这样就可以应对当下的迫切风险：基准测试只衡量解题能力，完全忽略理解能力、概念构建能力。当AI横扫新版First Proof测试集，新闻稿就可以写：“AI通过First Proof，在数学智能分级当中达到3级（满分10级）。”
数学家不应该惧怕主观性。这不等于作弊；而是追求公平，避免集体自我毁灭。事实上出题这件事本身就充满主观性。First Proof的题目、埃尔德什问题、千禧年大奖难题，除了“客观判断命题是否得到证明”之外，其余一切都不存在纯粹客观标准。
而数学创造当中更加深刻的那些维度——提出问题、规范化、构建概念、重构问题、化简、猜想，乃至构建完整新理论、开辟全新分支，这些东西不存在客观可核验的标尺，但绝不代表这些活动不存在，也绝不代表它们不重要。
主观评判当中同样存在客观维度。笛卡尔统一代数几何，牛顿莱布尼茨发明微积分，在他们同时代人眼里，很明显发生了重大突破。某种意义上，包括AI初创企业在内的整套技术体系，都在享用这些创造带来的红利。
理想的分级体系，应当是开放式，存在看上去遥不可及的最高档位。因为数学不是一件等待被“解决”的事物。
数学无穷无尽，难题无穷无尽，意味着进步的空间无穷无尽。当下最迫切的，就是让所有人明白，数学不是一件等待抢夺的奖杯。
数学的未来
令人悲伤的是，很多伤害已经注定会发生。就算执行得尽善尽美，在外部时间线的压力之下，我们也不可能完成一场认知层面的革命。当下大环境对基础科学极度不友好，每一处细微差别，都会立刻被解读成守门人的托词。
数学家的日子会变得艰难。学生会流失，经费缩减。博士后会抛出尖锐问题，资深教授必须给出回答。聚会当中，别人看你的眼神会变得古怪，仿佛你是活化石。
但压力终会得到缓解。行业会回归常态，AI数学初创企业必须找到自己的商业模式。而从大概率来看，不会是去解埃尔德什猜想。
对我而言，这就是当下时代最引人注目的一点。尽管声势浩大，各大AI实验室几乎并没有真正投入去理解数学本身，理解它的核心问题与意义。当然这也无可厚非，这本就不是他们的本职。
尘埃落定之后——如果真的会尘埃落定——人类数学会存活下来，只是已然蜕变。
我不去做时间预测，我不知道哪些能力会在何时达成，又会出现哪些局限。
但变化已经实实在在发生。这是一场真正的科学革命，研究社群已经投身其中。我写这篇文章的时候，每一天信息流里面都可以看到大量新进展，实在多到目不暇接。
悲观者会说，这只是恐惧催生的反应，各行各业都在发生同类转变。资本如此快速大规模重新配置，我们没有什么理性办法去为未来做好万全准备。
如果我没有离开一线研究，我也并不清楚自己会怎么选择。一个唾手可得的方向，就是用AI生成我那篇还没有写出来的胞分解定理形式化证明。之后去测试各种大胆想法与猜想。但这些都属于旧时代的思考方式。我怀疑未来数学研究的协作模式、产出物本身，都必须发生改变。
我的看法算不上多么新颖：未来做数学，离不开AI辅助，就如同现在做数学离不开集合论与LaTeX，这件事会变得理所当然。
但这并不会告诉我们二阶效应会是什么样。我做过一番推演，想到十多个可能性，并不全部深刻可信。下面三个，我认为很有意思：
我的观点：纯、应用，二者代表“可理解性‑实用性权衡”当中的不同最佳平衡点。投入百亿美元算力去求解等离子体约束方程，加速实现电网规模聚变反应堆，即便人类要再过一两百年才能完整理解它，这件事是合理的。但黎曼猜想，我认为并不适用这套逻辑。
我猜想AI给数学带来的变革，会类似采样器、音序器带给音乐行业的变革。掌握前沿概念的技术门槛会下降。勇敢的年轻数学家，可以用非传统手段，快速探索整片全新知识大陆，令老一辈为之惊叹。
他们站在巨型机器的肩膀之上，看得比前人更远。
AI已经带来始料未及的现实后果，这件事已经开始影响普罗大众的认知心理健康。如果我们讲不清楚“可理解性”在认知层面的价值，那么就再也没有任何理由去教授数学。毕竟99.99999%普通人一生遇到的数学问题，指尖随时可以调用AI给出答案。
人们隐约意识到这会导向愚昧社会，却讲不清楚为什么。我们依旧没有适配新时代现实的教学、评价模式。
真正令人担忧的，是那种错误认知：存在某种“正常”数学能力水准，仿佛某些概念比别的更加真实、更加具体，高深数学只是无端的抽象游戏。这种错觉让大家以为，普通人当下的数学水平就是“自然状态”；但现实这是大量、效率并不高的教学投入造就出来的结果，并不是什么天然的基准。人类完全可以演化出一种文化，语言里面数词最多只到5，部分狩猎‑采集部落就是如此。
有些人预言，未来数学会变得像国际象棋：少数怪人满怀热忱钻研，大众大可置之不理。
这是短视的看法，它忽略了数学的意义建构、求真特质，也忽略数学训练带来巨大认知收益。一旦你对数字、集合、统计、线性代数、微积分、微分几何、机器学习、组合学、动力系统、模型论、群论、奇点理论、同伦论、λ演算、范畴论建立直觉理解，你看待世界的方式会清晰得多。（清单可以无限往下写，当然一股脑全盘学习并不现实。）
这个困境并不是数学独有的。很多领域接纳AI的时候，都会遇到同类问题。但数学拥有独一无二的地位与光环，因为它自古以来就和“智能”这个概念深度绑定。
这就是为什么“AI做数学”这件事分量如此之重，妥善处理这件事，关乎人类物种的未来。
很多人讨厌数学，会把AI和数学混为一谈。他们把一切数学、计算机相关事物，视作对人性、主观体验、鲜活现实感受的威胁。
可他们会惊喜，也会心怀感激地发现：数学家其实站在他们一边，为美好事物而奋斗。
正如卡尔·古斯塔夫·雅可比所言：
“数学，是为人类精神之荣光而存在。”
（评论区已有120+条评论，作者做了一些回复，详见原文底部）
https://davidbessis.substack.com/p/the-fall-of-the-theorem-economy/comments
AI人工智能时代的数学家们——杰里米·阿维加德（Jeremy Avigad）
数学家心声：数学是什么，数学应当是什么？杰里米·阿维加德（Jeremy Avigad）2026-8-18
2026国际数学家大会ICM全体大会1小时报告内容剧透之《未来数学的形态》by Alex Kontorovich亚历克斯・康托罗维奇
数学家心声：Daniel Litt丹尼尔·利特《数学的一个新开端》2026-9-14
巴别图书馆中的数学——多伦多大学数学家丹尼尔・利特（Daniel Litt）再谈AI人工智能与数学研究的未来