AI赋能数学研究：工具演进、边界认知与实践策略

今日在学院午间研讨会进行了关于AI4Math的主题分享，以下为演讲完整内容。

各位同仁，中午好！

非常感谢学院提供的交流机会。坦白讲，接到这个分享任务时，内心确实有些顾虑。因为我知道，院内不少老师在人工智能的应用与探索方面已走在前列。今天我更多是以抛砖引玉、相互学习的态度，与大家分享个人的观察与心得。

计划用约三十分钟做简要汇报，之后预留更多时间，期待与各位同仁深入探讨。

今日分享的主题是：

AI赋能数学研究：工具演进、边界认知与实践策略

首先需要说明的是，这并非严格意义上的学术报告，更倾向于经验交流。过去一两年间，我也在持续学习、尝试和探索如何将人工智能融入教学、科研及项目工作中。因此，今日所分享的内容并非定论，而是我在运用AI开展数学研究、论文撰写、项目申报、材料修改以及指导学生过程中积累的一些观察、思考与实践经验。

首先想与大家分享一个学界与业界已形成共识的观点：

人工智能可能正在成为第四次工业革命的核心驱动力

近期有一句话令我印象深刻。李开复博士指出：

人工智能是我们几十辈子都难得一遇的机遇。

无论我们是否做好准备，人工智能正在深刻改变科研、教育、产业乃至整个社会的运作模式。对于数学工作者而言，一个值得深思的问题是：

人工智能究竟会如何影响数学研究？

今日的分享也将围绕这一核心问题展开。

先说结论：

人工智能并非数学的终点，而是数学研究工作流程的一次深刻变革。

为何如此说？

当前很多讨论容易走向两个极端。其一是神化人工智能，认为数学家即将失业，未来按一下按钮就能自动生成定理。另一极端是全然不信任人工智能，觉得它只会胡言乱语，对严肃数学毫无价值。

我的观点居于两者之间。人工智能固然会犯错，且错误往往非常隐蔽；但它也已经强大到不容忽视。它不只是帮我们撰写邮件、排版LaTeX，而是开始深入猜想、构造、证明、验证、写作等数学研究流程中的关键环节。

因此，今日我想探讨的核心问题并非“人工智能是否会取代数学家”，而是：

数学家应当如何运用人工智能？如何理解其能力边界？如何将其转化为提升教学、科研、论文与项目质量的工具？

今日分享的核心概念是AI4Math。此处的AI不仅指大语言模型，也包括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等工具。这些工具早已逐步融入数学研究。

只是过去许多工具更多是在帮助我们“计算”。

当前的新变化是，人工智能开始协助我们“思考”。

飞速发展的人工智能开始进入“猜想、构造、证明、验证”等更接近数学核心的位置。

近期数学界发生了一场不小的“震动”，而震源恰恰在组合数学领域。从某种意义上说，我们就处于震中附近。

这张时间轴展示了近几个月人工智能在数学研究中的几个标志性事件。

2026年2月：Gauss系统完成了球堆积问题的形式化验证。这是首个被完整形式化验证的菲尔兹奖级成果。

2026年4月：北大AI4Math团队（董彬、刘若川、肖梁等教授）利用“双智能体”框架攻克了Anderson猜想。一个智能体负责自然语言推理和文献检索，另一个负责Lean形式化验证，两者协同工作，最终解决了交换代数领域的重要猜想。

2026年5月8日：菲尔兹奖得主Gowers分享了使用GPT-5.5 Pro的经历，展示了人工智能在短时间内完成研究级数学探索的能力。

2026年5月20日：OpenAI模型给出了Erdős平面单位距离相关长期猜想的反例构造，引发了数学界的广泛关注。

最后这件事尤其令人震撼。

这个问题其实很容易阐述：在平面上放置n个点，最多能有多少对点之间的距离恰好等于1？

数十年来，数学家们积累了大量的构造与理论，对这一问题形成了相对稳定的直觉。许多学者相信，类似方格或晶格结构的构造已经非常接近最优解。

然而，OpenAI的模型却提出了一种全新的构造思路，并由此产生了反例。随后，数学家们对相关证明进行了整理、补充和验证。

这件事对组合数学和图论领域的冲击很大。因为这场“震动”的震中，就在我们的学术邻近领域：离散几何、组合、极值构造，这些方向与我们日常研究的问题非常接近。

无论我们是否愿意承认，人工智能已经开始改变数学研究的生态。

2026年6月（Leipzig Benchmark莱比锡基准）

还有一条最新消息，即Leipzig Benchmark。

数学家们组织了一场面向研究级数学问题的基准测试，共设置了100道题目。第一阶段，5个前沿模型各尝试一次后，仍有41道题完全未能解决；第二阶段，对表现较好的模型进行多次尝试，未解题数量降至16道；最后使用deep-thinking模型尝试，最终仅剩2道题未被解决。

当然，这一结果不能简单理解为人工智能已能完成98%的数学研究。因为题目类型、答案形式、提示方式、重复尝试次数等因素，都会影响最终结果。

但它至少说明了一点：研究级数学问题，已不再天然位于人工智能能力范围之外。

上面这张是会议照片。顺便一提，这次会议就在我攻读博士时期的马普应用数学所举行。看到照片中熟悉的办公室，以及许多老同事、老朋友，我感到非常亲切，也有些自豪。

目前较为公认的观点是：若讨论数学、物理等需要深度推理的问题，GPT 5.5基本处于第一梯队；若是大量编程和工程开发任务，Claude Code往往更具优势。当然，模型迭代非常迅速，这一结论可能几个月后就会发生变化。这个时代最大的特点之一，就是不要低估人工智能进步的速度。

下面是这100道题的领域分布，其中代数几何和代数组合所占比例最高。

接下来讨论Lean和形式化证明。

若要追溯机器证明在中国数学界的传统，可从吴文俊先生谈起。吴文俊先生很早就推动了机器证明，尤其在几何定理机器证明方面做出了奠基性贡献。今日我们讨论Lean，实际上也是“数学证明能否被机器严格验证”这一路线在新时代的延续。

如果说大语言模型更像一位可以用自然语言交流的数学合作者，那么Lean更像一位非常严格、甚至有些“不近人情”的证明检验器。

Lean的优势非常直观：若一个证明被写入Lean并通过检验，那么它的每一步都必须符合形式逻辑规则。它不依赖审稿人的直觉，不依赖作者的自信，也不依赖“这一步应该是显然的”这类数学写作习惯，而是由机器逐步验证。

这件事未来很可能影响数学论文的审稿方式。尤其是关键定理、长篇证明，以及那些容易出错的技术性引理，若能形式化，结果的可信度将大幅提升。

当然，Lean也并非万能。不同数学领域在Lean中的成熟程度差异很大。基础代数、逻辑、初等数论，以及部分分析方向，目前相对成熟；但组合数学、图论、动力系统、偏微分方程，以及许多几何问题，形式化基础仍然不够均衡。

我们从事图论研究的人对此有深刻体会。许多图论问题定义高度定制，构造非常图形化，小阶反例很重要，证明中还经常包含大量局部变换。要将这些内容全部写入Lean，成本非常高。

因此短期内，我并不认为每篇图论论文都需要Lean化。但我相信，未来重要结果的关键部分、标准理论，以及可复用的工具库，很可能会逐步形式化。

更现实的工作流程可能是：大语言模型帮助我们生成证明草稿，人类数学家负责整理结构、判断方向、补全细节，然后对最关键、最容易出错的部分进行形式化验证。

在这一方向上，国际上陶哲轩等数学家已进行了许多探索。国内也有不少团队在推进相关工作，如西湖大学陈华一教授，北大的肖梁、董彬、刘若川等教授，人大王善文教授，以及中科院的一些团队。

我们学院去年也邀请过王善文教授来做报告，题目是“人工智能与数学”，时间是2025年6月20日，地点就在现在的M315。当时王教授和北大、人大AI4Math团队的几位学生也到场了。他们当时的一个重要目的，是希望组织我们学院的学生参与Lean形式化方面的工作。

不过很有意思的是，仅一年时间，形势又发生了很大变化。去年许多Lean形式化工作还需要学生一行一行手写；但今年，随着人工智能工具的发展，许多基础性的Lean代码生成和修改工作，已经可以由人工智能辅助完成了。

2025年6月20日 M315

报告题目：人工智能与数学

报告人：王善文（中国人民大学）

这里我想分享一个我认为非常重要的观点：

数学家的价值不只是证明定理。

当然，证明定理是数学家的核心工作。但数学家还要做很多更上游的事情。

例如提出好定义。一个好定义可能比一个局部定理更重要。

例如选择好问题。一个问题值不值得做，有没有结构，有没有可能发展成理论，这需要判断。

例如找例子。数学里面许多理论都是从好例子开始的。

例如把局部技巧组织成理论，把一个结果讲成共同体能理解的故事。

历史上许多伟大数学家的贡献，不只是某个证明，而是他们改变了大家看问题的方式。

所以人工智能越能做局部推理，数学家的品位就越重要。

我想用一句话概括：

人工智能让尝试变便宜了，于是判断变得更贵了。

以前我们做一次尝试很昂贵，要查文献、写代码、推引理、改稿子。现在许多尝试可以让人工智能很快给出。问题是，尝试多了以后，如何判断哪条路值得走？哪个例子有结构？哪个引理是成立的？哪个结果可以发展成理论？

这仍然是数学家的核心价值。

数学研究大概可以拆分为八个环节。

第一，问题选择。第二，文献调研。第三，探索和实验。第四，猜想与构思。第五，证明拆解。第六，人工智能辅助证明与计算实验。第七，验证与检查。第八，论文写作、组织与修改。

在这八个环节里，人工智能所能发挥的作用并不相同。

问题选择主要还是依靠人类。人工智能可以帮助我们列出许多问题，但它并不知道什么问题真正值得投入几年时间，也不知道什么问题在一个领域中具有长期价值。

文献调研方面，人工智能非常有用，但一定会有遗漏。尤其是数学文献，一个关键引理可能藏在二十年前某篇论文的中间。人工智能给出的文献线索可以作为起点，但最终还是要查阅原文。

探索和实验方面，人工智能的作用越来越明显。它可以帮助我们编写程序、运行小阶例子、寻找反例、生成数据，也能帮助我们快速比较不同思路的可行性。许多时候，人工智能不一定直接给出答案，但能够帮助我们更快排除错误方向。

猜想与构思方面，人工智能很有启发性。它擅长做类比，也擅长提出“这个问题也许可以借助某某工具”的建议。当然，十个建议里可能九个都不靠谱，但只要有一个有价值，就已经很值得。

证明拆解方面，人工智能可以帮助我们把一个大目标拆解成若干引理或中间步骤。但它经常会提出一些看似合理、实际上难以证明甚至错误的中间命题，因此仍然需要人来判断。

辅助证明和计算实验方面，人工智能对短证明、局部论证、小阶搜索和计算实验都很有帮助。但对于真正复杂的长链条证明，目前仍然不够稳定。

验证与检查方面，人工智能很有价值，但不能过分依赖。它能够发现一些错误，也可能遗漏一些非常严重的错误。

我本人曾经测试过，我知道某篇已发布的论文中有个重要漏洞，但是让人工智能检查没有找出来。然后我告诉它，这里有个漏洞，它发现并且补齐了。

所以最终的正确性责任仍然在数学家自己身上。

论文写作方面，对我个人而言人工智能非常有帮助。它可以帮助整理结构、润色语言、修改摘要、绘图。但同时也存在风险：语言容易变得过于“人工智能化”，看起来很流畅、很漂亮，却缺少个人风格，或者不符合本领域的惯例，所以后期还需要很多人工的工作。

若借用斯坦福大学提出的Human Agency Scale，即H1到H5的人类主导权量表

H1是人工智能独立完成，例如简单排版、格式转换。

H2是人工智能主导、人类少量介入，例如初稿整理。

H3是人机平等协作，例如文献梳理、证明路线讨论。

H4是人类主导、人工智能持续辅助，例如复杂证明拆解。

H5是必须由人类全程主导，例如选题、原创理论、学术判断以及最终证明责任。

数学家整体核心工作归属于H5；

日常事务、计算、排版等基础工作落在H1/H2；

常规研究协作属于H3/H4；

原创理论、攻克难题这类核心价值环节，牢牢锁定在H5（人类不可替代）。

接下来分享一个近期澎湃新闻和返朴报道的案例：西安交通大学本科生汤泉宇同学的故事。

这个故事很有意思，也很有启发，但同时也很容易被误读。

若简单地将其理解为一个本科生靠人工智能做出了前沿数学成果，我认为是不准确的。更准确地说，这不是一个没有基础的人靠人工智能做数学的故事，而是一个有天赋、有准备的人，借助人工智能进一步放大能力的故事。

汤泉宇并不是普通意义上的初学者。根据报道，在大规模使用人工智能之前，他就已经独立或与他人合作解决过多个Erdős Problems网站上的问题，也已经在数学研究中积累了相当多的经验。这说明他本身就具有很强的数学基础、问题敏感性和研究能力。

后来，在人工智能辅助下，他又推进和解决了一些新的问题。其中一个很有代表性的例子，是Erdős Problem#650。报道中提到，他和合作者借助人工智能推进了这个问题，并且最终通过Lean完成了形式化校验。更有意思的是，在这个过程中，陶哲轩也关注到了相关问题，并参与了讨论。汤泉宇相当于是抢在陶哲轩之前，给出了一个陶哲轩也在关注的问题的关键证明。

这件事当然很惊人。但我想强调的是，人工智能在这里起到的作用，并不是凭空替代人的数学能力。人工智能帮助他更快地搜索思路、尝试证明、发现可能的路线；但真正关键的环节仍然在人：他要判断人工智能输出中哪些是有价值的，哪些是错误的；要继续追问、修正、重组问题；最后还要把想法推进成真正可以被数学共同体验证的结果。

所以这个案例给我们的启发，并不是说：有了人工智能，人人都可以轻松做前沿数学。

恰恰相反，它说明：

人工智能放大的是有准备的人的能力。

没有扎实数学基础的人，仍然很难提出真正好的数学问题，也更难判断人工智能给出的结果是否有价值。相反，那些已经有良好数学训练、又能熟练使用人工智能的年轻人，可能会被人工智能极大放大。

这对我们学院的人才培养也很有启发。未来我们培养学生，可能不仅要训练他们掌握数学基本功，还要训练他们学会使用人工智能，理解人工智能的能力和边界。也许在人工智能的赋能下，我们学院未来也有机会培养出这样一批学生：他们既有扎实的数学基础，又熟悉新的人工智能工具，能够更早进入前沿问题，更快参与真正的数学研究。

所以，汤泉宇这个案例最重要的意义，不是告诉我们“人工智能可以替代数学训练”，而是提醒我们：

未来稀缺的，是既懂数学、又懂人工智能数学边界的人。

我自己比较喜欢这样一个比喻：

大语言模型就像一位很聪明的合作者。他可能拥有数学或者科学多个方向的博士生级别知识，知识面很广，反应很快，也能提出很多有启发性的想法。

但正因为如此，我们更需要多接触它、多使用它，逐步了解它真正擅长什么、不擅长什么，哪里可靠、哪里容易出错。只有了解它的能力和边界，才能更好地与它合作。

在这个过程中，我们不能把自己放在“学生”的位置上，被人工智能牵着鼻子走。相反，我们仍然要做“导师”：要提出问题、判断方向、检查细节、决定哪些结果值得继续推进。

所以，我的基本态度是：

人工智能可以成为很强的数学合作者，但人类数学家仍然必须是导师和负责人。

下面我就介绍几个大语言模型介入数学科研的具体案例。

案例一（刘鸿及其合作者）：Turán问题

第一个场景，是我昨天在一个报告中听到的。

昨天刘鸿教授在“黄大年茶思屋”做了一个非常精彩的报告，题目是：

人工智能时代的数学：被超越，还是被增强？Mathematics in the Age of AI: Outpaced or Augmented 报告人：刘鸿，韩国基础科学研究院首席科学家 时间：2026年6月9日

这个报告中，刘教授分享了两个他自己的案例。其中第一个案例，正好是和我们学院丁教授的工作有关。

我想特别说明的是：这个结果并不是人工智能独立做出来的。恰恰相反，它首先是由数学家通过成熟的人工研究完成的。也就是说，核心定理、核心证明和主要数学思想，都是人做出来的。

人工智能发挥作用的地方在后面。

在人已经完成这个结果之后，人工智能因为另一个问题的启发，帮助把这个已有成果和一个新的应用场景联系了起来。也就是说，人工智能没有替代数学家完成原创证明，但它帮助放大了这个人工结果的影响力。

案例二（个人）：生物数学问题

第二个场景，是我自己最近做的一个生物数学问题。

这个问题原来的上界是O(r^5)。后来我们通过把问题转化为图论中的某种顶点染色问题，把上界推进到了O(r\log r)。这一部分结果目前已经放到arXiv上，但还没有正式投稿。

更有意思的是，最近在和人工智能反复讨论这个问题时，人工智能声称可以进一步做到线性上界，具体系数大约是126。

当然，这个线性结果目前还没有完全验证，不能说已经成立。猜想的最优结果可能是3r+1，也就是说线性是可能的，但常数应该还可以大幅压缩。

这里最有意思的地方，不只是人工智能给出了一个可能的更强上界，而是它帮助我们把原来的问题翻译成了另一个数学工具语言：从生物数学问题，到O(r\log r)的过程中翻译成的图的某种顶点染色方法，进一步在线性过程中转化为图的某种边列表染色方法。

这个过程再一次验证了：人工智能在跨越数学内部不同方向时很有潜力。它不一定能直接完成最后的严格证明，但它有时能帮助我们发现“这个问题也许应该换一种语言来表达”，而这种语言转换本身，往往就是数学研究中非常关键的一步。

案例三（个人）：组合数学和图论真的要被人工智能淘汰了吗？

近期有数学圈的朋友半开玩笑地问我：

组合数学和图论是不是要被人工智能淘汰了？

第三个场景也是我自己的经历，不过不是成功经历，而是失败经历。也许这个失败经历，正好可以部分回答这个问题。

先说一下Erdős。

Paul Erdős是20世纪最高产、影响力最大的匈牙利数学家之一，也是离散数学、组合几何和极值组合领域的奠基人之一。他一生提出了数千个问题和猜想，许多到今天仍然深刻影响着组合数学和图论的发展。

Erdős问题当然非常重要，也非常广泛。但需要强调的是，Erdős问题只是组合数学和图论中的一部分，并不代表整个领域。

顺便说一句，我自己有一点小小的自豪：我的Erdős数是2。因为我们陈教授是Erdős的合作者，他的Erdős数是1，所以我的Erdős数就是2。

但是图论和组合数学里，除了这些著名的Erdős问题，还有大量其他重要公开问题。我自己曾经用人工智能尝试过两个非常著名的猜想：

一个是László Lovász在书中提出的猜想。Lovász是2021年阿贝尔奖得主，也是现代图论和组合优化最重要的数学家之一。

另一个是List Edge Coloring Conjecture，也就是边列表染色猜想。

这两个问题我都尝试过让人工智能帮忙推进，而且不是随便问一问，而是反复拆解、反复尝试不同路线。但结果很现实：基本啃不动。

即使我们现在有非常强的大语言模型，有领域内最好的数学家不断尝试，这类问题依然很难被人工智能推进。原因可能在于，这些问题本身可用工具太少，结构太深，计算空间又大得惊人。人工智能很容易提出一些看起来像证明的路线，但真正检查细节时，往往会发现关键步骤根本站不住。

所以，从这个角度看，这其实是一件好事。

它说明，即使是在这次人工智能“震动”的震中——组合数学和图论领域，也仍然有大量问题不是人工智能现在能够轻易“淘汰”的。

人工智能的确已经能帮助我们做很多事情，也能在某些问题上产生惊人的突破；但它距离真正系统性地取代组合数学家和图论学家，还有很长的路要走。

更准确地说，人工智能不是要把组合数学和图论淘汰，而是会迫使我们重新思考：哪些部分是重复劳动，哪些部分是工具搜索，哪些部分才是真正不可替代的数学判断和结构洞察。

案例四：LLM以外的人工智能——数学智能体

除了直接使用大语言模型，我们也尝试过一些专门面向数学研究的智能体。不过从我们的实际体验来看，目前效果还比较有限。

第一个是Rethas。

Rethas是北大董彬教授AI4Math团队开发的数学专用自然语言推理智能体，是开源的。它可以和形式化验证智能体Archon配合使用，构成所谓的“双智能体协作框架”：一个智能体负责自然语言层面的数学推理和文献关联，另一个智能体负责Lean形式化验证。

我们在自己的图论问题上也尝试使用过Rethas。它确实通过关联到一个代数定理，帮助我们解决了问题中的一个很小的例子。但也仅限于此，对整个研究问题的实质推进并不明显。

我猜测，一个重要原因可能是：图论相关文献、尤其是许多细分方向和技术性引理，在智能体当前能够有效调用的知识库中还不够充分，因此它很难真正进入问题的核心结构。

第二个是HarmonicMath推出的人工智能数学家Aristotle，中文可以叫“亚里士多德”。

Aristotle是2025年底推出的数学专用智能体，因为独立破解Erdős问题#124这一30年悬案而受到关注。它目前没有开源，但任何人都可以在线试用：

https://aristotle.harmonic.fun/

我们尝试让它主动编写Lean形式化证明，这个尝试没有成功。

我理解主要原因在于：图论需要的形式化基础目前还不够丰富，而且许多图论问题本身也不容易形式化。图论证明中经常涉及具体构造、局部变换、染色过程、小阶反例以及大量“看图就明白”的直观操作。对人来说，这些步骤可能很自然；但要把它们严格翻译成Lean可以检验的形式，成本非常高。

相比之下，Aristotle这类智能体可能更适合那些已有形式化基础较好、知识库较完整、问题表达比较标准的方向。

所以，这两个尝试给我的体会是：数学智能体确实很有前景，但目前还远没有到“给它一个问题，它就能自动推进研究”的阶段。

引用《知识分子》采访中马骁老师的说法：

可以用“少跳”和“多跳”理解人工智能的数学能力。

少跳问题，就是从条件到结论中间跳数不多。比如一个局部引理、一个短证明、一个标准技巧、一个反例构造。人工智能很强。

多跳问题，就是需要维护很多对象、很多条件、很多不变量，证明链条很长。人工智能目前仍然不稳定。

所以它最适合做什么？

适合做局部推理，适合做跨界联想，适合做重复试错，适合做证明草稿，适合做代码实验。

不适合完全交给它做长篇结构证明，不适合让它独立决定选题，不适合把最终验证交给它。

现阶段最合理的模式是：

人类主导方向，人工智能扩大搜索；人类控制逻辑，人工智能生成候选；人类负责验证，人工智能辅助检查。

陶哲轩曾经多次谈到，未来数学可能会越来越像实验科学：更多合作者，更多工具分工，更多快速实验，更多可复现的验证流程。

传统数学有一种“个人英雄式”的模式：少数几个合作者，贡献很难区分，许多工作依靠个人长期思考。

人工智能时代可能会出现另一种模式：

有人负责提出问题；

有人负责理论框架；

有人负责计算实验；

有人负责形式化验证；

有人负责可视化和写作；

人工智能agent负责大量搜索、整理、草稿与检查。

这不一定让数学变浅。相反，它可能让数学走向更深的问题，因为许多“苦工”可以被工具承担。

但还是那句话，大方向要由人判断。我的个人经验是，人工智能容易走入局部，容易沿着错误方向越走越远，这时候我们要把它拉回来。

人类数学家的价值，会集中到更高层次的判断上。

人工智能进入数学，带来的不只有机遇，也有风险。

2026年6月发布的Leiden Declaration提醒数学共同体：人工智能正在挑战数学的一些核心价值，包括可靠性、署名、引用、开放性、同行评议，以及数学共同体对商业平台的依赖等。

这些问题并不抽象，而是会直接进入我们的日常研究。

比如，如果人工智能生成一个证明，而这个证明后来被发现是错的，谁来负责？

如果人工智能生成的内容实际上重组了已有论文中的想法，但没有给出引用，这算不算学术不规范？

如果越来越多关键工具、模型和训练数据都掌握在封闭的商业系统里，数学共同体如何保持自身的独立性？

如果学生大量使用人工智能，教师如何区分真正理解、机械模仿和不当使用？

如果审稿人使用人工智能辅助审稿，作者是否应该知道？审稿责任又该如何界定？

所以我觉得，对人工智能的态度可以用一句老话概括：

水能载舟，亦能覆舟。

我们当然要积极使用人工智能，而且应该尽快学会使用人工智能；但与此同时，我们不能把学术责任交给人工智能。

作为研究者，我们一定要对自己的数学产出负责。作为老师，我们既要培养学生使用人工智能的能力，也要防止学生滥用人工智能。作为论文作者，如果人工智能对证明、写作、实验、代码或材料整理产生了实质影响，我们也应该在合适位置说明人工智能的使用情况。

归根到底，人工智能可以帮助我们提高效率、拓展思路、发现问题，但数学的最终责任仍然属于数学家自己。

再次引用斯坦福大学最新研究中的一个观点。在H5级别的人机协作模式下，对于数学工作者——其实也包括航空工程师等高创造性职业——人工智能的核心作用不是替代人，而是作为工具去放大人的判断力、创造力和执行力，最终提升人的表现。

最后，我想用三句话总结今日的分享。

第一，人工智能可以帮助我们生成、搜索、整理和检查，但不能替代数学证明的最终责任。人工智能甚至可能生成一些我们自己都无法判断真假的“漂亮垃圾”。

我自己就遇到过这样的情况。人工智能曾经给出一个看起来非常漂亮的代数方法，声称解决了我正在研究的问题。整个论证写得头头是道，但当我认真去看时，却发现自己已经无法判断它到底是对是错。这个时候就必须格外谨慎。

因为如果连研究者本人都无法验证其正确性，那么最终产出的就有可能不是数学成果，而只是包装得非常精美的错误。如果未来我们的学生大量依赖人工智能，而缺乏独立验证能力，就很容易产生这样的“漂亮垃圾”。

第二，人工智能时代真正稀缺的，不是会不会向模型提问，而是能不能判断模型在哪里有用、哪里危险、哪里错了。换句话说，真正稀缺的是既懂数学、又了解人工智能数学边界的人。

第三，暂时不用过于担心数学家失业。

前几天我参加一个大型人工智能活动时，华中科技大学人工智能与自动化学院院长曾志刚教授在报告中感慨：

“人工智能的基础都是数学啊！”

这句话让我印象非常深刻。

从机器学习到深度学习，从优化理论到概率统计，从几何、代数到组合结构，人工智能的许多核心思想都深深扎根于数学之中。

因此，与其说人工智能会取代数学，不如说人工智能正在让数学的重要性被更多人重新认识。

过去，许多数学成果可能需要几十年以后才会体现应用价值；而今天，人工智能的快速发展正在不断把数学推向科技创新的前沿。

所以我并不认为人工智能会让数学家失业。恰恰相反，我觉得人工智能很可能会让数学迎来新的春天。

因为它让许多过去成本很高的尝试变得廉价，让更多跨领域联系成为可能，也让数学家能够把更多时间投入到真正重要的问题之中。

所以，我想用下面这句话结束今日的分享：

过去爱迪生说：天才来自1%的灵感加99%的汗水。

现在也许可以说：1%的灵感加99%的人工智能辅助。

但最后那1%的方向判断，以及100%的学术责任，仍然属于数学家。

也希望人工智能能真正赋能我们学院老师们的教学、科研、论文和项目工作，帮助大家提高文章和项目的数量与质量，也帮助我们培养新一代既懂数学、又懂人工智能边界的学生。

最后特别感谢陈冠涛教授的指导。这个报告是在陈教授周一报告的基础上准备的。如果今日的分享对大家有一点帮助，那主要是陈教授报告启发得好；如果我讲错了什么，那就是我自己准备得还不够充分。

题目：人工智能赋能图论与组合数学：从辅助运算到自主求解研讨会

报告人：陈冠涛

时间：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] 马骁. 专访马骁：当人工智能推翻80年经典数学猜想，数学家的护城河还能存在多久？ 知识分子，2026.https://www.sina.cn/news/detail/5307590258987580.html

[10] 澎湃新闻 / 返朴. 独家对话：人工智能正改变数学研究，一名中国本科生站在前沿. 2026.https://m.thepaper.cn/newsDetail_forward_33313803