科学网—AI 4 Math：数学研究的工作流、边界与实践
精选
已有 213 次阅读
2026-6-10 23:27
| 系统分类: 科研笔记
AI4Math：数学研究的工作流、边界与实践 今天在学院午餐会上做了个 AI4Math 的分享，以下是演讲稿全文。
各位老师，大家中午好！
非常感谢学院给我这个机会和大家交流。说实话，接到这个分享任务时，我心里是有些忐忑的。因为我知道，我们学院很多老师在 AI 的使用和探索方面都走在我的前面。今天我更多是抱着抛砖引玉、交流学习的心态，和大家分享一些自己的观察与体会。
我计划用大约 30 分钟的时间做一个简短汇报，后面预留更多时间，期待和各位老师一起讨论交流。
我今天分享的题目是：
AI4Math：数学研究的工作流、边界与实践 首先说明一下，今天并不是一个严格意义上的学术报告，更像是一场经验分享。过去一两年里，我也一直在学习、尝试和摸索如何把 AI 融入教学、科研和项目工作之中。因此，今天谈到的很多内容并不是最终结论，而是我在使用 AI 做数学研究、撰写论文、申请项目、修改材料以及指导学生过程中积累的一些观察、思考和实践经验。
首先想和大家分享一个学界和业界已经达到共识的观点：
AI 可能正在成为第四次工业革命的核心驱动力 最近有一句话让我印象非常深刻。李开复老师说：
AI 是我们 几十辈子 难得一遇的机遇。
无论我们是否已经准备好，AI 都正在深刻改变科研、教育、产业乃至整个社会的运行方式。而对于数学工作者来说，一个值得思考的问题是：
AI 到底会如何改变数学研究？
今天的分享，也将围绕这个问题展开。
我先说结论：
AI 不是数学的终点，而是数学研究工作流的一次变化。
为什么这么说？
现在很多讨论会走向两个极端。一个极端是神化 AI，认为数学家马上就要失业，以后按一下按钮就能自动出定理。另一个极端是完全不相信 AI，觉得它只会胡说八道，对严肃数学没有意义。
我的看法在中间。AI 当然会犯错，而且会犯很隐蔽的错误；但是它也已经强到不能被忽视。它不只是帮我们写邮件、排 LaTeX，而是开始进入猜想、构造、证明、验证、写作这些数学研究流程中的关键环节。
所以今天我想讲的核心问题不是“AI 会不会取代数学家”，而是：
数学家应该怎样使用 AI？怎样理解它的边界？怎样把它变成提高我们教学、科研、论文和项目质量的工具？
第一部分：AI4Math 的 AI，不只是大语言模型 
今天我想交流的是 AI4Math 。这里的 AI 不只是 LLM，也包括 Lean 这类形式化证明系统，机器学习方法，以及现在越来越多的智能体系统。
首先，我想澄清一个概念。今天说 AI4Math，这里的 AI 不是只指 ChatGPT，也不是只指某一个模型。
它至少包括四类东西。
第一类是大语言模型，比如 GPT、Claude、Gemini、DeepSeek、Qwen 等。它们适合做自然语言推理、生成证明草稿、讨论思路、修改论文、整理文献。
第二类是形式化证明系统，比如 Lean、Coq、Isabelle。这类工具的目标不是“猜”，而是把证明写成机器能逐步检查的形式。
第三类是机器学习和搜索方法，比如图神经网络、强化学习、SAT、ILP、自动搜索。这些方法在构造反例、寻找小阶结构、优化配置时非常有用。
第四类是智能体系统，也就是 agent。它不只是回答一句话，而是能够拆任务、调用工具、写代码、跑实验、继续迭代。
所以 AI4Math 不是单一工具，而是一整套数学研究工具链。
我们以前做数学，常见的工具是纸笔、黑板、讨论、文献、计算软件。现在工具箱里多了一组新的东西：LLM、Lean、搜索、agent。真正的变化不是多了一个软件，而是研究工作流开始变化。
第二部分：数学并不保守，但数学对工具要求极高 表面上看，数学这门古老学科似乎变化不大。现在的数学家仍然像两千多年前的阿基米德一样，很多时候还是靠纸笔、黑板和讨论进行研究。
这有一部分是真的。今天我们讨论一个证明，核心体验和古希腊时代并没有完全不同：还是要看定义、看结构、看逻辑链条。
但另一方面，数学其实一直在吸收工具。
吴文俊先生做机器证明，这是非常重要的传统。四色定理用了计算机辅助证明。后来我们有 Mathematica、Sage、SAT、ILP、Coq、Lean。这些工具本来就一步步进入了数学研究。
只是过去很多工具更多是在帮我们“算”。
现在的新变化是， AI 开始帮我们“想”。
迅猛发展的AI开始进入“猜想、构造、证明、验证”这些更接近数学核心的位置。
第三部分：最近数学界的地震
最近数学界发生了一场不小的“地震”，而震中恰恰就在组合数学。某种意义上说，我们就站在震中附近。
这张时间轴展示了最近几个月 AI 在数学研究中的几个标志性事件。
2026.02 ：Gauss 系统完成了球堆积问题的形式化验证。这是第一个被完整形式化验证的菲尔茨奖级成果。
2026.04 ：北大 AI4Math 团队（董彬、刘若川、肖梁等老师）利用“双智能体”框架攻克了 Anderson 猜想。一个智能体负责自然语言推理和文献检索，另一个负责 Lean 形式化验证，两者协同工作，最终解决了交换代数领域的重要猜想。
2026.05.08 ：菲尔兹奖得主 Gowers 分享了自己使用 GPT-5.5 Pro 的经历，并展示了 AI 在短时间内完成研究级数学探索的能力。
2026.05.20 ：OpenAI 模型给出了 Erdős 平面单位距离相关长期猜想的反例构造，引发了数学界广泛关注。
最后这件事尤其震撼。
这个问题其实很容易描述：在平面上放置 n 个点，最多能有多少对点之间的距离恰好等于 1？
几十年来，数学家们积累了大量构造和理论，对这个问题形成了相对稳定的直觉。很多人相信，类似方格或者晶格结构的构造已经非常接近最优。
然而，OpenAI 的模型却提出了一种全新的构造思路，并由此产生了反例。随后，数学家们对相关证明进行了整理、补充和验证。
这件事对组合数学和图论的人冲击很大。因为这场“地震”的震中，就在我们的学术邻域之内：离散几何、组合、极值构造，这些方向和我们平时做的问题非常接近。
无论我们是否愿意承认，AI 已经开始改变数学研究的生态。
2026年6月（Leipzig Benchmark 莱比锡基准） 还有一个前几天的最新消息，就是 Leipzig Benchmark。
数学家们组织了一个面向研究级数学问题的基准测试，一共设置了 100 道题。第一阶段，5 个前沿模型各尝试一次之后，还有 41 道题完全没有解出；第二阶段，对表现较好的模型进行多次尝试，未解题数量降到了 16 道；最后再使用 deep-thinking 模型尝试，最终只剩下 2 道题没有被解决。
当然，这个结果不能简单理解为 AI 已经能够完成 98% 的数学研究。因为题目类型、答案形式、提示方式、重复尝试次数等因素，都会影响最终结果。
但它至少说明了一点：研究级数学问题，已经不再天然位于 AI 能力之外。
上面这张是会议照片。顺便说一句，这次会议就在我读博士时所在的马普应用数学所举行。看到照片里熟悉的办公室，以及很多老同事、老朋友，我感到非常亲近，也有一点自豪。
目前大家比较公认的一点是：如果讨论的是数学、物理等需要深度推理的问题， GPT 5.5 基本处于第一梯队；如果是大量编程和工程开发任务， Claude Code 往往更有优势。当然，模型迭代非常快，这个结论可能几个月后就会发生变化。这个时代最大的特点之一，就是不要低估 AI 进步的速度。
下面是这 100 道题的领域分布，其中代数几何和代数组合所占比例最高。
第四部分：Lean 与形式化证明 
接下来讲一下 Lean 和形式化证明。
如果要追溯机器证明在中国数学界的传统，我们可以从吴文俊先生讲起。吴文俊先生很早就推动了机器证明，尤其是在几何定理机器证明方面做出了奠基性贡献。今天我们讨论 Lean，其实也是这一条“ 数学证明能否被机器严格验证 ”路线在新时代的延续。
如果说 LLM 更像一个可以用自然语言交流的数学合作者，那么 Lean 更像一个非常严格、甚至有些“不近人情”的证明检查器。
Lean 的好处非常直观：如果一个证明被写进 Lean，并且通过了检查，那么它的每一步都必须符合形式逻辑规则。它不依赖审稿人的直觉，不依赖作者的自信，也不依赖“这一步应该是显然的”这种数学写作习惯，而是由机器逐步验证。
这件事未来很可能会影响数学论文的 审稿方式 。尤其是关键定理、长证明，以及那些容易出错的技术性 lemma，如果能够形式化，结果的可信度会大幅提高。
当然，Lean 也不是万能的。不同数学领域在 Lean 里的成熟程度差别很大。基础代数、逻辑、初等数论，以及部分分析方向，目前相对成熟；但组合数学、图论、动力系统、PDE，以及很多几何问题，形式化基础仍然不够均衡。
我们做图论的人对此会有很强的体会。很多图论问题定义高度定制，构造非常图形化，小阶反例很重要，证明中还经常包含大量局部变换。要把这些内容全部写进 Lean，成本非常高。
所以短期内，我并不认为每篇图论论文都需要 Lean 化。但我相信，未来重要结果的关键部分、标准理论，以及可复用的工具库，很可能会逐步形式化。
更现实的工作流可能是：LLM 帮我们生成证明草稿，人类数学家负责整理结构、判断方向、补全细节，然后对最关键、最容易出错的部分进行形式化验证。
在这一方向上，国际上陶哲轩等数学家已经做了很多探索。国内也有不少团队在推进相关工作，比如西湖大学陈华一老师，北大的肖梁、董彬、刘若川等老师，人大王善文老师，以及中国科学院的一些团队。
我们学院去年也请过王善文老师来做报告，题目是“人工智能与数学”，时间是 2025 年 6 月 20 日，地点就在现在的 M315。当时王老师和北大、人大 AI4Math 团队的几位学生也来了。他们当时的一个重要目的，是希望组织我们学院的学生参与 Lean 形式化方面的工作。
不过很有意思的是，仅仅一年时间，形势又发生了很大变化。去年很多 Lean 形式化工作还需要学生一行一行手写；但今年，随着 AI 工具的发展，很多基础性的 Lean 代码生成和修改工作，已经可以由 AI 辅助完成了。
2025.6.20 M315
报告标题：人工智能与数学
报告人：王善文（中国人民大学）
第五部分：数学家的价值和品味 这里我想讲一个我认为非常重要的观点：
数学家的价值不只是证明定理。
当然，证明定理是数学家的核心工作。但数学家还要做很多更上游的事情。
比如提出好定义。一个好定义可能比一个局部定理更重要。
比如选择好问题。一个问题值不值得做，有没有结构，有没有可能发展成理论，这需要判断。
比如找例子。数学里面很多理论都是从好例子开始的。
比如把局部技巧组织成理论，把一个结果讲成共同体能理解的故事。
历史上很多伟大数学家的贡献，不只是某个证明，而是他们改变了大家看问题的方式。
所以 AI 越能做局部推理，数学家的品位越重要。
我想用一句话说：
AI 让尝试变便宜了，于是判断变得更贵了。
以前我们做一次尝试很贵，要查文献、写代码、推 lemma、改稿子。现在很多尝试可以让 AI 很快给出来。问题是，尝试多了以后， 怎么判断哪条路值得走？哪个例子有结构？哪个 lemma 是真的？哪个结果可以发展成理论？
这仍然是数学家的核心价值。
第六部分：AI 在数学研究工作流中到底怎么应用？
数学研究大概可以拆成八个环节。
第一，问题选择。 第二，文献调研。 第三，探索和实验。 第四，猜想与构思。 第五，证明拆解。 第六，AI 辅助证明与计算实验。 第七，验证与检查。 第八，论文写作、组织与修改。
在这八个环节里，AI 所能发挥的作用并不一样。
问题选择 主要还是依靠人类。AI 可以帮我们列出很多问题，但它并不知道什么问题真正值得投入几年时间，也不知道什么问题在一个领域中具有长期价值。
文献调研 方面，AI 非常有用，但一定 会有遗漏 。尤其是数学文献，一个关键引理可能藏在二十年前某篇论文的中间。AI 给出的文献线索可以作为起点，但最终还是要查阅原文。
探索和实验 方面，AI 的作用越来越明显。它可以帮助我们写程序、跑小阶例子、寻找反例、生成数据，也能帮助我们快速比较不同思路的可行性。很多时候，AI 不一定直接给出答案，但能够帮助我们更快排除错误方向。
猜想与构思 方面，AI 很有启发性。它擅长做类比，也擅长提出“这个问题也许可以借助某某工具”的建议。当然，十个建议里可能九个都不靠谱，但只要有一个有价值，就已经很值得。
证明拆解 方面，AI 可以帮助我们把一个大目标拆解成若干 lemma 或中间步骤。但它经常会提出一些看似合理、实际上难以证明甚至错误的中间命题，因此仍然需要人来判断。
辅助证明和计算实验 方面，AI 对短证明、局部论证、小阶搜索和计算实验都很有帮助。但对于真正复杂的长链条证明，目前仍然不够稳定。
验证与检查 方面，AI 很有价值，但不能过分依赖。它能够发现一些错误，也可能漏掉一些非常严重的错误。
我本人曾经测试过，我知道某篇已发布的论文中有个重要漏洞，但是让AI检查没有找出来。然后我告诉它，这里有个漏洞，它发现并且补齐了。
所以最终的正确性责任仍然在数学家自己身上。
论文写作 方面，对我个人而言 AI 非常有帮助。它可以帮助整理结构、润色语言、修改摘要、画图。但同时也存在风险：语言容易变得过于“AI 化”，看起来很流畅、很漂亮，却缺少个人风格，或者是不符合本领域的惯例，所以后期还需要很多人工的工作。
如果借用 Stanford 提出的 Human Agency Scale，也就是 H1 到 H5 的人类主导权量表
H1 是 AI 独立完成，例如简单排版、格式转换。
H2 是 AI 主导、人类少量介入，例如初稿整理。
H3 是人机平等协作，例如文献梳理、证明路线讨论。
H4 是人类主导、AI 持续辅助，例如复杂证明拆解。
H5 是必须由人类全程主导，例如选题、原创理论、学术判断以及最终证明责任。
数学家 整体核心工作归属于 H5 ；
日常打杂、计算、排版等基础工作落在 H1/H2；
常规研究协作属于 H3/H4；
原创理论、攻克难题这类核心价值环节，牢牢锁定在 H5（人类不可替代） 。
第七部分：本科生汤泉宇案例——AI 放大有准备的人的能力
接下来讲一个最近澎湃和返朴报道的案例：西安交通大学本科生汤泉宇同学的故事。
这个故事很有意思，也很有启发，但同时也很容易被误读。
如果简单地把它理解成“一个本科生靠 AI 做出了前沿数学成果”，我觉得是不准确的。更准确地说，这不是一个“没有基础的人靠 AI 做数学”的故事，而是一个“ 有天赋、有准备的人，借助 AI 进一步放大能力 ”的故事。
汤泉宇并不是普通意义上的初学者。根据报道，在大规模使用 AI 之前，他就已经独立或与他人合作解决过多个 Erdős Problems 网站上的问题，也已经在数学研究中积累了相当多的经验。这说明他本身就具有很强的数学基础、问题敏感性和研究能力。
后来，在 AI 辅助下，他又推进和解决了一些新的问题。其中一个很有代表性的例子，是 Erdős Problem #650 。报道中提到，他和合作者借助 AI 推进了这个问题，并且最终通过 Lean 完成了形式化校验。更有意思的是，在这个过程中，陶哲轩也关注到了相关问题，并参与了讨论。汤泉宇相当于是抢在陶哲轩之前，给出了一个陶哲轩也在关注的问题的关键证明。
这件事当然很惊人。但我想强调的是，AI 在这里起到的作用，并不是凭空替代人的数学能力。AI 帮助他更快地搜索思路、尝试证明、发现可能的路线；但真正关键的环节仍然在人：他要判断 AI 输出中哪些是有价值的，哪些是错误的；要继续追问、修正、重组问题；最后还要把想法推进成真正可以被数学共同体验证的结果。
所以这个案例给我们的启发，并不是说：有了 AI，人人都可以轻松做前沿数学。
恰恰相反，它说明：
AI 放大的是有准备的人的能力。
没有扎实数学基础的人，仍然很难提出真正好的数学问题，也更难判断 AI 给出的结果是否有价值。相反，那些已经有良好数学训练、又能熟练使用 AI 的年轻人，可能会被 AI 极大放大。
这对我们学院的人才培养也很有启发。未来我们培养学生，可能不仅要训练他们掌握数学基本功，还要训练他们学会使用 AI，理解 AI 的能力和边界。也许在 AI 的赋能下，我们学院未来也有机会培养出这样一批学生：他们既有扎实的数学基础，又熟悉新的 AI 工具，能够更早进入前沿问题，更快参与真正的数学研究。
所以，汤泉宇这个案例最重要的意义，不是告诉我们“AI 可以替代数学训练”，而是提醒我们：
未来稀缺的，是既懂数学、又懂 AI 数学边界的人。
第八部分：几个具体场景（LLM） 我自己比较喜欢这样一个比喻：
LLM 就像一个很聪明的合作者。他可能拥有数学或者科学多个方向的博士生级别知识，知识面很广，反应很快，也能提出很多有启发性的想法。
但正因为如此，我们更需要多接触它、多使用它，逐步了解它真正擅长什么、不擅长什么，哪里可靠、哪里容易出错。只有了解它的能力和边界，才能更好地和它合作。
在这个过程中，我们不能把自己放在“学生”的位置上，被 AI 牵着鼻子走。相反，我们仍然要做“导师”：要提出问题、判断方向、检查细节、决定哪些结果值得继续推进。
所以，我的基本态度是：
AI 可以成为很强的数学合作者，但人类数学家仍然必须是导师和负责人。
下面我就介绍几个 LLM 介入数学科研的具体案例。
案例一（刘鸿及其合作者 ）：Turán 问题
第一个场景，是我昨天在一个报告中听到的。
昨天刘鸿老师在“黄大年茶思屋”做了一个非常精彩的报告，题目是：
AI 时代的数学：被超越，还是被增强？ Mathematics in the Age of AI: Outpaced or Augmented 报告人：刘鸿，韩国基础科学研究院首席科学家 时间：2026 年 6 月 9 日
这个报告中，刘老师分享了两个他自己的案例。其中第一个案例，正好是和我们学院丁老师的工作有关。
我想特别说明的是：这个结果并不是 AI 独立做出来的。恰恰相反，它首先是由数学家通过成熟的人工研究完成的。也就是说，核心定理、核心证明和主要数学思想，都是人做出来的。
AI 起作用的地方在后面。
在人已经完成这个结果之后，AI 因为另一个问题的启发，帮助把这个已有成果和一个新的应用场景联系了起来。也就是说，AI 没有替代数学家完成原创证明，但它帮助放大了这个人工结果的影响力。
案例二（个人）：生物数学问题 第二个场景，是我自己最近做的一个生物数学问题。
这个问题原来的上界是 O(r^5) 。后来我们通过把问题转化为图论中的某种顶点染色问题，把上界推进到了 O(r\log r) 。这一部分结果目前已经放到 arXiv 上，但还没有正式投稿。
更有意思的是，最近在和 AI 反复讨论这个问题时，AI 声称可以进一步做到线性上界，具体系数大约是 126。
当然，这个线性结果目前还没有完全验证，不能说已经成立。猜想的最优结果可能是 3r+1 ，也就是说线性是可能的，但常数应该还可以大幅压缩。
这里最有意思的地方，不只是 AI 给出了一个可能的更强上界，而是它帮助我们把原来的问题翻译成了另一个数学工具语言：从生物数学问题，到 O(r\log r) 的过程中翻译成的图的某种顶点染色方法，进一步在线性过程转化为图的某种边 list 染色方法。
这个过程再一次验证了：AI 在跨越数学内部不同方向时很有潜力。它不一定能直接完成最后的严格证明，但它有时能帮助我们发现“这个问题也许应该换一种语言来表达”，而这种语言转换本身，往往就是数学研究中非常关键的一步。
案例三（个人）：组合数学和图论真的要被AI干掉了吗？
最近有数学圈的朋友半开玩笑地问我：
组合数学和图论是不是要被 AI 干掉了？
第三个场景也是我自己的经历，不过不是成功经历，而是失败经历。也许这个失败经历，正好可以部分回答这个问题。
先说一下 Erdős。
Paul Erdős 是 20 世纪最高产、影响力最大的匈牙利数学家之一，也是离散数学、组合几何和极值组合领域的奠基人之一。他一生提出了数千个问题和猜想，许多到今天仍然深刻影响着组合数学和图论的发展。
Erdős 问题当然非常重要，也非常广泛。但需要强调的是，Erdős 问题只是组合数学和图论中的一部分，并不代表整个领域。
顺便说一句，我自己有一点小小的自豪：我的 Erdős 数是 2。因为我们陈老师是 Erdős 的合作者，他的 Erdős 数是 1，所以我的 Erdős 数就是 2。
但是图论和组合数学里，除了这些著名的 Erdős 问题，还有大量其他重要公开问题。我自己曾经用 AI 尝试过两个非常著名的猜想：
一个是 László Lovász 在书中提出的猜想。Lovász 是 2021 年 Abel 奖得主，也是现代图论和组合优化最重要的数学家之一。
另一个是 List Edge Coloring Conjecture，也就是边列表染色猜想。
这两个问题我都尝试过让 AI 帮忙推进，而且不是随便问一问，而是反复拆解、反复尝试不同路线。但结果很现实：基本啃不动。
即使我们现在有非常强的大语言模型，有领域内最好的数学家不断尝试，这类问题依然很难被 AI 推进。原因可能在于，这些问题本身可用工具太少，结构太深，计算空间又大得惊人。AI 很容易提出一些看起来像证明的路线，但真正检查细节时，往往会发现关键步骤根本站不住。
所以，从这个角度看，这其实是一件好事。
它说明，即使是在这次 AI “地震”的震中——组合数学和图论领域，也仍然有大量问题不是 AI 现在能够轻易“干掉”的。
AI 的确已经能帮助我们做很多事情，也能在某些问题上产生惊人的突破；但它距离真正系统性地取代组合数学家和图论学家，还有很长的路要走。
更准确地说，AI 不是要把组合数学和图论干掉，而是会迫使我们重新思考：哪些部分是重复劳动，哪些部分是工具搜索，哪些部分才是真正不可替代的数学判断和结构洞察。
案例四：LLM 以外的AI——数学智能体 除了直接使用 LLM，我们也尝试过一些专门面向数学研究的智能体。不过从我们的实际体验来看，目前效果还比较有限。
第一个是 Rethas 。
Rethas 是北大董彬教授 AI4Math 团队开发的数学专用自然语言推理智能体，是开源的。它可以和形式化验证智能体 Archon 配合使用，构成所谓的“双智能体协作框架”：一个智能体负责自然语言层面的数学推理和文献关联，另一个智能体负责 Lean 形式化验证。
我们在自己的图论问题上也尝试使用过 Rethas。它确实通过关联到一个代数定理，帮助我们解决了问题中的一个很小的例子。但也仅限于此，对整个研究问题的实质推进并不明显。
我猜测，一个重要原因可能是：图论相关文献、尤其是很多细分方向和技术性 lemma，在智能体当前能够有效调用的知识库中还不够充分，因此它很难真正进入问题的核心结构。
第二个是 HarmonicMath 推出的 AI 数学家 Aristotle ，中文可以叫“亚里士多德”。
Aristotle 是 2025 年底推出的数学专用智能体，因为独立破解 Erdős 问题 #124 这一 30 年悬案而受到关注。它目前没有开源，但任何人都可以在线试用：
https://aristotle.harmonic.fun/
我们尝试让它主动写 Lean 形式化证明，这个尝试没有成功。
我理解主要原因在于：图论需要的形式化基础目前还不够丰富，而且很多图论问题本身也不容易形式化。图论证明中经常涉及具体构造、局部变换、染色过程、小阶反例以及大量“看图就明白”的直观操作。对人来说，这些步骤可能很自然；但要把它们严格翻译成 Lean 可以检查的形式，成本非常高。
相比之下，Aristotle 这类智能体可能更适合那些已有形式化基础较好、知识库较完整、问题表达比较标准的方向。
所以，这两个尝试给我的体会是：数学智能体确实很有前景，但目前还远没有到“给它一个问题，它就能自动推进研究”的阶段。
第九部分：AI 的能力边界：少跳和多跳 引用 《知识分子》采访中马骁老师的说法：
可以用“少跳”和“多跳”理解 AI 的数学能力。
少跳问题，就是从条件到结论中间跳数不多。比如一个局部 lemma、一个短证明、一个标准技巧、一个反例构造。AI 很强。
多跳问题，就是需要维护很多对象、很多条件、很多不变量，证明链条很长。AI 目前仍然不稳定。
所以它最适合做什么？
适合做局部推理，适合做跨界联想，适合做重复试错，适合做证明草稿，适合做代码实验。
不适合完全交给它做长篇结构证明，不适合让它独立决定选题，不适合把最终验证交给它。
现阶段最合理的模式是：
人类主导方向，AI 扩大搜索；人类控制逻辑，AI 生成候选；人类负责验证，AI 辅助检查。
第十部分：未来数学工作场景 
陶哲轩曾经多次谈到，未来数学可能会越来越像实验科学：更多合作者，更多工具分工，更多快速实验，更多可复现的验证流程。
传统数学有一种“个人英雄式”的模式：少数几个合作者，贡献很难区分，很多工作依靠个人长期思考。
AI 时代可能会出现另一种模式：
有人负责提出问题；
有人负责理论框架；
有人负责计算实验；
有人负责形式化验证；
有人负责可视化和写作；
AI agent 负责大量搜索、整理、草稿与检查。
这不一定让数学变浅。相反，它可能让数学走向更深的问题，因为很多“苦工”可以被工具承担。
但还是那句话，大方向要由人判断。我的个人经验是，AI 容易走入局部，容易沿着错误方向越走越远，这时候我们要把它拉回来。
人类数学家的价值，会集中到更高层次的判断上。
第十一部分：Leiden Declaration：水能载舟，亦能覆舟
AI 进入数学，带来的不只有机遇，也有风险。
2026 年 6 月发布的 Leiden Declaration 提醒数学共同体：AI 正在挑战数学的一些核心价值，包括可靠性、署名、引用、开放性、同行评议，以及数学共同体对商业平台的依赖等。
这些问题并不抽象，而是会直接进入我们的日常研究。
比如，如果 AI 生成了一个证明，而这个证明后来被发现是错的，谁来负责？
如果 AI 生成的内容实际上重组了已有论文中的想法，但没有给出引用，这算不算学术不规范？
如果越来越多关键工具、模型和训练数据都掌握在封闭的商业系统里，数学共同体如何保持自身的独立性？
如果学生大量使用 AI，教师如何区分真正理解、机械模仿和不当使用？
如果审稿人使用 AI 辅助审稿，作者是否应该知道？审稿责任又该如何界定？
所以我觉得，对 AI 的态度可以用一句老话概括：
水能载舟，亦能覆舟。
我们当然要积极使用 AI，而且应该尽快学会使用 AI；但与此同时，我们不能把学术责任交给 AI。
作为研究者，我们一定要对自己的数学产出负责。作为老师，我们既要培养学生使用 AI 的能力，也要防止学生滥用 AI。作为论文作者，如果 AI 对证明、写作、实验、代码或材料整理产生了实质影响，我们也应该在合适位置说明 AI 的使用情况。
归根到底，AI 可以帮助我们提高效率、拓展思路、发现问题，但数学的最终责任仍然属于数学家自己。
结尾：不要神化 AI，也不要错过 AI 再次引用斯坦福大学最新研究中的一个观点。在 H5 级别的人机协作模式下，对于数学工作者——其实也包括航空工程师等高创造性职业——AI 的核心作用不是替代人，而是作为工具去放大人的判断力、创造力和执行力，最终提升人的表现。
最后，我想用三句话总结今天的分享。
第一，AI 可以帮助我们生成、搜索、整理和检查，但不能替代数学证明的最终责任。AI 甚至可能生成一些我们自己都无法判断真假的“漂亮垃圾”。
我自己就遇到过这样的情况。AI 曾经给出一个看起来非常漂亮的代数方法，声称解决了我正在研究的问题。整个论证写得头头是道，但当我认真去看时，却发现自己已经无法判断它到底是对是错。这个时候就必须格外谨慎。
因为如果连研究者本人都无法验证其正确性，那么最终产出的就有可能不是数学成果，而只是包装得非常精美的错误。如果未来我们的学生大量依赖 AI，而缺乏独立验证能力，就很容易产生这样的“漂亮垃圾”。
第二，AI 时代真正稀缺的，不是会不会向模型提问，而是能不能判断模型在哪里有用、哪里危险、哪里错了。换句话说，真正稀缺的是既懂数学、又了解 AI 数学边界的人。
第三，暂时不用过于担心数学家失业。
前几天我参加一个大型 AI 活动时，华中科技大学人工智能与自动化学院院长曾志刚教授在报告中感慨：
“AI 的基础都是数学啊！”
这句话让我印象非常深刻。
从机器学习到深度学习，从优化理论到概率统计，从几何、代数到组合结构，AI 的许多核心思想都深深扎根于数学之中。
因此，与其说 AI 会取代数学，不如说 AI 正在让数学的重要性被更多人重新认识。
过去，很多数学成果可能需要几十年以后才会体现应用价值；而今天，AI 的快速发展正在不断把数学推向科技创新的前沿。
所以我并不认为 AI 会让数学家失业。恰恰相反，我觉得 AI 很可能会让数学迎来新的春天。
因为它让许多过去成本很高的尝试变得廉价，让更多跨领域联系成为可能，也让数学家能够把更多时间投入到真正重要的问题之中。
所以，我想用下面这句话结束今天的分享：
过去爱迪生说：天才来自 1% 的灵感 + 99% 的汗水。 现在也许可以说：1% 的灵感 + 99% 的 AI 辅助。 但最后那 1% 的方向判断，以及 100% 的学术责任，仍然属于数学家。
也希望 AI 能真正赋能我们学院老师们的教学、科研、论文和项目工作，帮助大家提高文章和项目的数量与质量，也帮助我们培养新一代既懂数学、又懂 AI 边界的学生。
最后特别感谢陈冠涛老师的指导。这个报告是在陈老师周一报告的基础上准备的。如果今天的分享对大家有一点帮助，那主要是陈老师报告启发得好；如果我讲错了什么，那就是我自己准备得还不够充分。
题目：AI 赋能图论与组合数学：从辅助运算到自主求解研讨会 报告人：陈冠涛 时间：6 月 8 日（周一）10:30-11:30 地点：国交 2 号楼 M315
谢谢大家，欢迎各位老师批评交流。
参考资料与延伸阅读 [1] Benchmarks in Leipzig, arXiv:2606.05818, 2026.
[2] OpenAI. An OpenAI model has disproved a central conjecture in discrete geometry, 2026.
[3] Alon, N., Bloom, T. F., Gowers, W. T., Litt, D., Sawin, W., Shankar, A., Tsimerman, J., Wang, V., Wood, M. M. Remarks on the disproof of the unit distance conjecture. arXiv:2605.20695, 2026.
[4] Stanford SALT Lab. Future of Work with AI Agents, 2025.
[5] Leiden Declaration on Artificial Intelligence and Mathematics, 2026.
[6] 吴文俊. 数学机械化与几何定理机器证明相关工作.
[7] Lean / mathlib Community.
[8] Max Planck Institute for Mathematics in the Sciences. Benchmarks in Leipzig. https://www.mis.mpg.de/news/benchmarks-in-leipzig
[9] 马骁. 专访马骁：当 AI 推翻 80 年经典数学猜想，数学家的护城河还能存在多久？ 知识分子，2026. https://www.sina.cn/news/detail/5307590258987580.html
[10] 澎湃新闻 / 返朴. 独家对话：AI 正改变数学研究，一名中国本科生站在前沿. 2026. https://m.thepaper.cn/newsDetail_forward_33313803
转载本文请联系原作者获取授权，同时请注明本文来自龙旸靖科学网博客。 链接地址： https://blog.sciencenet.cn/blog-3353914-1538819.html
上一篇： 我终于读懂了“温柔”——四十岁中年人仿写全国I卷作文 欢迎参加科学网十佳博文评选活动！ 主办单位： 
支持单位： 