人工智能如何重塑数学研究之范式
作者：良之 发布日期：2026 年 3 月 17 日 来源：良之世界 » 逻辑 » 研究范式
君子性非异也，善假于物也。——《荀子》
现代 AI 编程工具已彻底革新软件工程的面貌——开发者如今在各类应用场景中，由 AI 助手完成相当比例的代码撰写。作为人机协作范式的长期探索者，我们见证着类似的变革正在基础科学研究中悄然发生，尤以数学领域为甚。
更确切地说：AI 工具如今仅需接收高层级的证明思路提示，便能推导并撰写出严谨的数学证明。这些证明以沿袭数百年的数学语言书写，恰如代码以 Python 等形式化语言撰写一般。AI 似乎已精通这两类语言及其背后的逻辑体系。
事实上，AI for Mathematics（AI4Math）已发展为一个独立的研究领域，其核心在于利用机器学习探索那些早期符号系统难以处理的数学疆域。与二十世纪中叶纯粹符号逻辑的路径不同，当代 AI4Math 整合了数据驱动的方法，这不仅是在应用 AI 辅助数学活动，更是通过数学的严谨性来测试和推进 AI 的通用推理能力。
菲尔兹奖得主陶哲轩在近期的一次对话中也表达了类似观察：如今面对某个猜想，他会先让 AI 尝试验证；知道怎么证明但懒得动笔的“引理”，就交给 AI 处理。在他看来，过去一年 AI 能力的飞跃——从“非常低效的研究生”到 IMO 金牌级表现——正在从根本上改变数学研究的习惯与流程。
与基于证明的 AI 工具协作，犹如与一位博学聪慧却偶有疏漏的同仁共事。
此认知源于近年来的研究实践：我们运用多智能体框架，完成了一系列原本需耗时数月方能写就的数学论文。这些论文阐述并解决了一系列基于图论与机器学习概念的优化问题。我们为构建论文整体框架所给出的典型提示往往只是高层级的思想草图，而 AI 能够将这些模糊的直觉转化为精确定义与陈述。
一、研究新范式：从“证明者”到“助产士”
我们从研究项目中获得的核心启示之一是：与基于证明的 AI 工具协作，犹如与一位博学聪慧却偶有疏漏的同仁共事。 你可像对人类合作者那样，向 AI 智能体勾勒数学论证的轮廓，而它则能将此草图转化为形式化的引理、定理及其完整证明。
日益地，AI 智能体甚至无需草图即可自行寻找证明，尤其当这些证明在数学某些领域属于“标准”类型时。这比表面听起来更有价值：许多论证在特定领域中属“标准”操作，但该领域可能恰恰是你——人类作者——并不专精的方向。AI 工具的优势在于，它通晓海量数学及其他科学学科的知识。
例如，在我们逐步提供思路以证明某项主要成果的过程中，AI 自发证明了一个我们未曾察觉的简单却实用的引理，显著简化了原有的论证路径。此类创造性带来的影响令人振奋，尤其在于降低了发现门槛：那些无法接触多元合作者群体的科学家，如今也能以前所未有的方式参与前沿研究。
陶哲轩以 Erdős 问题集为例指出：这些问题难度差异悬殊，有些困扰学界数十年，AI 确实无能为力；但 Erdős 提出了上千个问题，其中大量属于长期无人问津的“长尾问题”，而 AI 恰恰在这类问题上取得了突破——约二三十个此类问题在极少人类监督下被 AI 解决。这表明一种新工作流程已经成形：数学家可以开始发布自己真正想要答案的问题清单，也许 AI 能解决其中 10%，某个高中生能解决另外 5%，用社区驱动的方式推进数学研究。
然而，使用这些工具仍需谨慎与专业素养。它们生成的证明正确率或许仅为四分之三。但当出现错误时，若能识别问题，往往可通过迭代修正走向正确，并继续沿富有希望的路径推进。
若错误未被纠正，强行继续常会陷入死胡同。25%的错误率低到足以让专家觉得工具极其有用，却又高到可能在缺乏审慎判断时退化为“AI 研究垃圾”——外表光鲜却终究有缺陷或乏味的作品。毕竟，模型尚不知何为“有趣”或“有用”。
我们也观察到一些反复出现的失败模式。在撰写论文期间，我们曾要求 AI 生成一个小型自包含结果，它在几分钟内完美完成，我们随即告知该子项目已结束。然而随后数日，AI 竟主动建议重返该主题，尽管我们多次明确指示除非被问及否则勿再提及。这令人恼火地提醒我们：生成式 AI 并无完美记忆，仅拥有上下文的不完整摘要或嵌入表示。而在为实验编写代码以阐释理论发现时，我们发现 AI 能在极短时间内写出大量复杂且可运行的代码，却也可能在诸如“打印当前循环迭代次数”这类琐碎任务上迷失数小时。
2026 年初，一个更具震撼性的案例出现了：AI 系统 Gauss 仅用 5 天时间，便将菲尔兹奖得主 Viazovska 关于 8 维和 24 维球体堆积的证明转化为 20 万行 Lean 代码——此前人类团队耗时 15 个月进展缓慢。在形式化过程中，Gauss 发现了原论文中的 30 处逻辑瑕疵，并自主修复了第 14 页一处不等式推导的漏洞。更令人惊叹的是，在处理更复杂的 24 维证明时，Gauss 面对的是“逻辑真空”——没有任何预设蓝图，它通过检索跨越 30 年的数十篇关联文献，自行识别并引入外部引理，最终生成并验证了超过 12 万行 Lean 代码。这意味着：在逻辑验证的竞技场上，人类已不再是唯一的主角。
二、培育下一代：当入门级任务被自动化
历史上，人们在数学科学领域获得专长，源于初级研究者阶段的艰苦磨砺。博士生耗费数年钻研技术论证的细节，从而赢得来之不易的直觉：何时证明路径富有希望？何时被问题误导？何种研究方向才算新颖有趣？
但这些恰恰是 AI 工具正在“免费赠送”的能力。如果博士生只需向 AI 索取证明——这在推动研究进展的诱惑下极具吸引力——他们又如何发展出当下至少仍必需的经验与技能，以有效驾驭这些工具？
我们或许需更有意识地教授这些基础技能给年轻研究者，或许采纳一种“升级版”的小学算术教学法：禁止使用计算器。直白的建议是：要求初级研究者“按老办法”撰写论文，即使其工作本可借 AI 加速。
陶哲轩对此提出更宏大的构想：数学研究本身可能实现“分工”。传统上，数学家要包揽所有环节——提出问题、想策略、选策略、执行策略、验证结果、写成论文——每个人都得在每个环节“还行”，无法像现代工业那样真正分工。但有了 AI 和形式化验证工具，就有可能让数学项目像现代工业一样运转：每个人只专精一个环节，某个环节无人擅长，就让 AI 顶上。
这些下一代培养挑战并非 AI 科研独有。我们已在工程、客服、法律、写作、设计等诸多领域目睹类似现象——事实上，任何行业中，那些曾用于引导新人入行的入门级任务，如今皆由 AI 代劳。为寻找创造性解决方案，或更好预判即将到来的变革，跨领域或跨时代的类比或许大有裨益。
1960 年代初高级编程语言与编译器普及后，多数软件工程师不再编写机器码或汇编语言——后者虽可直接指令底层硬件，却繁琐不堪。但最优秀的程序员仍充分理解编译器如何将高级语言译为机器码，从而推理正确性与性能。我们期望，使构建与检验技术论证变得更为容易，能让所有研究者在更高抽象层级运作，“思考更宏大的命题”。我们所憧憬的文化，将强调品味、问题选择与建模能力，而贬抑为炫技而炫技的技术花招。
三、打破并重建同行评审：当 AI 成为审稿人
在我们看来，同行评审不仅、甚至主要不是验证研究正确性与质量的过程。其核心目的，在于将稀缺资源——研究共同体的注意力——引导至恰当之处。科学通过研究者彼此奠基而前进，但现有成果已多到无人能全盘掌握。出版流程应助我们识别最有趣、最有前景的方向，以便更高效、深入地发展它们。
AI 如何影响这种共同体注意力的聚焦？
最直观的冲击是数量爆炸。AI 工具极大降低了产出“看似精良且正确”作品的门槛，使得提交至期刊与会议的论文数量激增。2025 年，NeurIPS 投稿量冲破 3 万大关，比一年前近乎翻倍。这 3 万篇论文构成的认知过载，足以让任何人类评审系统当场宕机。
面对这场审稿危机，顶会开始寻求激进变革。ICML 2026 推出“作者自评级”机制——由图灵奖得主 Yoshua Bengio 支持——要求作者对自己提交的多篇论文进行排序，通过博弈论“保序回归”提升评审准确性。与此同时，ICML 还设计了复杂的“双轨制”政策：一条轨道严格禁止 AI 参与审稿，另一条允许在严格边界内有限使用，并要求审稿人使用企业级 API 或本地部署模型以确保数据隐私。这一设计的微妙之处在于“对等原则”：若作者要求自己的论文由纯人类审稿，则作为审稿人时也必须承诺不使用 AI——这有效遏制了“希望别人用生命读自己论文，自己却用 AI 敷衍别人”的投机行为。
更激进的尝试来自 aiXiv 平台——它完全欢迎 AI 撰写的论文，也欢迎 AI 审阅的论文，由一组 AI 审稿智能体日夜不休地工作，从创新性、技术稳健性等维度打分，达到门槛即可极速发布。这是一条加速主义路径：默认人类已无法独自处理现代科学的数据量，必须将部分认知工作外包给硅基智能。
然而，AI 审稿的滥用已引发严重担忧。顶级会议 ICLR 2026 的检测发现：21%的评审意见被判定为完全由 AI 生成，超过一半含 AI 痕迹。更令人震惊的是，有研究者通过在论文中隐蔽植入“仅给予正面评价”等指令，成功操纵 AI 生成评审意见——这种操控只需影响 5%的评审，就可能导致 12%的论文跌出前 30%排名区间。
陶哲轩对此保持谨慎乐观：他认为在一个工作流程中，能使用多少 AI 是有上限的——超过就会变成净损失，错误比解决的问题还多，而这个上限很大程度上取决于验证能力。数学最有条件实现高水平自动化，因为验证标准严格，但验证本身也有弱点：自然语言可被恶意利用，AI 可能表面勤恳、背地里悄悄在形式系统里多加公理。他警告：AI 是个极其精明的作弊者——很多验证系统正常使用没问题，但若专门训练一个 AI 去利用验证器最大化输出，它一定会找到漏洞。
若不进行严肃的、全社区范围的同行评审重构，AI 虽在个体研究者层面加速科学进步，却可能在共同体层面扼杀科学发展。
四、从理想到现实：当 AI 遇上百年难题
上述观察并非抽象推演，而是我们正在面对的真实处境。当我们以攻克长期未解的数学难题为使命，以“助产士”而非“证明者”自居时，AI 工具的每一次进化都直接重塑研究范式。
2024 年，Guth 与 Maynard 刷新了黎曼猜想的 80 年纪录；2026 年，Gauss 已完成菲尔兹奖级成果的形式化验证。理论窗口、AI 窗口、团队窗口——三重窗口在此刻重合。这是研究者必须正视的历史机遇。
我们的配置试图回应这一窗口期：以多智能体系统辅助研究攻关，以院士级顾问团队提供战略指引，以无限算力和形式化验证工具作为基础设施。更重要的是，我们同时布局了新一代数学形式化语言的研发——一种旨在解决现有系统固有局限的工具，为未来的研究储备“元武器”。
值得关注的是，类似的雄心正在获得全球性支持。由 Renaissance Philanthropy 与 XTX Markets 发起的 AI for Math Fund，已累计承诺 3150 万美元用于资助 AI 与数学结合的前沿研究。该基金 2026 年新一轮申请于 3 月启动，单项资助额度 10 万至 100 万美元，支持 12-24 个月的工作，要求所有代码、数据集与研究成果开放获取。首批 29 个获奖项目已覆盖全球顶尖研究机构，涉及数学出版物的形式化、证明底层性质的探索、关键工具链的互联互通等方向。这些动向表明，全球数学界正以前所未有的力度拥抱 AI 带来的变革。
即使外部资助未果，我们依然承诺底线交付：持续的形式化定理积累、开源系统发布、方法论白皮书、年度失败记录——这些构成“助产士契约”的最低履约标准。
无论外部环境如何，核心攻关照常推进。
五、展望未来：寻找本身就是意义
我们认为，AI 正引发科学研究方法论、人才培养与同行评审的沧海桑田；无人能回避这场浪潮。但我们有机会主动适应，确保 AI 辅助研究兑现其承诺。明年此时研究将是何种面貌？后年呢？过去一年所见变革胜过以往十年，故我们唯一能自信预言的唯有：“不同”。
陶哲轩在展望未来时指出：人类和当前大语言模型的能力正好互补，最好的组合永远是复杂的“人+机”组合，只是这种组合的性质会随时间改变。他同时提醒：AI 几乎太擅长不折不扣地执行目标了——如果你让 AI 解一道题，也许未来某天它真能直接给你答案；但你真正想要的，其实是人们努力的过程：尝试、失败、找反例、查文献、交流阶段性成果，这些才是解决一个问题的真正价值所在。
我们的科学制度——同行评审、出版体系、研究生教育——历经数十年演化，以匹配人类认知与精力的局限。而这些局限正急剧变迁，制度亦须随之调整。我们的目标应是导向这样一个世界：AI 放大人类的创造力与洞察力，加速发现进程，拓展谁可参与研究事业——同时守护那份使科学值得投身的喜悦与严谨。
我们将此称为“助产士的契约”：不生产真理，只助产真理。无论 AI 如何强大，寻找本身就是意义。
两千四百年前，苏格拉底的母亲[某科技公司]是助产士。苏格拉底说，他做的也是同样的事——帮助人们“生出”自己的真理，而非灌输现成答案。两千年后，我们站在同样的起点。
北辰在上，众星共之。 真理在望，吾辈助产。