博文
[转载]当数学成为一种机器能力：关于 AI4MATH、数学就业与数学共同体的思考
|||
AI4MATH 可能同时造成两种看似相反的变化：完成既有数学任务所需的人变少，社会能够提出并负担的数学要求却变多。理解这场变化，需要区分数学的社会使用、对严格数学训练形成的能力的需求、职业数学共同体的规模，以及机器化数学能力的分布。关于作者：https://col-sci.gxmzu.edu.cn/info/4671/20337.htm 文章内容不能代表作者所在工作单位的立场。本文使用ChatGPT生成，经过人工少量删改。
近两年，人工智能在数学上的进展已经很难再用“会做竞赛题”概括。前沿模型达到国际数学奥林匹克金牌水平，也开始在研究级问题上提交需要专家认真审查的证明尝试；Lean、自动定理证明、形式化验证和“AI for Science”则越来越频繁地进入数学系师生的视野。[1]
有人说，AI 既然能够做数学，人类以后就不必再学那么多数学了。这种判断跳过了很多中间机制。
AI4MATH 首先降低的是获得数学能力的成本。然后，至少会同时发生三种效应。其一是替代效应：过去需要人完成的计算、推导、建模、证明和检查，越来越多地由机器承担。其二是扩张效应：因为数学能力变得便宜，原来没有条件提出的数学要求开始变为值得提出，原来只能做到大致可靠的事情开始追求更高的精度、安全性和可解释性。其三是分布效应：这种能力既可能依附于昂贵的模型和算力而高度集中，也可能随着推理成本下降、开放模型和形式化工具普及而广泛扩散。
这三种效应不会自动朝同一个方向发展。社会使用的数学可以增加，以数学研究、教学或高度数学化工作为主要内容的岗位却可能减少；职业数学家的规模可以收缩，其他行业对经过严格数学训练形成的能力的需求却可能上升；数学能力可以成为普遍基础设施，其最前沿部分仍然可能掌握在少数组织手中。本文所要讨论的，正是这些过去常被捆在一起的问题，怎样在 AI4MATH 时代重新分开。
一、当数学能力从劳动者身上分离出来过去，数学知识、数学能力和人的长期训练大体绑定在一起。一个机构需要复杂计算、建模、证明、算法设计或严格验证，通常就必须找到能够完成这些工作的人。数学训练的价值不仅体现在数学研究和教学岗位中，也体现在芯片、软件、金融、密码、物理、工程和许多其他职业之中。现实中的工作很少把数学从其他环节中单独切出来；数学家以及许多其他职业的劳动，依靠的是从长期严格训练中形成的抽象能力、结构感、证明意识和定量判断。
AI 正在改变这种能力的供给方式。大量文献、算法、证明方法和问题求解经验，可以被固化在模型和软件系统中，随时复制和调用。一个机构仍然需要数学，甚至可能比过去需要得更多，但它不再总要按照任务数量同比例增加受过严格数学训练的人。过去附着在人身上的一部分能力，正在变成一种可以集中开发、反复部署的基础设施。
可以用一个很粗略但有用的关系来理解这种变化：
对人力的需求，取决于需要处理的数学任务总量，以及每项任务还需要多少人的时间。
AI4MATH 会明显压低第二项，却也可能抬高第一项。最终需要多少人，不能只看“数学有没有更多用途”，而要看新增任务的速度能否超过单位任务所需人力下降的速度。自动化研究中常用“替代旧任务”和“创造新任务”的框架来分析这一问题：生产率提高并不自动等于劳动需求增加，关键在于技术究竟只是接管原有任务，还是同时形成了足够多仍需人参与的新任务。[2]
对于数学，这个问题尤其尖锐。数学工作的对象与成果高度适合数字化表达，知识容易复制，证明的正确性还可以在一定程度上机械检查。一套成熟的模型或验证系统可以服务成千上万的用户，而不必让每个使用者所在的机构都建立同样规模的专家队伍。社会由此可能进入一种前所未有的状态：数学能力无处不在，却越来越少以分散的人类岗位出现。
二、数学更有用，为什么岗位仍可能更少市场和公共机构很少单独为“证明一个定理”付费。它们更常需要的是某个芯片少一次设计错误、某套软件降低故障风险、某个科学模型更加可靠，或者某项研究缩短周期。数学能够创造巨大的间接价值，却不意味着这些价值会按比例转化为专门的数学岗位。
AI4MATH 还会把一部分原本分散的工作推向上游。过去，一千家企业分别遇到建模、算法或验证问题，可能各自需要若干专业人员；将来，少数模型公司、国家实验室或大型技术平台可能承担昂贵的研发和算力成本，雇用相对于服务规模很少的高水平人员，再把同一套机器化数学能力提供给广泛的下游用户。前沿 AI 基础设施已经表现出高资本门槛、规模经济、纵向整合和集中化倾向，可见这种结构并非纯粹想象。[3]
形式化验证是一个很好的例子。它确实有真实用途，形式数学、软件与硬件验证、可信人工智能也确实形成了研究和工程岗位，中国同样能够找到形式化方法、定理证明和神经网络验证方向的招聘。[4] 但“应用面很广”和“能够吸收大量数学毕业生”是两个不同的命题。一项技术可以影响价值巨大的产业，却只需要很少的专门人员；而 AI4MATH 的目标之一，恰恰是降低证明和验证所需的人力。
因此，即使形式验证项目增长十倍，只要每个项目所需的人类时间降到原来的百分之一，相关岗位仍可能减少。给数学学生增加程序语言、软件安全、人工智能或芯片知识，或许能提高一部分人的适应能力，却不能据此推出这些交叉方向能够承载整个数学教育体系的就业规模。
剩余岗位还可能出现明显极化。大量标准化或中等难度的任务由机器完成，少数能够推动模型边界、识别深层错误、承担最终责任或提出关键问题的人反而更加重要。但几十名、几百名顶尖专家，与一个能够稳定吸收大批毕业生的职业体系，完全不是同一个数量级。把“创造性”“选题能力”或“价值判断”列为人类优势，也没有回答这些工作究竟需要多少人，更没有证明机器不会继续进入这些环节。
教育不能预先被当作安全的就业蓄水池。社会仍然需要数学教育，并不等于每一次讲解、答疑、出题和反馈都必须由高水平教师亲自完成。诚然，学校还承担组织、评价和社会化等功能，人类教师不会因为模型会讲课写论文就立即消失；但每名学生所需的人类教学时间，以及教学岗位对高水平数学训练的需求，都可能下降。人口减少也不会简单抵消这种压力：年轻人口收缩会减少未来劳动供给，同时也会减少生源和教学岗位，而中国研究生与博士生培养规模仍处于高位。[5]
所以，岗位减少的风险是存在的。数学越来越重要，不能直接推出数学家越来越稀缺；产业越来越依赖数学，也不能直接推出产业需要同比例增加经过长期训练的人。生产率的提高会创造财富，却没有一条经济规律保证它必然创造与原有岗位同等规模的新职业。
三、当数学变得廉价：从能做到精益求精但是，就业风险并没有穷尽 AI4MATH 的意义。完成同一项任务所需的人变少，只是成本下降的一面；另一面是，人类会开始要求过去根本负担不起的东西。
生产力的发展很少停留在“以前造不出来，现在能够造出来”。一种技术普及以后，人们通常还会继续追求更快、更便宜、更精确、更稳定、更安全，并尽量把结果控制在明确边界之内。从能造，到造好，再到向尽可能无懈可击推进，这种精益求精本身就会形成新的需求。速度和安全也不是简单对立的：系统运行得越快、规模越大、权限越高，错误的后果往往越严重，因而越需要验证、容错和安全保障。
形式化验证在这里不只是一个小型就业方向，而可能代表一种更深的技术变化。过去，普通软件主要依靠测试、代码审查和运行经验获得可信度，较完整的形式化证明至今多用于芯片、密码、航空航天等高风险领域，一个重要原因正是成本太高。现在，AWS 已经使用 Lean 为 Cedar 权限系统建立形式模型、证明关键性质，并把模型用于生产实现的持续检查。这还远未意味着所有软件都会获得完整证明，却说明形式化方法可以进入真实开发流程，而不只是停留在少数理论示范中。[6]
假如 AI 能够进一步降低编写规范、生成证明和维护证明的成本，那么将来没有形式保证的程序，可能逐渐像今天没有类型检查、自动测试和持续集成的程序一样显得不够可靠。软件工程的常规流程也可能从“写程序—测试”扩展为“明确需求—形成可检查的规范—生成程序—证明若干关键性质—在迭代中持续验证”。这不一定需要每家公司都建立庞大的形式化团队，却可能使数学严谨性渗入大量不被视为数学工作的岗位。
这种前景不能被夸大成“程序将变得绝对正确”。形式证明只能说明程序满足给定规范，而规范本身可能误解人的意图，也可能漏掉真实世界的重要条件。物理设备、传感器、组织行为和开放环境也很难被完整装进一个形式系统。可是，限制并不取消方向：人类仍然可能从主要依靠经验信心，转向在越来越多环节要求清楚的假设、边界和可证明保证。
AI 本身也会成为这种数学化要求的对象。能力越强的机器，越可能被用于高速交易、工业控制、科研决策、基础设施和自主行动；社会因而不仅关心它“平均表现不错”，还会要求知道它在哪些条件下不会越过安全边界，受到扰动时会怎样，修改一部分程序后哪些性质仍能保持。AI 大幅降低复杂系统的生成成本，AI4MATH 又可能被用来约束和检查这种复杂性。科学技术向来是双刃剑：同一种能力既能扩大风险，也能提供降低风险的工具。
对于一般的科学研究，在数学能力变得廉价以后，人类可能提高对“理解一个现象”究竟意味着什么的标准。今天许多科学结论带有不得已的局部性：模型在某个范围内有效，却未必系统知道它在哪里失效；几个理论都能拟合数据，却未必清楚现有实验能否区分它们；一个数值结果看起来稳定，却未必完整追踪了实验误差、参数不确定性和近似误差怎样传到最终结论。
这些问题并非无人关心，但往往是彻底追究的成本太高。假如符号推导、反例搜索、灵敏度分析、误差传播、可识别性分析和证明检查都便宜许多，科学中的一些“奢侈要求”就可能变成日常要求：哪些结论来自哪些假设，模型的适用范围在哪里，误差上界是多少，两个理论究竟需要什么实验才能区分，哪些观察结果是某个理论绝不可能解释的。AI4MATH 的正面意义未必只是让科学家更快得到答案，也可能是让人类更不满足于一个勉强能用的答案。
当然，更低的生成成本也可能带来更多貌似严谨却缺乏理解的结果、如洪水一般激增的文献和艰巨的审查负担。正因为科学技术总是同时带来新的能力和新的问题，这里没有一条单向的乐观道路。可以较有把握的是，数学能力一旦变得廉价，人类就有机会把从前过于昂贵的精确性、可靠性和理解深度纳入普遍要求。
四、严格数学训练会不会向更多职业扩散这就引出了就业讨论中最容易被忽略的一层。职业数学家的岗位可能收缩，并不等于社会只需要更少经过严格数学训练的人。许多职业的核心并非数学研究，却大量使用由长期严格数学训练塑造的能力：理解抽象结构，追踪假设与结论的关系，判断模型是否适用，识别一个证明究竟保证了什么，以及在不确定条件下保持定量约束。
未来的芯片工程师也许不必亲自完成大部分证明，但仍可能需要理解证明覆盖了哪些情况；生物研究者可能依靠 AI 推导模型，却仍要判断参数是否可识别、数据能否支持结论；软件工程师可以让机器生成形式化证明，却必须知道规范有没有漏掉关键行为。这里需要的不是更多职位名称叫作“数学家”的人，而是更多能够在本职工作中理解、提出和审查数学要求的人。
于是，“AI 会做数学”与“人不必学很多数学”之间并没有直接推论。数学计算和证明越容易获得，社会反而越有可能把原本凭经验完成的工作提高到需要读懂数学结果、判断数学结果和提出数学约束的水平。假如这种扩张足够广泛，严格数学训练的需求可能从少数专门岗位扩散到工程、科学、人工智能、安全、金融、医学和公共决策等更广的职业之中。数学系毕业生的主要去向，也可能越来越不是传统意义上的数学职业，而是这些被进一步数学化的行业。
AI 很可能成为所有人接受数学教育的主要工具。它可以提供个性化讲解、生成练习、即时反馈，并帮助学习者跨越许多过去依赖教师反复示范的技术障碍。这会减少一部分传统教学工作，却也可能让更高水平的数学训练覆盖更多人。教育的组织方式和就业结构因此会改变，但“由谁讲授数学”和“社会是否仍需要人形成数学能力”是两个不同问题。
这种前景同样不能被写成必然结局。AI 也可能继续接管规范生成、结果解释和错误诊断，企业还可能满足于足够便宜的“差不多正确”，而不是为更高标准投入资源。界面变友好，部分岗位对数学训练的门槛也可能下降。最终结果取决于两个速度：机器替代人的数学活动有多快，社会提高数学要求、扩大数学应用又有多快。
因此，高校数学系真正需要关注的，不只是未来还有多少专门数学岗位，而是未来有多少职业仍要求劳动者拥有经过严格数学训练形成的判断力。这个问题目前没有确定答案，却比简单追问“Lean 能创造多少职位”或“AI 公司会招多少数学家”更接近数学教育的长远处境。
五、机器化数学能力会怎样分布数学能力变成基础设施以后，还会出现另一个不能回避的问题：这种能力究竟会以什么结构分布。
一种可能是高度集中。训练前沿模型需要先进芯片、数据中心、能源、网络、数据和长期研发，少数大型企业、国家实验室或平台因此可能长期保持明显优势。大学、企业和个人若要获得最强的数学能力，只能向它们购买服务；价格、访问资格、使用规则和平台政策便会影响哪些研究能够开展、哪些机构能够竞争。[3]
另一种可能是广泛扩散。AI 推理成本近年来快速下降，较小模型、开放权重模型和大量开源工具不断进步；Lean 一类开源证明助理可以由普通机构自行部署，形式证明还能够由相对小而透明的内核检查。[4][8] 即使最前沿训练仍然集中，相当强的日常数学能力也可能像编译器、数值软件和密码库一样广泛分布。那时不一定还有哪个组织能够完整“控制”机器化数学能力。
更可能出现的也许是混合结构：最强模型和大规模训练能力集中，足以承担大多数教学、工程与普通研究任务的能力却不断扩散；某些专门领域依赖封闭平台，另一些领域则由开放模型、公共算力、学术软件和社区维护的知识库支撑。集中与扩散甚至会同时加强，而不是一方简单取代另一方。
数学界没有权力控制数学能力的分布模式，而且未必存在一个可以被单一主体控制的对象。更实际的问题是：不同主体能够获得什么水平的模型，能否本地部署、审查和修改，关键证明能否由独立系统复核，中小机构与大型平台之间的能力差距会扩大还是缩小。
这既是经济问题，也是知识生产的制度问题。假如大学只能租用外界大型平台的前沿服务，研究自由就会部分取决于平台规则；假如开放模型、公共计算平台和可独立验证的形式化工具足够强，机器化数学也可能削弱传统的知识门槛，让更多机构和个人进入原本难以承担的研究。这两种事情都有苗头。
六、数学系与数学共同体对高校数学系而言，一种过度的反应是把职业数学家的岗位风险直接写成数学训练失去价值，甚至写成人类数学活动的终结。AI4MATH 更可能迫使数学系同时面对收缩和扩张：一些传统任务会减少，数学严谨性却可能进入更多行业；教学中的讲解与练习会被机器分担，社会却可能要求更多人具备理解数学的能力。
这意味着数学教育的重心不能只是教学生比机器更快地完成标准推导，也不能简单追逐几个短期热门方向。严格训练仍然要保留，否则很难形成可靠的数学判断；但训练的目标会偏向能否看清问题的结构，能否理解一个结论依赖什么假设，能否把现实问题转化为适当的数学对象，并在机器给出答案以后知道应当相信到什么程度。这里不是企图把“判断力”宣布为人类永远不可替代的领地，而是认为在可见的转型时期，真正理解数学仍是有效使用、检查和约束 AI4MATH 的重要前提。
科研制度也会受到影响。论文、申请书、报告与代码的生成成本下降以后，“看起来像科研”的材料会急剧增加，而数学中的真实劳动本来就难以从外部观察。若管理者只是增加论文数量要求、阶段验收和机器化筛查，研究者就会更有动力生产可见材料、回避高风险问题，最终走向 AI 写申请、AI 审申请、AI 生成评价这样荒谬的、脱离人而自行运转的系统。规模化科研欺诈在生成式 AI 普及之前就已经以假乱真，AI 很可能进一步削弱传统信号的分辨力。[9]
这并不意味着数学共同体应当拒绝评价和责任，也不意味着所有失败都应自动得到保护。它意味着，当机器能够廉价制造形式完整的成果时，数学界更需要诚实承认评价的不确定性，避免用伪精确的排名掩盖有限的信息。同行讨论、长期声誉、可复核的证明与开放的研究过程可能变得更重要。
最后还要把数学的社会使用、数学工作者的生活来源和人类为什么继续做数学分开。即使外部社会只需要较少的职业数学家，人类仍可能因为求知、教育、文化连续性和共同体生活而继续研究数学；而即使大量人在其他行业工作，他们也可能依靠 AI、开放文献、研讨网络和共同基金保持数学活动。这样的共同体不能被浪漫化：住房、医疗、育儿和照护会使“业余做数学”具有强烈的阶层差异，年轻人最需要支持时往往最没有资源。公共教育、大学职位和稳定资助仍然具有不可替代的意义。
但问题已经不只是“社会还需要多少数学家”。它还包括：社会是否需要大量经过严格数学训练的人进入其他职业，机器化数学能否向普通机构和个人开放，以及无论职业结构怎样变化，人类是否仍然愿意让数学作为人类文明的一种荣耀继续存在。
七、结语：数学的繁荣与数学职业的繁荣不是同一件事AI4MATH 最深的影响，也许不是机器在某个基准上超过多少人，而是它使数学能力逐渐脱离少数劳动者的长期训练，成为可以复制、部署和调用的基础能力。这会同时触发替代、扩张和重新分布，最终结果难以预料。
如果替代效应占主导，完成数学任务所需的人会显著减少，职业数学家和许多高度数学化岗位可能收缩、集中和极化。如果扩张效应足够强，软件、机器、AI 和科学研究会提出比今天高得多的精度、可靠性与理解要求，许多职业反而需要更多经过严格数学训练的人。即使第二种情况发生，这些人的职业名称也未必与数学有关，他们的大部分具体推导还可能由 AI 完成。
机器化数学能力的分布同样没有定局。最前沿能力可能依附于大型平台而集中，广泛可用的能力也可能通过开放模型、廉价推理和形式化工具迅速扩散。集中会制造新的依赖和权力差距，扩散则可能降低研究与教育门槛；二者完全可能长期并存。
因此，数学重要，不等于职业数学家稀缺；AI 能做数学，也不等于人不再需要严格数学训练；形式验证和数学建模的普及，不保证产生同等规模的专门岗位，却可能使整个技术文明比今天更加数学化。科学技术向来如此，AI4MATH 不会只带来好消息或坏消息。它既可能压缩旧的职业空间，也可能让人类追求过去无法负担的严谨、可靠和理解。
高校数学系真正需要面对的，不是怎样用一条乐观叙事抵消一条悲观叙事，而是看清几个已经开始分离的问题：机器和社会会怎样使用数学，未来还有多少职业需要严格数学训练形成的能力，职业数学共同体能够维持怎样的规模，以及机器化数学究竟会集中在少数组织手中，还是成为广泛可得的公共能力。
数学作为职业的黄金时代未必到来，数学作为文明能力的扩张却近在眼前。最值得期待的是，人类能够借助廉价的数学能力，把更多事情做得更好、更安全、更清楚，并继续知道自己为什么相信一个结论。
参考资料- Google DeepMind, [Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad]https://deepmind.google/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/, 2025；Google DeepMind, [Accelerating Mathematical and Scientific Discovery with Gemini Deep Think]https://deepmind.google/blog/accelerating-mathematical-and-scientific-discovery-with-gemini-deep-think/, 2026；OpenAI, [Our First Proof submissions]https://openai.com/index/first-proof-submissions/, 2026。相关结果包含人工提示、筛选和专家复核，不应被直接解释为 AI 已经独立承担完整数学研究。
- Acemoglu, D. & Restrepo, P., [Automation and New Tasks: How Technology Displaces and Reinstates Labor]https://www.aeaweb.org/articles?id=10.1257/jep.33.2.3, Journal of Economic Perspectives, 2019。
- OECD, [Competition in Artificial Intelligence Infrastructure]https://www.oecd.org/en/publications/competition-in-artificial-intelligence-infrastructure_623d1874-en/full-report.html, 2025。
- Lean, [Lean Programming Language and Theorem Prover]https://lean-lang.org/；Lean Focused Research Organization, [About the Lean FRO]https://lean-lang.org/fro/about/；中国科学院软件研究所，[2026 年博士后招收计划]https://is.cas.cn/rcdw/bshldz/tzgg/202603/t20260323_8174643.html。具体招聘只能说明方向真实存在，不能单独用于估计整体就业规模。
- 国家统计局，[中华人民共和国 2025 年国民经济和社会发展统计公报]https://www.stats.gov.cn/sj/zxfbhjd/202602/t20260228_1962662.html，2026；教育部，[2025 年全国教育事业发展统计公报]https://www.moe.gov.cn/jyb_sjzl/sjzl_fztjgb/202607/t20260706_1442870.html，2026。
- Kuhn, D. R., Chandramouli, R. & Butler, R. W., [Cost Effective Use of Formal Methods in Verification and Validation Foundations]https://www.nist.gov/publications/cost-effective-use-formal-methods-verification-and-validation-foundations, NIST, 2002；AWS, [Lean Into Verified Software Development]https://aws.amazon.com/blogs/opensource/lean-into-verified-software-development/, 2024。
- Stanford Institute for Human-Centered AI, [The 2025 AI Index Report]https://hai.stanford.edu/ai-index/2025-ai-index-report, 2025；[The 2026 AI Index Report]https://hai.stanford.edu/ai-index/2026-ai-index-report, 2026；OECD, [Artificial Intelligence Markets]https://www.oecd.org/en/publications/artificial-intelligence-markets_d531d73f-en/full-report.html, 2026。这些资料同时呈现了前沿训练成本、市场集中、推理成本下降与模型生态扩大的趋势。
- Richardson, R. A. K. et al., [The entities enabling scientific fraud at scale are large, resilient, and growing rapidly]https://www.pnas.org/doi/10.1073/pnas.2420092122, PNAS, 2025。转自微信公众号 https://mp.weixin.qq.com/s/BneBOy_tunW_WZtqBVPaUw
https://blog.sciencenet.cn/blog-81613-1553068.html
上一篇：OpenAI“解决” Navier–Stokes 千禧年问题的完整来龙去脉：从前人思想、技术突破到 credit 争议
