十九世纪数学经历深刻变革，霍华德·斯坦（Howard Stein）称其第二次诞生；马克·吐温（Mark Twain）说死亡报道夸大。我近期参加汇聚研究（Convergent Research）支持的科创会议，该组织监督精益 FRO（Lean FRO）开发精益定理证明器（Lean theorem prover）的非营利机构。会上我以数学家身份自我介绍后，众人急于探讨近期 AI 对数学的影响及学界反应。他们惊讶我认为博客回应积极，尽管日常工作将变。这些讨论助我形成分享想法。

“十九世纪数学经历深刻变革，堪称学科的第二次诞生——第一次在古希腊。”出自 Howard Stein 的论文《Logos, Logic, and Logistiké: Some Philosophical Remarks on Nineteenth-Century Transformation of Mathematics》

马克·吐温：“我死去的报道被夸大了。”

“愿你们生活在有趣的时代。”（传统谚语）

我近期参加了一个由 Convergent Research 支持的科创初创会议，该组织监管开发 Lean 定理证明器的非营利 Lean FRO。会上我以数学家身份自我介绍后，许多人想谈 AI 近期对数学的影响及学界反应。他们惊讶地发现，我认为如本博客和 Proofs and Prompts 上的社群回应总体积极鼓励，尽管我们都承认日常工作必将改变。这些讨论帮我形成了此处分享的想法。

对数学家工作的狭义看法体现在日常流程：解题，太难就做简化近似再调参数。近几个月的事件打破了这习惯，因为一年前能发论文的结果现在用 AI 轻易生成。这让我们担忧未来做数学的意义，以及如何培养下一代数学家。

数学史给出更广阔视角。数世纪变化中稳定的是：数学是严谨推理与交流的文化，提供语言和抽象让我们可靠高效思考沟通。AI 时代这种推理仍重要。数学的美感不减其实用，反而由此解释：做数学愉悦或因它练就物种生存基本能力，写入 DNA。若如此，数学思想不会消失。

挑战在于，让 AI 解题使我们数十年来解题与增进数学理解脱钩。问题不是是否还需数学，而是 AI 时代如何追求理解。我给三个总体回答。

解决更难的问题

当今基础模型两个显著特征：一是已读遍数学文献，二是不知疲倦；智能体群尝试无数变体找解。这解释了为何 AI 生成的开放问题解都有相似特质：AI 能拼凑现有技法治愈的问题（感谢 Matthew Ballard 此描述及分析）。

每个有趣数学问题都能这样回答吗？可能不，即便能，也可能有更新颖满意的解需新见解。近未来 AI 或能想出，但至少我们还未到那步。强化学习训练让系统连惯常步骤，从成败史学哪些最有希望。行动价值仅按最终轨迹成功评定，催生超人巧妙却可能缺创造与高层策略。无论如何，仍有难题和宏大研究计划，AI 助进展令人兴奋。

想更大的念头

若数学是外星人强加的习题考试，现状更令人沮丧。幸好我们做数学时能选题、评解、偏爱最佳。我们定何为有趣、追何问、为何。命运在手。

数学中最羡之物常如天降。1853年青年伯恩哈德·黎曼向导师卡尔·弗里德里希·高斯提交三个候选题目供其就职讲座选，高斯据报选了黎曼准备最少的，想看其发挥。该讲座《论几何基础之假设》1868年遗著出版，革新领域。它区分空间度量与拓扑性质，引入流形一般概念（后者至20世纪才严格）。关注空间内在性质（黎曼几何中由度量定、独立于嵌入）是数十年后爱因斯坦广义相对论关键。黎曼几何应用超黎曼想象，从机器人、医学成像到统计分析。

William Ewald 的文献集 From Kant to Hilbert 引费利克斯·克莱因描述：“[黎曼讲座]出版时我正独立钻研数学，仍鲜活记忆其思路对当年青年数学家的冲击。我们觉昏暗难解却深不可测，而现代数学家自幼吸收，只赞清晰多产。”

青年克莱因觉昏暗者今成经典，基础模型如青年数学家般训练吸收。再谢 Ballard 举此例并指出无强化学习能评黎曼决策：益处弥散难追踪，时间跨度太长。

无数数学发展开新视野者同理，如伽罗瓦着眼置换群解代数方程、庞加莱动力系统定性研究、格罗滕迪克深远概念创新。AI 终能此类进展？此问不当。告之某 AI 吐出对其同类有趣的定理于我无益。我们仅在结果对我们有趣重要时在乎 AI，终由我们定意。数学发展的价值嵌于历史文化。

试想阿拉斯加荒野背包行：或乐让 AI 订机票，但不愿 AI 代徒步发照。数学攸关非娱乐，而是推理抉择的能动性。无论 AI 能否思，不能代我们思。我们有自己的生活；数学是我们讲述的故事，如何讲述由定。有 AI，探索更多，发现途径不缺。

尝试新事物

迄今我聚焦用 AI 助做旧事，但勿忘技术本身提新问题，我们需学高效用。我另文（将刊 Notices of the AMS）主张数学家应积极参与理解技术，想新法做新数学。

AI 改变数学之意非无先例。17世纪代数解几何是新技，非人人喜；然我们掌握并高效用。同世纪无穷小微、19世纪代数结构、20世纪初集合抽象结构语言、近数值符号计算皆然。新时皆陌生不安。应视投入证明辅助与神经网络助发现数学者为做数学，而非仅技术员。AI 时代，发展符号自动化或训神经网络贡献不逊手动推证定理。

闻辩称就业紧缩应内守传统技能。相反，我认为参与新技术学用之增推理发现能保学科强。拓宽数学观是扩职业保相关最佳法。

给下一代的信息

我对未来乐观及浅议解难题、想大念、试新物，难慰脚下地动的学生和早期职业研究者。我言非淡化挑战或给易应。数学系、领袖、教育者、学会、期刊编委会正开紧急会拟具体建议行动。任务艰巨。

虽不确定，可给下一代清晰信息。一、我们与你们同在。无重于学科健康强盛及保你们繁荣。我们谦认经验专有限，昔以为知者已不验。承诺尽力合作保职业强。

二、数学今仍重要，需你们。AI 不可代我们集体推理抉择力，数学仍是核心能力。无法想象数学不居生活要位之世。

三、未来几年极有趣。我们处新前沿，共同规范价值期望崩解，替何由共定。信未来史家视此为新数学纪元始，量我们行决后果。数学从来非怯者事；此乃我们奋起面挑战之机。

社区普遍承认 AI 在数学证明上进展迅速，但分歧在于应全力推进 AI 自我迭代、警惕无监管导致人类被霸权支配，还是更重视人类数学教育与底层工具链的真实贡献。

认为 AI 解决数学难题是必然且 AI 理解优先于人类

• 反驳怀疑论关于 AI 缺乏新颖洞察的看法，指出 AI 已解决复杂任务乃至千禧年问题，生成定理是推进前沿的方式，AI 数学理解比人类重要得多。（认可度：少数人） > 人工智能持续解决更复杂任务甚至千禧年问题，其对数学的理解比人类重要百万倍。（@charcircuit）

警告无监管 AI 将全面超越人类并造成霸权

• 厌倦谨慎乐观，主张若无监管 AI 必然在所有领域超越人类，使无权控制模型者彻底无力、经济冗余，诚实讨论此风险是必要的。（认可度：少数人） > 若无监管，人工智能必在各领域超越人类，令无权者彻底无力、经济冗余并受制于 AI 霸权，回避即是欺骗。（@atleastoptimal）

强调提升人类数学理解与教育比追逐定理更重要

• 认为数学目的在促进人类理解，AI 自动化证明后，下一前沿应是教学性以提升大众素养；有应用数学学生表示原文鼓励数学不可替代让其安心。（认可度：较多人） > 若数学旨在促进人类理解，提升大众数学素养比追逐又一定理羽毛更重要，尤其当 AI 能自动采摘时。（@drivebyhooting）

认为真正突破应归功于 Lean 与 Mathlib 而非大语言模型

• 指出当前自动证明进展过多归功大语言模型，实则是 Lean 语言设计与 Mathlib 生态结合之功，其他证明器栈未见同等突破。（认可度：少数人） > 若非 Lean 与 Mathlib 的特定组合，此类进展恐难实现，自动定理证明器并不新鲜却未在其他技术栈突破。（@nylonstrung）