人工智能在数学领域的应用：进展、挑战与展望

https://arxiv.org/pdf/2601.13209v1

AI for Mathematics: Progress, Challenges, and Prospects

人工智能在数学领域的应用：进展、挑战与展望

摘 要

人工智能用于数学（AI for Mathematics，简称 AI4Math）已作为一个独立领域出现，它利用机器学习来探索那些对早期符号系统而言历来难以处理的数学领域。尽管20世纪中期的符号方法成功实现了形式逻辑的自动化，但由于搜索空间的组合爆炸，它们在可扩展性方面面临严重限制。近期数据驱动方法的引入重新激发了这一研究方向。

在本综述中，我们对 AI4Math 提供了系统性的概述，强调其主要目标是开发人工智能模型以支持数学研究。至关重要的是，我们指出这不仅限于将人工智能应用于数学活动；它同时也包括构建更强大的人工智能系统——其中数学所具有的严谨性可作为推进通用推理能力的顶级试验平台。

我们将现有研究划分为两个互补方向：一是面向特定问题的建模（problem-specific modeling），涉及为不同数学任务设计专用架构；二是通用建模（general-purpose modeling），聚焦于能够支持更广泛推理、检索与探索性工作流的基础模型（foundation models）。

最后，我们讨论了关键挑战与未来前景，倡导开发超越仅确保形式正确性的 AI 系统，转而致力于促成有意义成果与统一理论的发现，并认识到一个证明的真正价值在于它为整个数学领域所提供的洞见与工具。

关键词：机器学习，深度学习，形式验证，自动形式化，数学发现，自动推理，数学信息检索

1 引言

自人工智能（AI）诞生以来，数学推理的自动化一直是其核心目标之一。机械化推理的梦想甚至早于数字计算机的出现，可追溯至20世纪20年代，当时大卫·希尔伯特（David Hilbert）提出了一个纲领，旨在将全部数学形式化，以期在一致的公理系统内证明所有定理。尽管这一乐观愿景在1931年受到库尔特·哥德尔（Kurt Gödel）不完备性定理的理论挑战——该定理表明，任何足够丰富的形式系统必然是不完备的——但哥德尔的结果并未终结这一研究方向。正如乌拉姆（Ulam）[116]所指出的，冯·诺依曼（von Neumann）认为这些发现应促使人们重新思考形式主义的角色，而非彻底放弃它。后续研究进一步表明，经典数学的大部分内容可以进行有穷主义的约简[111]，从而维持了部分机械化梦想的活力。

随着数字计算机的出现，这些理论构想被付诸实践。20世纪50年代，马丁·戴维斯（Martin Davis）实现了普雷斯伯格算术（Presburger arithmetic）的一个判定过程[27, 35]，这可被视为计算机机械验证逻辑命题的首个实例。不久之后，纽厄尔（Newell）、西蒙（Simon）和肖（Shaw）开发了“逻辑理论家”（Logic Theorist）[97]，被广泛认为是第一个真正意义上的人工智能程序，它能在符号逻辑中进行定理证明。在符号主义时代，一个尤为具有影响力的里程碑是吴文俊（Wen-Tsun Wu）提出的几何定理机器证明方法[131, 133]。他通过将几何问题转化为代数方程组，并应用特征集方法，展示了复杂的逻辑推论可以被算法化地导出。

然而，大多数这类符号方法面临一个关键瓶颈：搜索空间的组合爆炸。随着证明复杂度的增加，可能的逻辑路径数量呈指数级增长，使得穷举搜索变得不可行。近几十年来，机器学习的引入重新激发了这一研究方向，提供了数据驱动的方法来导航这些复杂的数学空间。自2010年代起，联结主义人工智能（connectionist AI）迅速崛起，在计算机视觉和自然语言处理领域取得了显著成功。数学家们随后开始利用这些模型来识别可引导人类直觉的模式[34, 39, 57]，通过强化学习（RL）构造反例[54, 109, 119]，以及训练神经定理证明器[10, 132]。更近以来，大语言模型（LLMs）的飞速发展已能够生成新的数学构造[50, 98, 105]、实现自动形式化（autoformalization）[95, 135]，并支持协作式定理证明[156]。

这一融合催生了跨学科领域“人工智能用于数学”（AI for Mathematics，简称 AI4Math）。我们强调，AI4Math 不仅是将人工智能工具应用于数学任务，还包含构建更强大的人工智能系统——其中数学所具有的严谨性可作为推进通用推理能力的顶级试验平台。广义而言，该领域的研究可分为两个互补方向：

• 面向特定问题的建模（Problem-Specific Modeling）：涉及为特定研究问题或狭窄类别的数学问题设计专用架构，例如在纽结理论中引导直觉，或在封闭几何系统中进行推理。除了在目标任务上具有高度有效性外，这些模型通常所需的数据量和计算资源显著较少，使更广泛的科研人员能够使用。然而，若不进行大量修改，它们很少能迁移到其他领域。
• 通用建模（General-Purpose Modeling）：聚焦于开发基础模型（foundation models），包括专门面向数学的语言模型到通用推理引擎，旨在支持跨多个数学领域的广泛工作流。尽管具备通用性，但这类方法需要海量训练数据、大量计算资源以及深厚的工程专业知识。此外，当应用于定义明确的狭义数学问题时，它们可能无法达到专用模型那样的针对性和有效性。该方向涵盖自然语言推理的进展、通过自动形式化弥合非形式与形式数学之间的鸿沟，以及构建能够自动定理证明和信息检索的智能体系统。

值得注意的是，AI4Math 的技术范畴实际上超出了逻辑推理，还包括“人工智能用于计算数学与科学计算”。该子领域致力于构建人工智能模型以辅助数值计算，例如求解偏微分方程（PDEs）、优化问题和反问题。这一方向的根源可追溯至1980至1990年代，当时研究者探索使用浅层神经网络近似微分方程的解。然而，该领域在2015年前后随着深度学习的兴起而迎来复兴。尽管这些计算方面的进展构成了更广泛 AI4Math 图景中的重要支柱，但本综述将聚焦于数学推理——包括数学发现、形式化与证明。对 AI4Math 计算方面感兴趣的读者可参考其他综合性综述文献[6, 17, 21, 38, 70, 130]。

本文对 AI4Math 的进展、挑战与前景提供系统性概述。我们的目标并非穷尽所有工作，而是突出具有代表性的成果，以展现该领域的演进脉络。对特定子领域感兴趣的读者可参阅关于几何自动推理[25, 134]或用于定理证明的深度学习[85]等现有综述。第2节考察面向特定问题的建模，第3节回顾通用建模。最后，第4节讨论未来面临的关键挑战，倡导开发超越简单验证、迈向发现深刻数学洞见的系统。

2 面向特定问题的建模

随着数据驱动技术的快速发展，研究人员开始设计专门的机器学习模型，以应对特定的数学研究问题。这些工作大致可分为三个方向：
（1）在高维数据中识别模式，以引导人类直觉并激发新猜想；
（2）构造例子或反例，以严格检验或证伪数学假设；
（3）在封闭的公理系统（如欧几里得几何）内进行形式推理。
本节将回顾这三个领域的最新进展，并讨论各自的优势与局限。

2.1 通过机器学习引导人类直觉
利用机器学习辅助提出数学猜想的早期范例之一是文献[18]。该研究采用线性回归预测大量F理论几何结构中几何规范群的秩，成功重新发现了关于规范群秩的一个已有猜想。在此基础上，作者进一步将逻辑回归应用于涉及E₆规范群的分类问题；通过对模型进行归因分析（attribution analysis），他们提出了一个全新的猜想，随后由人类数学家完成了证明。

然而，真正展示深度学习在数学研究中广泛潜力的关键性工作是文献[34]。该研究的核心贡献是一个系统性框架，旨在加速猜想生成过程——传统上，这一过程耗时漫长，需数学家反复提出关系假设、尝试证明并迭代优化思路。在[34]提出的流程中，数学家首先假设两个数学对象之间可能存在某种关系；随后训练一个专门设计的神经网络，用其中一个对象的特征预测另一个量；接着使用归因方法识别最具影响力的输入成分，从而引导数学家形成更精确、更精细的猜想。该循环不断重复，直至得出具有数学意义的命题。利用这一方法，作者在纽结理论中发现了一个代数不变量与几何不变量之间的新关系[33]，并基于对称群的组合不变性猜想提出了一个候选算法[15]。

受此范式启发，文献[39]为仿射Deligne–Lusztig簇（ADLV）的研究设计了另一套AI引导直觉的框架。该工作不仅独立重新发现了算术几何中的经典“虚拟维数公式”，还建立了一个新颖且精确的下界定理。该结果通过提供一种填补重要理论空白的定量刻画，展示了AI引导直觉在纯数学深层领域促成严格发现的有效性。

除精炼猜想外，机器学习还被证明能揭示全新的数学现象。一个突出的例子是文献[58]：作者将椭圆曲线表示为向量，并训练逻辑回归分类器以区分不同秩的曲线。为解释分类器的优异性能，他们对向量表示进行了主成分分析（PCA）。在绘制固定秩和导子（conductor）的椭圆曲线的Frobenius迹平均值时，他们发现了一种令人惊讶的振荡模式，并将其命名为“低语”（murmurations）。这一现象此后成为深入理论研究的对象[16, 81, 158]。越来越多的文献正持续利用机器学习在各类数学领域中发现或重新发现关系[5, 12, 14, 18, 42, 55, 72, 77, 79, 80, 106]。

2.2 构造例子与反例
将机器学习用于构造例子和反例的开创性工作之一是文献[119]。该研究将图编码为0–1序列，并应用强化学习（RL）中的深度交叉熵方法，搜索可作为现有猜想反例的图结构。在此先例之后，RL被广泛用于多种结构性问题。例如，文献[11]将代数几何中奇点消解的核心框架——广中（Hironaka）博弈——建模为马尔可夫决策过程（MDP）。通过结合蒙特卡洛树搜索与深度Q网络，作者成功训练出一个智能体，能将奇点替换为光滑点，在du Val奇点上实现了近优的消解。类似地，文献[109]研究了Andrews–Curtis（AC）猜想。作者首先使用经典搜索算法验证了Miller–Schupp序列无限子族的AC平凡性，并在Akbulut–Kirby序列中实现了长度缩减；随后将一般问题形式化为MDP，并在不同难度的问题实例上训练RL智能体，最终发现了两个此前经典搜索方法未能找到的平衡展示（balanced presentations）的新型AC平凡化。

除强化学习外，多种其他机器学习技术也被用于数学构造。文献[4]在合成数据上训练Transformer模型，以预测稳定动力系统的Lyapunov函数；训练后的模型被用于发现非多项式系统的新Lyapunov函数。在组合数学中，文献[19]提出了一种迭代自举（bootstrapping）流程：该方法首先通过局部搜索算法生成候选构造，再在得分最高的候选集上训练神经网络，然后从网络中采样新种子以初始化下一轮局部搜索。利用此方法，作者成功找到了一个存在30年之久的猜想的反例。此外，文献[13]应用遗传算法生成2至5维的自反多面体（reflexive polytopes），在5维中识别出若干此前未知的多面体。其他利用机器学习构造例子或反例的工作还包括[23, 24, 54, 112]。

2.3 面向特定问题的形式推理

AlphaGeometry [115] 是一种神经符号方法，用于求解奥林匹克级别的欧几里得几何问题。它将一个符号化的几何推理引擎与一个用于建议辅助构造的语言模型相结合。其符号组件基于演绎数据库（Deductive Database, DD）[26]和代数规则（Algebraic Rules, AR），能够对给定前提集进行穷尽式推导，生成其演绎闭包。然而，纯粹的符号演绎无法引入新的几何对象——而这一能力在复杂证明中常常是必需的。为此，系统利用语言模型提出有用的辅助点。为克服人类证明数据稀缺的问题，作者通过交替执行符号演绎与随机点插入，生成了一个大规模的合成证明图数据集，并通过回溯（traceback）提取出最简证明。在推理阶段，系统以循环方式运行：符号引擎扩展演绎闭包，语言模型提出高概率的辅助点，循环重复直至达到目标结论。该架构使 AlphaGeometry 的性能显著优于基于启发式的系统，达到了国际数学奥林匹克（IMO）银牌水平。

其后续版本 AlphaGeometry2 [22] 通过在表达能力和效率两方面的增强，进一步推进了这一范式。形式化几何语言被扩展，以支持轨迹描述、线性几何关系以及非构造性陈述；底层符号引擎也经过重新设计，速度更快、鲁棒性更强。这些改进使得语言模型能够使用更大、更多样化的合成训练集进行训练。此外，AlphaGeometry2 引入了一种新颖的搜索算法——“共享知识搜索树集成”（Shared Knowledge Ensemble of Search Trees, SKEST），该算法并行执行多个搜索树，并允许它们交换所发现的信息，从而显著提升了对辅助构造空间的探索能力。因此，AlphaGeometry2 在 IMO 级别几何问题上达到了金牌水平。

除了基于神经网络的辅助点生成方法外，近期工作如 HAGeo [41] 提出了一种纯启发式策略，通过引入具有优良几何性质的辅助构造（如直线与圆的交点、中点、点反射等），同样实现了金牌级别的性能。其他关于欧几里得几何问题求解的工作可见于 [59, 147, 151, 152, 157]。

2.4 讨论

本节所讨论的三类方法——通过识别模式引导直觉、构造反例、以及在封闭系统中进行形式推理——各自具有独特优势，同时也面临不同的挑战。

AI引导直觉的范式之所以强大，在于它使数学家能够发现高维数据中难以或耗时手动检测的模式，从而有效缩小探索性研究中的搜索空间。然而，该方法并非普遍适用。它依赖于精心选择的问题，因为目标问题必须能够生成足够大且具有代表性的数据集。此外，成功实施需要较高的双重专业门槛：除了标准的机器学习考量（如架构设计、损失函数工程）外，深厚的数学洞察力对于解释模型输出并将经验性关联转化为严格数学理论至关重要。最终，由于证明和验证通常仍由人类数学家完成，该工作流的自动化程度仍然有限。

另一方面，利用机器学习构造例子与反例可显著加速猜想的提出与检验，尤其能发现违背人类直觉的对象。然而，这一方向也面临技术障碍，特别是分布外（out-of-distribution, OOD）泛化问题。例如，文献[4]中从采样解反向生成问题的方法可能产生具有特定分布的训练集，这在泛化到典型问题实例时会带来挑战，通常需要精心设计的机制（如作者提出的促进Lyapunov函数多样性的机制）来确保鲁棒性能。此外，当使用强化学习时，将数学问题映射为马尔可夫决策过程（MDP）并非易事。定义合适的状态表示、动作空间和奖励函数可能非常复杂[119]，而稀疏奖励和长规划视野等问题还会进一步加剧学习难度[109]。

最后，像 AlphaGeometry 这样的面向特定问题的形式推理系统表明，在结构化领域中，将符号引擎与神经语言模型结合可达到专家级性能。然而，这些系统的成功通常依赖于特定领域的符号引擎（例如用于几何的演绎数据库[26]）以及生成大规模合成数据的能力。因此，这类架构往往高度定制于其特定问题范围，若不进行大量修改，难以迁移到数学的其他领域。

3 通用建模

通用建模标志着从为孤立问题设计的专用算法，转向能够处理广泛数学领域的可适应系统。与面向特定问题的建模不同——后者针对每个新任务都需要定制特征和架构——通用建模方法利用在海量语料上训练的基础模型（foundation models），学习数学知识的通用表示。这些模型旨在支持多种活动，从求解多样化的习题集，到检索定理，再到协调复杂的发现工作流，而无需为每个新领域进行大量修改。

我们将通用建模领域的近期进展划分为四个互补方向：
（1）利用语言直观力量的自然语言推理模型；
（2）通过与证明助手交互以确保严谨性的形式推理模型；
（3）将推理锚定于既有知识的数学信息检索系统；
（4）整合上述能力以探索新成果的数学发现智能体。

本节首先分析基础模型（尤其是大语言模型，LLMs）的能力与内在局限，为后续对这四个关键方向的详细综述奠定背景。

3.1 基础模型与大语言模型（LLMs）
与传统机器学习模型（通常针对单一、狭义定义的任务进行训练）相比，大语言模型作为基础模型：采用单一架构，在广泛的数据和任务集合上以统一方式进行训练。从数学角度看，这一区别代表了一种范式转变——从函数逼近（function approximation）转向算子逼近（operator approximation），而这一过程与元学习（meta-learning）密切相关。

其成功的一个关键因素在于处理多样化数据类型的能力：分词（tokenization）将异构输入转换为统一的序列表示，而“下一个词元预测”（next-token prediction）目标则提供了一条适用于模型所遇所有任务的统一学习规则。在此框架中，基于注意力的架构至关重要。除了能有效随模型规模和数据量扩展外，注意力机制在训练过程中通过强制长上下文一致性，成为推理的核心引擎。这使得模型能够捕捉并维持长序列中的复杂依赖关系——这是逻辑演绎的先决条件。通过接触多样化的领域和监督信号，模型被迫将海量异构数据压缩为共享的内部表示，并在不同任务与语言之间发现共同的低维结构。一个自然的假设是，该低维结构中的关键组成部分对应于通用推理能力，这种能力可在不同语言和领域中表达。

数学天然契合这一框架。数学工作受严格逻辑规则支配，许多数学任务可被表述为在计算、推导或证明中生成下一个有意义的步骤——这正是“下一个词元预测”目标所设计建模的逐步结构。因此，当大语言模型作为基础模型在足够丰富的数学与科学语料上训练时，支撑跨领域泛化与长上下文一致性的相同机制，也可用于学习和运用广泛的数学推理能力。

然而，在掌握标准化考试与从事研究级数学之间仍存在根本性鸿沟。尽管当前模型在求解定义明确的本科水平问题上表现出色，但真正的数学研究要求开放式的探索、绝对的逻辑严谨性，以及驾驭高度专业化领域知识“长尾”的能力——在这些方面，随机性文本生成往往力有不逮。要将人工智能从一名胜任的解题者提升为可靠的科研伙伴，通用建模必须超越简单的“下一个词元预测”，通过整合形式验证、语义检索与智能体工作流，弥合“看似合理文本”与“严格真理”之间的鸿沟。

3.2 自然语言推理

当前的自然语言数学推理方法通常分为两类：数学专用的大语言模型（math-specific LLMs） 和 通用推理模型（general-purpose reasoning models）。

数学专用的大语言模型通常通过对通用基础模型进行专门的预训练和后训练流程（pre-training and post-training pipelines）加以适配。在预训练阶段，过滤流水线（filtering pipelines）[107, 141] 从网络语料（如 Common Crawl）、教科书和研究论文中提取高质量的数学内容，以最大化领域相关性。后训练阶段则通过监督微调（Supervised Fine-Tuning, SFT）和强化学习（RL）对模型进行进一步优化。

用于监督微调（SFT）的数据通常以“思维链”（Chain-of-Thought, CoT）[129]对的形式组织，包含问题及其分步解答；或采用“工具集成推理”（Tool-Integrated Reasoning, TIR）[53]示例，其中整合了外部代码执行。一个突出的例子是 NuminaMath [83]，它通过对高质量的 CoT 和 TIR 数据集进行微调，在首届 AIMO 进展奖（AIMO Progress Prize）中拔得头筹。尽管这类模型 [9, 107, 141, 144] 在基础数学和竞赛级基准测试（如 GSM8K [28]、MATH [60]、AIME）上表现出色，但其在高等数学方面的能力仍较少被探索。

与此同时，通用大语言模型（general-purpose LLMs）凭借规模扩展和新颖的推理策略，在数学领域也取得了显著进展。早期版本如 GPT-3 在基本算术任务上表现不佳，而 GPT-4 [1] 在 GSM8K 上达到了 92.0% 的准确率。随着“测试时扩展”（test-time scaling）的引入，该领域发生了范式转变——模型在推理阶段投入更多计算资源用于推理。OpenAI 的 o1 模型在 AIME 上展现出强大性能，后续的推理模型 [30, 56, 114, 140] 进一步验证了这一方法的有效性。截至 2025 年，增强型推理模型（如 Google 的 Gemini Deep Think）仅依靠纯自然语言推理，就在国际数学奥林匹克（IMO）中达到金牌水平，标志着该技术在中学奥数领域已趋于成熟。

然而，从奥数问题过渡到高等数学提出了更严峻的挑战。先前研究表明，尽管 GPT-4 能辅助处理本科阶段的内容，但仍需人类的关键监督 [29]，且在研究生层次上常常失败 [45]。近期的基准测试量化了这一差距：文献 [69] 报告称，DeepSeek-R1 在研究生代数（FATE-H）上的证明准确率为 71.0%，但在博士资格考试（FATE-X）上骤降至 33.0%。同样，在由未发表的研究级问题组成的 FrontierMath 基准测试 [51] 中，Gemini 3 Pro 在研究级子集上的得分仅为 18.75%，表明稳健的研究级推理能力仍是一个开放性问题。

为实证评估当前最先进模型的能力，我们构建了一个包含 100 道题目的数据集，题目选自北京大学（PKU）11 门本科数学课程的期末考试。我们评估了五个模型：GPT-4、o1、o3-mini、DeepSeek-R1 和 Gemini 2.5 Pro。附录 B 提供了样题及模型回答。人类专家根据 0–5 分制（评分标准见表 A）对输出进行打分，归一化后的结果如图 1（左图和中图）所示。尽管 GPT-4 得分低于 60，但经过推理增强的模型（OpenAI o 系列、DeepSeek-R1、Gemini 2.5 Pro）表现显著提升，其中多个模型得分超过 90。

此外，我们还在北京大学博士资格考试（涵盖分析、概率、代数、几何与拓扑）的 58 道题目上评估了 o3-mini。如图 1（右图）所示，o3-mini 的平均得分为 84.4。进一步分析各科表现可发现明显差异：该模型在代数方面表现最强，而在几何与拓扑方面得分最低。假设这些考试对人类学生构成相近难度，则这一结果表明，当前的人工智能系统在处理抽象代数结构方面相对更擅长，而在需要几何直觉的任务上相对较弱。尽管由于潜在的数据污染风险以及考试题目与开放性研究问题之间的本质差异，这些结果需谨慎解读，但它们提供了有力证据：顶尖模型如今已能处理相当一部分研究生层次的数学内容。

综合上述发现，我们观察到一条清晰的发展轨迹：大语言模型的数学推理能力已从掌握基础运算和中学竞赛，发展到胜任本科课程内容，并正开始进入研究生乃至研究级数学的领域。

3.3 形式推理
尽管顶尖的大语言模型（LLMs）如今已能解决某些研究生层次甚至部分研究级数学问题，但对其能力的评估仍是一个重大瓶颈，需要大量人工投入。随着数学复杂性的增加，评估高度依赖领域专家；然而，由于自然语言本身具有内在的模糊性，即便是经验丰富的数学家也可能误判论证。一个著名的历史案例发生在1994年：《数学年刊》（Annals of Mathematics）发表了一篇论文，声称Busemann–Petty问题在四维及以上维度具有负解 [148]。该结论后来被证明是错误的 [73, 74]，而1999年的一篇论文最终确立了该问题在四维情形下实际上具有正解 [149]。这一事件表明，即使在顶级期刊严格的同行评审流程中，错误仍可能长期存在。因此，为了实现对数学推理快速且可靠的验证，研究必须转向一种更机械化、更无歧义的框架。形式系统（formal systems）恰好提供了这样的基础。本节将讨论形式系统对数学研究的益处及其在增强大语言模型推理能力方面的价值，随后综述自动定理证明与自动形式化（autoformalization）领域的最新进展。

3.3.1 形式系统
形式系统提供了一种精确的符号语言，并配以严格定义的机制，用于构造和验证证明。目前存在多种形式系统，其区别在于底层逻辑基础：HOL 系统（如 HOL Light、Isabelle/HOL）采用简单类型论（simple type theory）；Coq 和 Lean 使用依赖类型论（dependent type theory）；Metamath 基于一阶逻辑并显式指定公理；而 Mizar 则建立在 Tarski–Grothendieck 集合论之上。一旦将数学论证翻译成交互式定理证明器（Interactive Theorem Prover, ITP）的形式语言，即可对其进行绝对严谨的验证。倘若1994年那篇关于 Busemann–Petty 问题的错误结果当初在形式系统中被形式化，其潜在的逻辑缺陷很可能立即被发现，从而避免错误结论的发表。

除了对数学正确性本身具有内在价值外，形式系统对人工智能发展还提供了一个关键优势：它们提供了可靠且可验证的监督信号。与初等数学不同（其答案常为数值，易于核对），面向证明的高等数学问题缺乏简单的验证器，难以生成可靠的训练信号。交互式定理证明器通过为每一步逻辑推理提供精确反馈，弥补了这一缺口。这种能力为强化学习（RL）提供了高质量的训练信号，从而使模型能够在严格环境中发展出更强的推理能力。

在众多交互式定理证明器中，Lean [36, 37] 已培育出一个尤为强大的生态系统。其统一的数学库 mathlib4 通过大规模社区协作迅速扩展，截至2025年12月，已包含超过25万条定理和12万个定义。该领域的一项里程碑式成就是由 Johan Commelin 主导的“液态张量实验”（Liquid Tensor Experiment），该项目形式化了 Peter Scholze 关于液态向量空间的一个核心定理。Scholze 最初对该证明的正确性存有疑虑，后来称该定理可能是他“迄今为止最重要的成果”²。该项目历时约18个月，不仅验证了该结果，还简化了 Clausen–Scholze 原始证明，帮助 Scholze 更深入地理解了论证的结构³。此外，“液态张量实验”还推动了 mathlib4 中代数基础设施的发展：它促成了同调代数与范畴论的早期形式化，并吸引了一大批代数学家加入社区。

其他值得注意的里程碑包括：Polynomial Freiman–Ruzsa（PFR）猜想的形式化、球面翻转定理（sphere eversion theorem）的形式化，以及由 Kevin Buzzard 领导的费马大定理（Fermat’s Last Theorem）形式化工作。在应用数学方向，近期研究还在 Lean4 中建立了数值优化的形式化基础，特别是验证了一阶算法的收敛性 [82]。

然而，这些项目仍然高度依赖人力，需要专家手动将定义和证明翻译为代码。这种高昂的成本推动了自动形式化工具与自动定理证明器的发展，以加速数学知识的数字化进程——即将标准的非形式化数学转化为 Lean 等严格形式系统中的内容。

3.3.2 自动形式化（Autoformalization）
自动形式化是指以自主方式（例如通过语言模型）将自然语言中的数学陈述和证明翻译为形式化代码的任务。该领域的早期工作采用序列到序列（sequence-to-sequence）模型，并在对齐数据上进行训练。例如，文献[126]通过将Mizar形式陈述“非形式化”（informalizing）来构建数据集，用于训练翻译模型。为应对对齐语料稀缺的问题，文献[125]随后探索了基于循环一致性损失（cycle-consistency losses）的无监督方法：模型在无需显式监督的情况下，通过在非形式与形式领域之间来回翻译并重建原始陈述来学习映射关系。

大语言模型（LLMs）的出现从根本上改变了这一范式。研究表明，现成的LLMs通过少样本提示（few-shot prompting）即可生成合理的形式化结果[3, 8, 46, 135]。尤为关键的是，文献[135]观察到一种不对称性：对模型而言，将形式代码翻译为自然语言（即“非形式化”）远比反向操作（即形式化）更容易。这一洞见催生了大规模合成数据集的构建——研究者利用LLMs对庞大的形式库（如mathlib4）进行非形式化，从而生成高质量的对齐语料，用于训练专用的自动形式化器[48, 66, 87, 90]。

近期工作聚焦于提升这些系统的质量与语义根基（grounding）。Herald [48] 提出了一种分层非形式化策略，该策略尊重mathlib库的依赖图结构：通过按拓扑序翻译声明，确保在翻译依赖定理时，其前提概念的自然语言描述已可用。Herald还通过基于策略（tactic-based）的状态合成进一步扩充数据，在miniF2F验证集上实现了超过96%的准确率。为增强语义根基，RAutoformalizer [87] 引入检索机制，将生成的代码锚定于已有的形式化声明之上。针对研究级数学中常见的“缺失概念”问题，文献[122]提出了Aria——一个基于LLM的智能体系统。

更一般地，基于LLM的智能体（agent）指一类通过与环境显式交互循环运行的系统：它维护中间状态，基于观测进行推理，执行多步规划，并据此选择行动。这些行动可包括调用外部工具，如语义检索、符号推理模块或代码合成组件，而环境反馈则用于指导后续决策。此类智能体设计能够将复杂任务分解为结构化的子任务，并支持超越单次生成的迭代优化[123]。在此框架下，Aria将非形式陈述分解为概念依赖图；若某概念在mathlib库中缺失，该智能体会通过语义搜索与合成，自底向上递归地定义该概念，从而有效处理数学术语中的“长尾”现象。

评估与验证
自动形式化的评估并非易事。尽管人类专家评审是黄金标准，但其不可扩展。因此，核心挑战在于开发自动化的正确性度量方法：

• 有参考真值（With Ground Truth）：当存在参考形式陈述时，正确性应通过逻辑等价性（而非简单的字符串匹配）来评估。例如，BEq [87] 利用神经定理证明器检验生成陈述与参考真值是否可相互推导。类似等价性检验方法也在[88, 101]中被探讨。
• 无参考真值（语义验证，Semantic Verification）：在缺乏参考形式陈述的情况下，需验证语义正确性——即形式代码是否忠实捕捉了非形式陈述的意图。一种朴素方法是“回译”（back-translation）：让LLM将代码再翻译回英文进行比对[48, 143]。然而，这种方法容易出错，因为LLM可能忽略细微的逻辑差异。为缓解此问题，文献[139]提出了Mathesis——一个细粒度评估框架。Mathesis将陈述分解为假设与结论，分别评估各组成部分的一致性，并通过模糊积分（fuzzy integral）聚合得分，以严格排除不一致情况。为进一步辅助验证，Aria [122] 通过检索每个形式术语的详细元数据（类型、取值、非形式描述）来丰富上下文，从而支持更准确的语义判断。

可靠的验证器不仅对评估至关重要，还可作为强化学习（RL）中的关键奖励模型，形成一个反馈闭环，持续提升自动形式化的性能[63, 90, 139]。

注：本节聚焦于陈述的自动形式化。而证明的自动形式化——即不仅翻译定义，还需转换逻辑推理步骤——与自动定理证明密不可分。因此，我们将在下一节关于证明生成的讨论中一并阐述证明的自动形式化。

3.3.3 自动定理证明
形式系统中的自动定理证明旨在为形式化陈述生成有效的证明。基于深度学习的方法大致可分为两类：单模型方法（single-model approaches） 和 智能体方法（agentic approaches）。单模型方法又可进一步细分为证明步骤生成（proof step generation） 与完整证明生成（whole-proof generation）。

证明步骤生成（Proof Step Generation）

证明步骤生成方法将定理证明建模为一个树搜索问题。在此框架中，搜索树的每个节点对应一个证明状态（proof state），每个动作对应应用一个策略（tactic），从而将证明器转移到新的证明状态。一旦找到一条通往“无剩余目标”状态的路径，即成功构造出证明。图2展示了此类方法生成的证明树示例及其最终形式化证明。

该方法的优势在于可重用性与探索能力。在搜索过程中，证明状态是可重用的：若新遇到的状态与先前已探索的状态一致，则可合并。此外，系统在每一步尝试多种策略，展现出强大的探索能力。然而，这些方法常因树搜索的计算开销而面临推理速度慢、训练不稳定，以及对高效交互式工具在训练和推理阶段的高度依赖等问题。

该领域最早的神经方法之一是 Holophrasm [132]，它采用蒙特卡洛树搜索（MCTS）进行探索，并集成三个神经组件：用于检索有用定理的相关性网络、用于提出变量替换的生成网络，以及用于估计可证性的价值网络。后续工作大多将策略预测视为分类问题，代表性工作包括 GamePad [62]、DeepHOL [10] 和基于图的方法 [99]。超越纯分类范式，GPT-f [103] 训练了一个 Transformer 模型，通过条件语言建模目标生成证明步骤，并使用最佳优先搜索（best-first search）构造证明。类似地，文献[76]引入了超树（hypertree）搜索结合在线训练策略，其中策略网络与评判网络定期根据重复证明搜索所收集的数据进行更新。

该领域的一大挑战是大规模形式化数据的稀缺。为应对这一问题，REALProver [110] 提出了一套集成流水线：包含一个陈述自动形式化器（用于翻译非形式陈述）、一个基于检索增强的证明器（其策略生成以相关前提为条件），以及一种专家迭代（expert iteration）范式。在该循环中，模型在生成的状态-策略对上训练，执行证明搜索，并从成功搜索中迭代收集新的训练数据。

一个显著的里程碑是 AlphaProof [64]。AlphaProof 训练了一个30亿参数的证明网络，可同时输出策略与价值估计。其训练流程包括：在3000亿词元上预训练，在30万组状态-策略对上进行监督微调，并在8000万条自动形式化陈述上进行强化学习。这些形式陈述源自约100万道非形式问题，其自动形式化模型在（非形式陈述，形式化思维链，形式陈述）三元组上训练，每道问题生成多个不同翻译。对于特别困难的任务，AlphaProof 还采用测试时强化学习（test-time RL），通过构建并训练专用课程（curriculum）来适应问题结构。结果，其性能达到IMO银牌水平。其他值得注意的方法包括 [67, 84, 102, 121, 138, 142]。

完整证明生成（Whole-Proof Generation）

相比之下，完整证明生成方法旨在通过单次前向传递生成整个形式化证明（可能辅以内联注释）。其主要优势在于高推理速度，以及在生成过程中无需依赖交互式工具。然而，其探索能力相较于逐步搜索较为有限；它们通常依赖行为克隆（behavior cloning），且由于无法访问中间证明状态，更容易出现错误累积。

该范式高度依赖数据的质量与数量。由于缺乏先验的、原则性的数据质量判定方法，评估通常通过模型性能间接进行。为解决数据量问题，文献[136]提出了一套集成流水线：包括自动陈述形式化、过滤（剔除平凡或错误陈述）、陈述证明，以及在所得验证对上进行迭代训练。在此基础上，DeepSeek-Prover-V1.5 [137] 通过构建更丰富的数据集（包含形式代码前撰写的非形式证明及内联非形式注释）并应用来自验证器反馈的强化学习（RLVF），进一步提升了性能。采用该范式的其他工作包括 [9, 40, 44, 144, 150]。

智能体方法（Agentic Approaches）

智能体方法代表了从单模型系统向模块化工作流的范式转变。这些方法将定理证明分解为若干协调的子任务（如检索、分解、验证），并通过结构化工作流将语言模型与外部工具集成。其有效性依赖于三个核心组件：鲁棒的检索系统、LLM 的推理能力，以及模拟数学研究过程的工作流设计。

Draft, Sketch, and Prove (DSP) [68] 是该范式的原型。它首先生成非形式证明，将其翻译为带有开放子目标的形式化草稿（sketch），再使用轻量级证明器闭合这些子目标。LEGOProver [120] 在此基础上扩展，维护一个持久的引理池（lemma pool）。其独特之处在于，通过维度扩展、关键概念识别、参数化和复杂度增强等策略，将已验证的引理演化为新引理。Hilbert [118] 则通过递归子目标分解（由定理检索引导）将非形式证明转化为形式草稿。Seed-Prover-1.5 [20] 同样采用专用草稿模型与专用证明器模型，在研究生级基准 FATE-H/X [69] 上取得优异成绩。

针对非形式推理与形式代码之间的粒度鸿沟，文献[128]提出了两阶段的“状态链”（Chain of States, CoS）框架。该方法在生成具体转换策略前，先提取与非形式论证逻辑流对齐的中间形式状态序列，从而在计算资源受限的情况下显著降低策略生成的复杂度。

更先进的智能体如 Aristotle [2] 将非形式推理与形式验证交织进行：它以引理序列为单位起草证明，对其进行形式化并尝试验证，并根据反馈迭代优化输出。Aristotle 结合几何求解器，在 IMO 金牌水平上取得成果。最后，Gauss 智能体 [95] 展示了人机协作的力量：在专家搭建的脚手架（scaffolding）支持下，仅用三周便完成了强素数定理（strong Prime Number Theorem）的形式化。

这些成果表明，精心设计的智能体工作流能够有效融合模型的内在推理能力与外部工具，从而在自动定理证明中实现显著突破。

3.4 数学信息检索（Mathematical Information Retrieval, MIR）

数学信息检索旨在从大规模数学文档集合中检索数学内容，包括公式、定理和问题解答。与标准文本检索不同，MIR 必须显式考虑数学表达式的独特结构与语义。数学公式本质上是结构化对象，其含义取决于符号的组合方式与关系结构，而非简单的词汇重叠。因此，一个有效的 MIR 系统必须应对诸如匹配数学结构与符号模式等挑战，同时利用周围的文本上下文来消解歧义并解释语义。

尤为重要的是，MIR 不仅是供人类用户使用的搜索工具，更是现代自动定理证明（ATP）和 AI 智能体系统的基础组件。在 ATP 中，“前提检索”（premise retrieval）——即从庞大的数学库中识别出对证明新定理有用的定理、引理或定义——往往是主要瓶颈。随着数学库规模扩大至包含数十万条形式化陈述（如 mathlib4），能否高效检索到“大海捞针”般的关键前提，直接决定了证明器能否成功解决问题，还是因超时而失败。对于智能体系统而言，MIR 使其能够访问长期的数学记忆，从而将推理建立在已确立的知识基础上，而非凭空生成未经支持的“幻觉”事实。这要求检索范式从传统的关键词匹配转向基于推理的检索。一个鲁棒的 MIR 模型必须理解逻辑蕴含与数学等价性；例如，它应能识别出“方阵行列式非零”这一陈述，是回答“该矩阵列向量是否线性无关”这一查询所必需的关键前提，即便两者之间没有任何共享关键词。

根据检索目标的粒度与查询的性质，MIR 涵盖若干紧密相关的任务，主要包括：语义检索（semantic retrieval）、问答检索（question-answer retrieval）和前提检索（premise retrieval）。

语义检索（Semantic Retrieval）

语义检索旨在根据数学含义（而非表面相似性）从数学语料库中识别出数学上等价或高度相关的陈述。该任务源于实际需求，例如在大型数学库中进行定理搜索。例如，Lean 用户在构造证明时常需在 mathlib4 中定位相关定理。在此场景中，查询可以是自然语言或形式代码，而检索语料库通常由 mathlib4 的形式化声明组成。

为弥合非形式查询与形式语料之间的鸿沟，LeanSearch⁴ 构建了一个源自 mathlib4 的对齐非形式–形式语料库，并在联合表示空间中执行检索 [47]。该方法实现了跨表示模态的语义匹配，显著提升了自然语言查询的检索效果。除 LeanSearch 外，其他为 mathlib4 开发的语义搜索工具还包括 Moogle⁵、LeanExplore [7]、LeanFinder [89] 和 LeanDex⁶。

公式检索（formula retrieval）是语义检索的重要子任务，其查询为数学公式或公式模式，目标是从文档集合中检索语义相关的公式。该任务带来独特挑战：表示同一数学概念的公式可能因记号差异或代数性质（如交换律）而在表面形式上大相径庭；反之，视觉上相似的公式在不同数学语境下可能含义迥异。

传统公式检索方法主要基于树表示，以编码数学表达式的结构组织。公式被表示为树，相似性通过子树或路径匹配，或通过计算树编辑距离来定义。广泛使用的表示包括符号布局树（Symbol Layout Tree, SLT）[145]，其中节点对应符号，边编码上标、下标或邻接等空间关系；以及算子树（Operator Tree, OPT）[49]，其内部节点表示运算符，叶节点表示操作数。与 SLT 相比，OPT 抽象掉视觉布局，聚焦于数学运算及其层次关系。

基于树的检索算法通常通过匹配子树或路径，或计算树编辑距离来比较公式。例如，Approach0 [154, 155] 将公式表示为算子树，并以叶到根的路径作为基本检索单元：先筛选出路径与查询重叠的候选公式，再基于最大公共子树导出的相似性度量对候选结果重排序。

除传统符号匹配外，近期研究探索了使用文本嵌入模型进行公式检索。早期方法通过线性化结构化公式编码，将其嵌入连续向量空间。例如，TangentCFT [93] 对 SLT 和 OPT 进行深度优先遍历，将所得元组序列分词后应用文本嵌入模型获取公式表示。同期工作通过融合周围文本上下文来更好捕捉语义 [75, 92]。例如，MathAMR [92] 将公式整合进其语言上下文中：结合抽象语义表示（Abstract Meaning Representation, AMR）图与 OPT，用对应 OPT 的根节点替换 AMR 图中的公式节点，并使用 Sentence-BERT 嵌入线性化后的图结构。

问答检索（Question-Answer Retrieval）

问答（QA）检索旨在响应自然语言查询，检索数学答案、解释或支持性文档。数学问题本质上是多模态的，通常结合自然语言与符号表达式、公式或图表，候选答案也具有类似结构。因此，数学 QA 检索中的相关性由语义充分性定义——即答案是否正确且有意义地回应了问题，例如提供有效解法、证明或概念性解释，而非依赖表面词汇重叠。

早期数学 QA 检索主要依赖通用文本检索技术，如 TF–IDF 和 BM25。尽管可直接应用，但这些方法在数学领域表现不佳，因其依赖精确词匹配，无法建模数学语言的语义或公式中编码的结构关系。

随着深度学习兴起，研究转向基于预训练 Transformer 的神经检索模型。常见做法是在大规模数学语料上预训练并微调 Transformer 模型，以获得更契合数学语法与语义的表示。例如，MathBERT [100] 在富含公式的语料上预训练，并引入“掩码公式子结构预测”等目标，以更好地在上下文中建模数学符号。

基于稠密检索范式，文献[104] 在 ARQMath 基准 [94, 146] 上研究了 ColBERT [71] 的应用，通过基于规则启发式选取负样本，在数百万问答对上微调神经检索器。鉴于符号方法与神经方法的互补优势，若干混合方法也被提出。例如，Mabowdor [153] 将稠密段落检索与基于结构感知数学索引的稀疏检索并行结合，并通过学习加权方案融合输出。该混合策略在 ARQMath-3 [91] 中表现优异，凸显了将经典数学结构与神经语义表示相结合在 QA 检索中的有效性。

前提检索（Premise Retrieval）

在自动定理证明中，一个核心子问题是前提检索：给定一个猜想和一个包含大量已有数学陈述的库，系统需识别出哪些前提可能有助于构造证明。

早期方法主要依赖手工设计的相似性度量与启发式规则 [61, 96]。此类思想的变体与扩展（包括基于树的相似性评分）在近期工作中仍被探索 [127]。同时，轻量级机器学习方法（如 k 近邻或稀疏朴素贝叶斯）也曾用于前提选择 [32]。

过去十年，深度学习方法在前提检索中日益普及。代表性早期神经方法是 DeepMath [65]：它分别编码猜想与候选前提，将所得表示拼接后输入全连接网络，预测该前提是否有助于证明该猜想。训练采用监督方式，利用现有证明——出现在证明中的前提视为正样本，并通过困难负采样（hard negative mining）构建信息丰富的负样本。

后续工作试图更好地利用逻辑公式的内部结构。例如，FormulaNet [124] 将每个公式表示为源自其语法结构的图，节点对应常量、变量或量词，再通过图神经网络计算嵌入，组合后输入分类器估计相关性。

超越成对评分模型，后期研究探索了对整个陈述库的图级表示。文献[43] 构建了一个全局图，其中节点对应数学陈述，有向边编码从证明中提取的前提–结论关系。新猜想的前提选择被建模为链路预测问题，使用图卷积网络基于节点的文本与结构特征对潜在边进行评分。

与此同时，另一研究路线采用基于嵌入的检索方法：将每条数学陈述视为文本，通过学习的嵌入模型编码为单个向量，相关性通过嵌入空间中的相似性评估，通常再经学习的重排序阶段优化候选集。训练通常依赖对比目标：将猜想与其证明中出现的前提拉近，同时推远无关陈述。该方法的代表工作包括 [110, 113, 142]。

3.5 数学发现智能体（Agents for Mathematical Discovery）
随着大语言模型（LLMs）能力的持续增强，基于 LLM 的智能体也不断进步，近期多项工作已展现出它们在发现新数学构造方面的潜力。

FunSearch [105] 采用进化方法搜索能够生成目标构造的程序。对于具备明确定义评估器（evaluator）的问题，FunSearch 利用现成的 LLM 迭代地将低分候选程序演化为高分程序。具体而言，该方法维护一个规模大且多样化的程序池，并反复提示 LLM 对早期候选程序进行改进。通过这一方法，FunSearch 发现了新的大容量帽集（large cap sets）构造，其结果超越了极值组合学中此前已知的最佳成果。

在此基础上，AlphaEvolve [98] 采用了更强的 LLM，并将进化过程从单个函数扩展至整个代码文件，同时支持多指标联合优化。AlphaEvolve 已在多个问题上取得了改进的构造，包括“最小重叠问题”（Minimum Overlap Problem）和 11 维空间中的“接吻数问题”（Kissing Numbers problem）。

受 AlphaEvolve 启发的开源实现包括 OpenEvolve [108]、ShinkaEvolve [78] 和 DeepEvolve [86]。这类 AlphaEvolve 风格的智能体特别适用于那些可通过编写代码来处理、并能通过明确定义的评分函数进行评估的数学问题，尤其擅长寻找新的数学构造。

4 挑战与展望
尽管人工智能在数学领域（AI for Mathematics）取得了令人鼓舞的进展，该领域仍面临一个根本性障碍：当前的人工智能系统，尤其是基础模型，尚缺乏进行研究级数学所需的深度推理能力。弥合这一鸿沟需要从被动辅助转向在严格“逻辑环境”中的主动学习。这要求加速数学的形式化（或数字化）进程，以提供可自动验证的反馈，从而迭代式地增强 AI 的推理能力。此外，提升这些能力还需将专业数学知识——从高质量数据构建到专用智能体工作流的设计——深度融入模型开发过程。最终目标是将 AI 无缝整合进数学家的日常实践中，而这一愿景唯有通过 AI 研究者、工程师与数学界持续、紧密的合作才能实现。我们将在下文总结这些关键挑战与未来方向：

1. 领域专业知识与特征工程：在面向特定问题的建模中，输入特征的设计往往需要深厚的领域专业知识。人类直觉在选择具有数学意义的特征以及解释模型输出以提炼理论洞见方面仍不可或缺。这一依赖同样适用于面向发现的智能体（如 AlphaEvolve 类系统），它们依赖精心手工设计的表示和评分函数。因此，开发有效的 AI for Mathematics 必须依靠机器学习研究者与领域专家之间长期、紧密的合作，以确保计算成果能转化为真正的数学进步。
2. 验证瓶颈与自动形式化：准确高效的验证是研究级数学的关键瓶颈。自然语言固有的模糊性，加上能够审核高级证明的专家稀缺，使得人工验证既缓慢又易出错。为实现可靠性，数学推理最终必须扎根于形式语言之中，其正确性可由机器机械地检验。然而，由于高质量形式数据严重匮乏，当前 LLM 的形式推理能力远落后于其自然语言表现。解决这一“形式数据鸿沟”需要开发鲁棒的自动形式化工具，以弥合非形式与形式数学之间的差距。通过为特定子领域构建可靠基础设施，并支持库级（repository-level）形式化，我们可加速将自然语言推理转化为形式证明。这将形成一个良性循环：形式可验证的反馈可作为高质量训练信号，进一步提升 LLM 在数学乃至更广泛领域的推理能力。
3. 形式化中的语义一致性：自动形式化面临一个微妙挑战：验证所生成形式陈述的语义正确性。现有模型常难以判断回译后的形式陈述是否忠实捕捉了原始非形式猜想的细微含义。这需要开发细粒度、鲁棒的语义一致性验证器。尽管语义意图的最终判断理应保留给人类专家以确保概念准确性，但自动化系统可作为高效的第一道筛选机制。通过大幅减少需人工复核的候选数量，这类系统可在不牺牲严谨标准的前提下规模化形式化进程。
4. 超越正确性，迈向理解：形式有效性是数学价值的必要条件，但非充分条件。正如威廉·瑟斯顿（William Thurston）著名指出的 [31]：“数学不是关于数字、方程、计算或算法；而是关于理解。”一个有价值的证明不仅确立真理性，更提供洞见、揭示结构，并贡献可应用于其他问题的技术。类似地，斯坦尼斯瓦夫·乌拉姆（Stanislaw Ulam）[117] 引述斯特凡·巴拿赫（Stefan Banach）的话：“优秀的数学家看到定理或理论之间的类比，而最杰出者则看到类比之间的类比。”这揭示了一个更深层的真理：证明的价值在于其深化我们对数学图景概念性把握的能力。因此，未来的 AI 系统必须超越单纯验证，协助发现那些能重塑我们思维、揭示此前不可见联系的证明。
5. 从启发式到专家常规流程：尽管独立的 LLM 是强大的推理引擎，但 AI4Math 的未来在于设计能模拟专业数学家复杂工作流的智能体系统。研究级数学极少是线性演绎；它涉及一个复杂的迭代循环：构造例子、查阅文献、提出猜想，并根据中间失败不断调整证明策略。然而，当前的智能体仍大多通用化。一个关键前沿是开发能显式建模这些专家“常规流程”（routines）的架构，学会以反映研究者认知过程的方式协调工具与策略。这包括使用“计算草图”（computational sketching）——不仅用代码生成形式证明，还用于构造数值玩具示例或执行符号推导，以快速验证或证伪人类直觉。此外，这些智能体可自动化高价值但常被人类忽视的“长尾”任务，如证明重组、条件弱化、以及晦涩已有解法的语义检索。最终目标不仅是模仿人类工作流，更是优化它们，创造出能以超越人类的系统性与规模探索数学思想空间、攻克难题的智能体。
6. 积极的社区参与：呼应领域专业知识的必要性，AI 推理能力的提升需要数学家的主动介入。除了生成形式数据，社区必须积极探索这些系统，以集体构建对其能力与边界的心理模型。例如，明确模型在代数操作上是否优于几何拓扑，对确定 AI 可靠部署的场景至关重要。这不仅要求加速数学知识的数字化以创建可验证的训练语料库，还要求开展“对抗性协作”（adversarial collaboration）以识别逻辑漏洞。通过严格刻画这些优劣势，数学家可引导开发出不仅统计强大、而且数学上可靠（mathematically sound）的模型。
7. 拥抱 AI 辅助研究：我们必须为一场文化转变做好准备：AI 将从计算工具演变为研究副驾驶（copilot）。2025 年末陶哲轩（Terence Tao）与 Google DeepMind 合作的工作 [50] 正凸显了这一转型。陶哲轩观察到，尽管这些模型可能仍缺乏真正理解，常常只是“模仿思考”，但它们已能自主发现人类直觉难以企及的数学构造。即使模型产生幻觉或推理有缺陷，其生成看似合理结构候选的能力仍使其成为有效的副驾驶——引导研究者走向富有成果的探索路径，而将最终的严格验证留给专家。

我们认为，即便 AI 的发散式推理（提出随机或创造性变体）正确概率较低，只要“验证杠杆”（verification leverage）足够高，整体研究效率仍会提升。在许多高等数学领域，生成一个解在计算或认知上代价高昂，而验证一个候选解则相对迅速。这种不对称性使研究者可将 AI 作为高吞吐量的候选思想生成器——单次有效洞见所节省的时间，远超剔除错误建议的低成本。

然而，实现这一潜力不仅需要强大的模型，更需要精心设计、易于使用的工具。要促进高参与度，必须通过稳健的软件设计降低使用门槛。近期框架（如 AlphaEvolve）相比早期原型在易用性上的显著提升表明：工程质量是决定这些技术能否从实验性新奇物转变为全球广泛采用的标准工具的关键因素。

原文链接：https://arxiv.org/pdf/2601.13209v1