AI4Math 综述：人工智能如何重塑数学研究
前言
最近看到一句话“世界顶尖的数学家你们该努力了，留给你们发财的数学难题已经不多了”，虽然是一句调侃的话，不过也道出了现在人类文明发展进化的方向。2026 年 5 月，AI 在数学领域接连交出重磅成果：OpenAI 的通用推理模型另辟蹊径，推翻了埃尔德什提出、困扰学界长达八十年的几何猜想；谷歌 DeepMind 的 AlphaProof Nexus，一举解开九道搁置半个世纪的数学难题。如今，越来越多顶尖数学家开始与人工智能携手合作，不断取得突破性进展。不难看出，人工智能与数学的深度结合，正将数学研究带入一个全新的发展阶段。本文将从技术发展脉络、主流工具、标志性成果以及未来趋势四个方面，对这一快速发展的领域展开全面梳理。
从符号主义到 AI4Math：一场跨越半个世纪的演进
用机器实现数学推理自动化，这个想法的出现，甚至早于现代数字计算机。早在二十世纪二十年代，大卫・希尔伯特便提出了一个宏大构想：将全部数学内容形式化，力求在一套自洽的公理体系中完成所有定理的证明。尽管 1931 年哥德尔不完备性定理，为这份乐观的愿景划定了理论边界，但人们对数学机械化的探索，始终没有停下脚步。
随着数字计算机问世，这些设想终于有了落地的可能。上世纪五十年代，马丁・戴维斯完成了普雷斯伯格算术的判定过程，这也是计算机实现逻辑命题机械验证的首个案例。此后，纽厄尔、西蒙与肖研发的 “逻辑理论家”，被视作真正意义上第一款用于定理证明的人工智能程序。在国内，吴文俊提出的几何定理机器证明方法同样影响深远：他将几何问题转化为代数方程组，证明了复杂的逻辑推演完全可以借助算法来实现。
不过，早期这类基于符号逻辑的方法，都遇到了同一个难以逾越的障碍 —— 搜索空间的组合爆炸。当证明过程变得复杂，可供选择的逻辑路径会呈指数级增多，依靠穷举搜索的方式，根本无法继续推进。
近十余年来，依托数据驱动技术发展起来的 AI4Math，彻底改变了这一局面，并逐步成长为独立的研究方向。研究人员开始借助机器学习，攻克以往符号系统难以处理的数学问题。正如 2026 年初一篇专题综述所提到的，发展 AI4Math，不只是打造服务于数学研究的智能工具；数学本身具备的严谨特质，也是打磨通用推理能力的绝佳试验场。简单来说，数学为人工智能的进阶提供了沃土，而人工智能又成为数学研究的强大助推器，二者相辅相成、双向赋能。
北京大学数学科学学院院长、中国科学院院士刘若川，曾将 AI 与数学的融合过程划分为四个阶段：计算辅助、逻辑验证、模式发现、协同推理。这个划分清晰展现出，机器从单纯的工具，一步步转变为数学家同行者的全过程。而 2026 年涌现的一系列成果，也让这一发展蓝图从设想变成了现实。
主要 AI4Math 工具全景
如今，服务于数学领域的智能工具已经形成丰富多元的生态。下面对其中几类代表性成果逐一介绍。
2.1 DeepMind 系列：AlphaProof、AlphaGeometry 与 AI Co-Mathematician
在 AI4Math 领域，谷歌 DeepMind 一直走在前沿。2024 年，团队研发的 AlphaProof 在国际数学奥林匹克竞赛中表现亮眼，拿到 21 分，达到赛事银牌选手水准，也成为第七个成功解答 IMO 压轴难题的 “参赛方”。这套系统擅长自动生成并完成形式化数学证明与验证，能够把数学问题转化为 Lean 证明环境下可核验的完整推理过程。
2026 年 5 月，DeepMind 推出全面升级的 AlphaProof Nexus，并在 arXiv 发表论文《Advancing Mathematics Research with AI-Driven Formal Proof Search》。这款新版本首次在前沿数学问题上实现大规模突破。它的核心思路，是把大语言模型的内容生成能力，与 Lean 形式化系统的验证能力深度结合：由 Gemini 3.1 Pro 负责构思、撰写并修改证明初稿，再交由 Lean 编译器逐段检查。一旦发现逻辑错误，系统便会反馈给智能体重新调整，循环往复直至证明成立。
AlphaProof Nexus 一共迭代出四个功能递进的智能体版本：基础版智能体 A、融合 AlphaProof 强化学习能力的智能体 B、加入进化式搜索的智能体 C，以及整合所有优势的完整版智能体 D。最终版本搭建了共享证明素材库，同时引入基于 Elo 分数的评价机制，让多个智能体在已有思路的基础上持续优化。这种 “大模型构思、形式化校验、强化学习拆解问题、多智能体协同迭代” 的思路，也为整个领域提供了清晰可行的技术路径。
除此之外，DeepMind 还推出了面向数学研究的多智能体协作系统 AI Co-Mathematician。在公认难度极高、一度被认为数十年内难以攻克的 FrontierMath Tier 4 测试集中，这套系统自主解题正确率达到 48%，在 50 道未公开难题中解出 23 道，刷新了业内纪录。作为参照，纯基座模型 Gemini 3.1 Pro 正确率仅 19%，GPT-5.5 Pro 为 39.6%。能力提升的关键，并不在于单纯扩大模型规模，而是优化整体架构：分层协作的多智能体设计、专职审核模块的交叉校验、可长期运行的异步工作机制，让这套系统能够像科研伙伴一样，伴随研究项目持续探索数日，不断推进研究进展。
2.2 OpenAI/Anthropic：通用大语言模型在数学领域的突破
和 DeepMind 深耕专用系统的路线不同，OpenAI 与 Anthropic 选择依托通用大语言模型开展研究。2026 年 5 月，OpenAI 一款尚未对外公开的通用推理模型，独立完成了一份原创数学证明，推翻了匈牙利数学家埃尔德什在 1946 年提出的平面单位距离猜想。这个困扰几何界近八十年的经典问题，终于迎来答案。
格外亮眼的是，AI 的解题思路完全跳出了人类以往的研究框架。几何学家们多年来始终在传统领域内探索，而这款模型另辟蹊径，运用代数数论中的经典方法完成论证，用全新的数域构造方式解开了难题。菲尔兹奖得主蒂莫西・高尔斯审阅后评价：“如果这是一位学者向《数学年鉴》投递的稿件，我会毫不犹豫建议录用。以往没有任何 AI 产出的证明，能达到这样的水准。” 多伦多大学数论学家 Arul Shankar 也坦言，如今的人工智能早已不只是辅助工具，它们可以提出新颖独到的想法，并且完整落地为最终的研究成果。
这样的突破并非个例。在此之前，业余研究者 Liam Price 仅向 GPT-5.4 Pro 提出问题，AI 便用简短篇幅，给出了一道搁置六十年的素数集难题的优美证明。斯坦福大学的 Jared Lichtman 称其为 “近乎完美的经典证明”。一系列案例足以说明，随着长程推理能力大幅提升，通用大语言模型已经具备参与前沿数学研究的实力。
2.3 北大 AI4Math 团队：双智能体协作架构
国内方面，北京大学 AI4Math 团队走出了独树一帜的路线，兼顾形式化证明与常规逻辑推理并行发展。团队由北京大学北京国际数学研究中心董彬教授牵头组建，成员涵盖代数数论、优化理论、机器学习、人工智能等多个方向，学科交叉优势突出。
团队打造的双智能体协作框架，由自然语言推理模块 Rethlas 和形式化验证模块 Archon 共同组成。在研究过程中，Rethlas 依托自研的 Matlas 语义检索系统，从海量数学资料里，找到看似无关、实则能发挥关键作用的整环完备化理论，以此构造出问题的反例。随后，Archon 将整套推理转化为约一万九千行 Lean 4 代码，转化过程中还能主动发现原有思路里的逻辑漏洞，重新规划证明路径。即便遇到 Lean 标准库尚未收录的数学概念，它也能找到等价理论完成替代。据团队测算，完成同等体量的形式化工作，这套系统的效率比资深 Lean 研究者高出十倍以上。
团队同时搭建了 LeanSearch 与 Matlas 两套检索引擎：前者支持用自然语言检索相关定理，目前已经在 Lean 全球社区广泛使用；后者可对海量数学命题做语义检索。刘若川院士也评价，这类检索工具，是人工智能开展严谨数学推理的重要基础。
2.4 其他代表性 AI 系统与项目
Gauss 智能体：由初创公司 Math, Inc. 开发，擅长数学推理与形式化验证。团队此前耗时两年半，仅完成两万行代码，用以验证 2022 年菲尔兹奖得主 Maryna Viazovska 关于八维、二十四维球体堆积的定理；而 Gauss 只用五天，就新增五万行代码完成整套验证，随后又在一周内补全二十四维相关内容，累计生成四十五万行代码，最终精简整合为二十万行，成为目前规模最大的单一主题 Lean 形式化项目。在工作中，Gauss 还主动发现并修正了原论文里两处细节错误。
ALPHA 项目：由加州大学洛杉矶分校（UCLA）牵头，获得美国国防高级研究计划局（DARPA）五百万美元资助，是一项为期三年的前沿研究。项目由韦王教授主持，菲尔兹奖得主陶哲轩也参与其中。团队目标是打造开源智能工具，聚焦偏微分方程、数论、复杂性理论三大方向，实现问题拆解、引理识别、证明思路自动生成，同时打通自然语言与形式化证明之间的转换通道。
CRT-ASA：由 Liangjing Zhang 等人研发，依托代数推理与中国剩余定理，生成严谨的数学证明。
AutoReal：基于大语言模型构建的定理证明工具，主要面向工业级系统验证，在 Isabelle 平台上展现出良好的适配能力。
三大技术路线：各显神通
综合目前业内主流实践，AI4Math 的技术路径大致可以归为三类，各自有着鲜明的特点。
3.1 形式化验证路线
这条路线的核心思路，是把数学证明转化为计算机能够识别的形式化语言（如 Lean、Isabelle），确保每一步逻辑推导都经过严格校验。形式化验证的理念由来已久，早期符号推理方法受困于组合爆炸问题，一直难以大范围应用，直到近十年结合机器学习技术后，才真正发挥价值。
当下最主流的工具是微软研究院 Leonardo de Moura 开发的 Lean 4，也被形象地称作 “数学编译器”：只要代码顺利通过编译，就代表整套证明逻辑完全成立。除此之外，Isabelle、Coq（Rocq）也是应用广泛的形式化系统。
AlphaProof Nexus 是这条路线的典型代表：借助大语言模型构思证明步骤，再交由 Lean 系统逐项验证；遇到错误便回溯修改，循环推进直至完成证明，整套流程由多个智能体分工配合，分别负责思路搭建、局部求解、效果评估与内容核验。
优势与局限：形式化验证最大的优点是绝对可靠，不会出现逻辑偏差。但它也存在明显短板：编写形式化代码工作量大，如何把自然语言描述的证明自动转化为形式化内容，至今仍是技术难点。同时，完全符号化的证明文本可读性不强，有学者担心，过度依赖这类成果，会让研究者难以读懂证明背后的思考，错失有价值的数学启发。
3.2 自然语言推理路线
这类方法直接依托通用大语言模型，用自然语言完成理解、推导与证明，无需额外转换为形式化语言。早期符号系统难以处理自然语义，业内也曾对纯文本推理心存顾虑，如今随着大模型能力提升，这一路线迎来快速发展。
主流工具以 OpenAI GPT 系列、Anthropic Claude Opus 系列为代表。
前文提到的 OpenAI 推翻埃尔德什猜想、GPT-5.4 Pro 证明经典素数问题，以及 ChatGPT 5.5 Pro 解开组合数学难题，都是自然语言推理的经典案例。这类模型擅长整合海量文献知识，打破学科边界，给出出人意料的解题思路。
优势与局限：自然语言推理灵活度高，容易产生创新性想法。但缺陷同样突出：大模型基于概率生成内容，容易出现 “看似合理、实则有误” 的逻辑假象，也就是常说的 “幻觉”。一处微小错误，还会在长链条推导中不断放大。因此，AI 产出的自然语言证明，必须由专业学者逐句核查，一定程度上降低了实际使用效率。
3.3 混合双智能体路线
混合路线结合了前两者的长处：一边依靠自然语言模块完成思路构思、文献检索，发挥创造力；一边借助形式化模块完成校验、落地，保障严谨性，两套体系协同工作。
北大 AI4Math 团队的 Rethlas 搭配 Archon，是这一思路的标杆方案。
此前 AI 攻克安德森猜想的过程，就充分体现了混合路线的价值：Rethlas 从海量资料中锁定关键理论、构造反例，Archon 再将整套内容转化为规范的 Lean 代码，过程中自主补全漏洞、调整方案。DeepMind 的 AlphaProof Nexus，本质上也属于混合路线，只是用多智能体模式进一步细化了分工。
优势与局限：融合创新能力与逻辑严谨性，是目前业内普遍看好的发展方向。但整套系统架构复杂，对跨领域技术整合能力要求很高，落地和推广的难度也更大。另外和纯形式化路线类似，高度标准化的证明内容，有时也会弱化证明过程中值得深挖的数学思想。
结合刘若川院士提出的四阶段划分来看：形式化验证路线，正从逻辑验证阶段持续向上发展；自然语言推理路线，在计算辅助与模式发现方面表现突出；而混合双智能体与 DeepMind 多智能体系统，已经迈入协同推理的高阶阶段。2026 年的多项成果也证明，这样的发展趋势正在不断加快。
里程碑式成果（2024—2026）
2024 至 2026 年，AI4Math 领域迎来成果集中爆发，下面按类别梳理其中具有里程碑意义的进展。
4.1 研究级数学问题的大规模突破
AlphaProof Nexus 攻克九道埃尔德什开放问题：2026 年 5 月，DeepMind 的 AlphaProof Nexus 一次性解决九道埃尔德什遗留的难题，其中历史最久的一题已搁置五十六年。与此同时，系统还证明了四十四项 OEIS 整数序列相关猜想，解开一道历时十五年的代数几何难题，并且优化了凸优化领域沿用已久的理论边界。整套工作单题推理成本区间在 200 至 400 美元，最低仅需 7.5 美元，所有 Lean 形式化证明内容均已在 GitHub 开源。这也是 AI 首次在前沿数学问题上实现系统性、规模化突破。
OpenAI 推翻埃尔德什八十年单位距离猜想：2026 年 5 月，OpenAI 通用推理模型证伪了离散几何领域的经典难题 —— 平面单位距离猜想。模型借助代数数论方法构造高维格点，证明存在无穷多 n 值，可以搭建出拥有至少n ^(1+C)组单位距离的点集。这是 AI 首次独立攻克数学界知名的经典未解问题，成果也获得菲尔兹奖得主的高度认可，达到顶级期刊发表水准。
AI Co-Mathematician 突破高难度基准、助力经典难题求解：DeepMind 的 AI Co-Mathematician 在高难度测试集 FrontierMath Tier 4 中正确率达到 48%。牛津大学 Marc Lackenby 教授也借助这套系统，解开了群论经典典籍《Kourovka Notebook》中尘封六十年的第 21.10 题。AI 先写出存在瑕疵但方向正确的证明初稿，审核模块精准找出问题，再由人类学者结合专业知识补齐关键环节，最终完成完整证明，也让人机协作的价值得到充分体现。
北大 AI4Math 团队攻克安德森猜想：2026 年 4 月，北大团队依托自研 AI 框架，解开交换代数领域十余年来悬而未决的安德森猜想，并完成约一万九千行 Lean 4 代码的形式化验证。这也是国内首次依靠人工智能，攻克前沿代数猜想并完成大规模形式化落地。
4.2 形式化验证的标志性突破
Gauss 完成菲尔兹奖级成果形式化：AI 智能体 Gauss 仅用五天，就完成了菲尔兹奖得主 Viazovska 关于八维、二十四维球体堆积定理的完整形式化验证，新增五万行 Lean 代码；随后又用一周时间完成二十四维相关内容，累计生成四十五万行代码，最终整理为二十万行标准内容。这也是本世纪首次由 AI 完成菲尔兹奖级别成果的全流程形式化验证，同时还修正了原论文中的两处细节问题。
AI 完成整本拓扑教材形式化：2026 年 1 月，研究人员借助 ChatGPT 5.2，通过命令行接口开展工作，仅用两周时间，就完成经典教材《Munkres 拓扑学》的形式化转换，生成十三万行规范代码，印证了通用大模型在大规模形式化工作中的实用性。
4.3 数学竞赛领域的持续领先
在数学竞赛方面，AlphaProof 早在 2024 年就拿到 IMO 赛事银牌，成功解答当年难度最高的第六题。专为几何题型优化的 AlphaGeometry，在奥数几何题目中同样表现优异。
4.4 AI 自主发现新定理与新方法
AlphaEvolve 刷新拉姆齐数纪录：DeepMind 的 AlphaEvolve 让大模型自主迭代搜索算法，一口气更新了五项经典拉姆齐数的下界，探索出以往人类未曾想到的研究思路。
AI 发现全新矩阵乘法算法：2026 年初，DeepMind 相关工具成功推导出新的矩阵乘法算法，同时为多项复杂几何问题划定新的理论边界。这也意味着，AI 不再只是解题工具，已经深度参与到数学理论的创新之中。
DeepSeek-Math-V2 开源模型：2025 年 11 月，DeepSeek 推出开源数学模型 DeepSeek-Math-V2，成为全球首款达到 IMO 金牌水准的开源模型。在 IMO-ProofBench 基准测试中，得分高出 Gemini DeepThink 十个百分点，有力推动了 AI 数学推理领域的开源生态建设。
技术挑战与展望
5.1 当前面临的核心挑战
推理幻觉问题：不搭配形式化校验的大模型，在长链条复杂推理中，容易出现隐蔽的逻辑断层，这类错误很难被非专业人员识别。而 AlphaProof Nexus 的核心思路，正是借助 Lean 编译器的强校验能力，从源头规避这一问题。
可读性与思想传递问题：形式化证明虽然保证了结果正确，但高度符号化的内容，很难传递证明背后的思考与数学洞见。不少学者担忧，过度依赖这类成果，会弱化数学研究重视理解与思辨的本质。
泛化与拓展能力不足：不少专用 AI4Math 系统，仅能处理和训练数据风格相近的问题，面对全新领域、全新题型时，表现会明显下滑。DeepMind 在研究中也提出，随着大模型能力不断增强，依靠多智能体循环协作，有望逐步替代针对性的专项训练。
知识库建设滞后：现有形式化数学库的覆盖范围仍然有限。北大团队在实践中发现，当研究用到库中未收录的概念时，AI 需要自行寻找等价理论替代，而在更多细分数学领域，这类问题会更加突出。
5.2 未来发展趋势
从辅助工具走向协同伙伴：刘若川院士提出的 “协同推理” 阶段正在加速到来。DeepMind 的 AI Co-Mathematician 已经具备雏形：依托分层多智能体架构与可长期运行的工作机制，AI 可以像研究搭档一样，连续数日跟进同一课题，记录每一次尝试、梳理不同研究分支，最终产出附带注释与文献引用的完整研究文稿。
人机协作成为主流工作模式：牛津大学学者借助 AI 解题的案例极具代表性：AI 负责产出初步思路，智能模块负责核查纠错，人类学者结合专业知识完成最终完善。这种分工模式，很可能成为未来数学研究的常规流程。
技术开源，降低使用门槛：AlphaProof Nexus 将整套证明代码对外开源，DeepSeek-Math-V2 也选择开放模型，这类趋势会让全球研究者共享技术成果，合力突破现有瓶颈。
AI 成为数学创新的助推器：正如多项研究展望所言，发展 AI4Math 的目标，并非用机器取代数学家，而是借助 AI 强大的探索能力，拓宽人类的研究边界。ALPHA 项目也提出，希望借助智能工具，从根本上改变数学家探索、验证新想法的方式。
结语
2026 年，被业内视作 AI4Math 的爆发之年。从 OpenAI 证伪八十年经典猜想，到 DeepMind 批量破解半世纪难题；从 Gauss 快速完成菲尔兹奖成果验证，到国内团队用双智能体系统攻克前沿猜想，一系列成果清晰证明：人工智能与数学的结合，已经完成从 “被动辅助” 到 “主动协作” 的跨越。
当 AI 能够独立构思证明、构造反例、推导新结论，并且经受最严苛的逻辑检验时，数学这门古老学科的研究方式，正在发生根本性改变。未来，每位数学家身边，或许都会有一位专属智能伙伴。它不会替代人类提出深刻问题的能力，却能极大释放探索未知的潜力。
回望过往，从希尔伯特的宏伟设想，到哥德尔的理论发现，从吴文俊开创机器证明方法，再到如今 AI 全面融入数学研究，让机器探索数学真理的理想几经起伏，却始终不曾中断。而现在，这份理想终于迎来了全新的发展阶段。