当前位置：首页 > news >正文

重塑数学边界：人工智能如何引领数学研究的新纪元

news 来源：原创 2025/5/4 9:26:47

一、人工智能如何重新定义数学研究的边界

（一）数学与AI的关系：从基础理论到创新思维的回馈

（二）AI的创造力：突破传统推理的局限

（三）AI对数学研究的潜在贡献：创新的催化剂

二、AI 与数学的碰撞：从传统到生成式AI的进化

（一）传统人工智能：符号推理与规则系统

（二）机器学习：从数据驱动到模式识别

（三）生成式AI：数学创新的新时代

（四）生成式AI在数学中的创造性潜力

三、人机共证：AI 参与数学证明的前沿探索

（一）初衷与基础工具：从手工推理到机器验证的演进之路

（二）自动化形式证明生成：AI 在严谨推理中的新进展

1. 关键特点：AI 证明系统三要素

1.1 早期探索者：RNN、搜索与强化学习的结合

1.2 向交互式智能迈进：与人类协同工作的证明助手

2. 大语言模型的介入：从 GPT-f 到 COPRA 的新范式

3. 更多范式的探索：递归式、Dojo 式、甚至 Olympiad 水平的 AI 数学家

（三）自动形式化：让 AI 学懂数学语言

1. 从规则系统到神经网络：早期的尝试与突破

2. 大模型介入：从模仿到理解

3. 数据集构建：AI 数学语言教育的基础工程

4. 形式化≠验证：自动评估的新挑战

（四）全流程证明生成：从自然语言到完整证明的自动化路径

1. AlphaProof 的曙光与迷雾

2. 人机协同：草稿、结构与证明

3. 自然语言证明生成：回归“人类语言”

四、从识别模式到理论探索：AI 与数学家的共创旅程

（一）数据驱动的数学研究范式转变

（二）从数据中生发理论：人机协同框架的实践

（三）从模式识别走向生成性思维

五、显式构造数学对象：从强化学习到语言模型的双路径探索

（一）强化学习方法：构造的决策旅程

（二）语言模型路径：从语义到构造的创造性跳跃

1. 🧠 从零训练的语言模型：构造函数与组合结构

2. 💡利用大模型进行“类比构造”：FunSearch 框架

（三）🌱 遗传编程的现代重构：LLM + 进化算法

六、结语：走在数学与AI交汇的十字路口

干货分享，感谢您的阅读！

当数学遇上人工智能，会碰撞出怎样的火花？这不再是遥远的幻想，而是正在发生的现实。从符号推理到生成式AI，从定理验证到新理论的提出，AI 正在重新定义数学研究的边界。本文将带你走进这场前所未有的人机共创之旅，探索智能时代下数学的全新可能。

一、人工智能如何重新定义数学研究的边界

在我们所处的数字时代，人工智能（AI）正以前所未有的速度改变着各行各业的格局，从医疗健康到金融科技，从自动驾驶到创意产业，AI正在无声无息地融入我们的生活。而在这些技术应用背后，有一个领域正在悄然发生着深刻的变革——那就是数学。我们可能习惯于将数学视为纯粹的逻辑与理性领域，认为它完全依赖于严谨的推理与抽象的思维。然而，随着人工智能的崛起，数学研究的模式正在悄然转变。

（一）数学与AI的关系：从基础理论到创新思维的回馈

长期以来，数学为人工智能提供了强大的理论基础，从概率论到统计学，再到线性代数与优化理论，AI的许多核心算法都深深扎根于数学的土壤中。然而，近年来的AI发展，尤其是强化学习（RL）和大语言模型（LLMs）的突破，开始显示出AI能够反过来为数学研究提供支持的巨大潜力。这种潜力不仅仅表现在算法上的改进，更重要的是，AI在创造力与灵感上的优势，正逐渐成为数学创新的新源泉。

（二）AI的创造力：突破传统推理的局限

数学问题往往是复杂的挑战，常常没有现成的解决模板，需要依赖深邃的推理和灵活的战略思维。正如费马大定理的证明经历了数百年的困扰，直到安德鲁·怀尔斯教授凭借全新的代数数论框架成功解决。这一过程强调了数学创新背后的关键——突破传统的思维框架，探索未知的理论边界。

然而，当我们审视现代的AI，尤其是大语言模型时，我们发现它们并不像人类一样通过深刻的推理来解决问题。相反，LLMs是通过从大量数据中学习模式，自动生成合理的答案。虽然这种模式识别能力让它们在许多领域表现出色，但在数学推理中，它们往往面临着巨大的挑战。LLMs可能在面对复杂的数学推理时变得僵化，无法像人类一样灵活地调整策略，进行动态推理和多步骤推理。因此，尽管AI在执行某些常规任务时非常高效，但当面对需要创造性解决方案和深度思维的问题时，它们往往显得力不从心。

（三）AI对数学研究的潜在贡献：创新的催化剂

尽管如此，AI并非完全不能在数学研究中发挥作用。相反，它可以作为一种重要的辅助手段，帮助数学家们拓展思维，激发新的创意。例如，AI可以在构建数学对象、探索新颖的数学假设、或者通过高效的计算方法验证已有的理论方面，发挥其独特的优势。AI的创造性，尤其是在生成式AI领域，展现出它们在识别浅层模式的同时，能够为数学研究提供新的视角和解决方法。

在这篇《MATHEMATICS AND MACHINE CREATIVITY: A SURVEY ON BRIDGING MATHEMATICS WITH AI》论文中，作者强调了AI与数学的互动不仅仅是数学对AI的推动，更是一个双向的过程，AI能够在数学研究的过程中发挥创新的作用。这种跨学科的合作，正是我们在未来数学研究中所需要的关键。

二、AI 与数学的碰撞：从传统到生成式AI的进化

传统的人工智能（Symbolic AI）以基于规则的系统为核心，侧重于符号推理和决策制定。而近年来，生成式AI（Generative AI）的崛起引发了一场关于AI是否能够真正进行数学推理的讨论。通过这个部分，我们将深入探讨AI在数学领域的演变、它与数学的相互作用，以及生成式AI在数学探索中的潜力。

（一）传统人工智能：符号推理与规则系统

在传统AI时代，人工智能的核心思想是通过规则系统来模拟人类的推理过程。传统AI方法主要依赖于符号推理和显式编程的逻辑结构，强调确定性解答和基于形式逻辑的推导过程。例如，在解决组合优化问题时，广度优先搜索（Breadth-First Search）和深度优先搜索（Depth-First Search）等搜索算法能够有效地系统化地探索解空间。这些方法虽已取得一些成果，但由于计算复杂度的限制，当问题规模过大时，它们往往会变得低效或不切实际。

传统的AI虽然在解决某些数学问题时能够提供一定的帮助，但更多的是提供一种“框架”，帮助人们以结构化和形式化的方式去推理和计算。即使如此，它依旧面临着对复杂数学问题理解和创新能力的局限。

（二）机器学习：从数据驱动到模式识别

随着机器学习（ML）的出现，人工智能进入了一个新的阶段，重心逐渐转向从数据中提取模式和进行统计推断。与传统AI相比，机器学习更侧重于通过大量数据的训练来捕捉潜在的规律和关联。线性回归、逻辑回归、支持向量机等经典算法，都是基于统计学和数学理论构建的，通过对数据的分析，能够在一定程度上进行预测和分类。

尤其是在深度学习（Deep Learning）的兴起后，机器学习更是进入了一个全新的领域。深度神经网络通过自动化的特征提取，在图像识别、自然语言处理等任务中展现了令人惊叹的能力。深度学习将高维数据的处理能力发挥到极致，尤其是在复杂的数学计算和模式识别方面，表现出了传统算法无法比拟的优势。

（三）生成式AI：数学创新的新时代

而生成式AI的到来，则彻底改变了AI的功能，它不再只是依赖规则进行推理，而是具备了自动生成内容的能力。以Transformer为代表的架构在生成式AI中占据了主导地位。其核心创新在于“注意力机制”，允许模型在处理序列数据时能够动态地聚焦于输入的不同部分，从而更好地理解上下文信息。

生成式AI不仅能够生成高质量的文本，还可以生成图像、音频，甚至是代码。这一能力让生成式AI在数学领域的潜力逐渐被发掘，尤其是在数学推理、公式生成和新理论的构建方面，展现了巨大的前景。基于大量数据进行预训练的生成式AI，能够理解数学问题的语言并进行合理推理，甚至在一些复杂的数学问题上，能通过少量的例子和提示就得出合适的解答。

（四）生成式AI在数学中的创造性潜力

随着大语言模型（LLMs）的发展，AI逐渐展现出更多“创造性”的能力。例如，在解答复杂的数学问题时，LLMs能够通过少量的上下文理解问题，并生成合理的推理步骤。这种在上下文中学习的能力，意味着生成式AI不仅能回答问题，还能提出新的数学假设和洞察。

然而，尽管生成式AI在某些方面表现出色，它的推理能力仍然面临一些挑战。现有的AI模型虽然在标准的数学基准测试中取得了不错的成绩，但在处理一些更为复杂、抽象的数学问题时，依然存在一定的不足。这表明，尽管AI能够辅助数学研究，它的“思维”方式与人类的创造性推理存在显著差距。

AI不只是帮助数学家验证推理，更有可能帮助他们发现新的数学对象、构建全新的理论框架，甚至提出前所未有的猜想。与传统AI方法不同，生成式AI在生成输出时并不依赖于深厚的领域知识，而是通过高速的模式识别和生成能力，打开了数学探索的新天地。

通过跨学科的合作，AI与数学的结合不仅能拓展数学理论的边界，还能够在新的问题领域中提供创新的解决方案。因此，我们有理由相信，生成式AI将在未来的数学研究中扮演越来越重要的角色，推动数学的发展进入新的高峰。

三、人机共证：AI 参与数学证明的前沿探索

数学的灵魂在于证明。每一个定理的背后，都隐藏着逻辑的严谨推演与智慧的灵光闪现。

当我们提到“机器辅助证明”，很多人脑海中会自动浮现出一个图景：一台超级智能的 AI，接收一个数学命题后，像魔法师一样生成一整份完备的、严谨的、无懈可击的证明文档。这样的幻想听起来很美，却也反映出一个常见误解：认为 AI 已经可以完全替代人类来完成从定理提出到证明构建的整个过程。

事实远比这复杂。所谓“机器辅助”，更多时候意味着人类与 AI 的协同配合：AI 可能在查找已有知识、验证某个推理步骤的逻辑正确性，或提出某些有启发性的猜想方面提供支持，而真正的核心推导和抽象判断，仍然依赖于人的洞察力和经验。

在接下来的内容中，我们将深入解析当前 AI 如何参与数学证明的多个层面，既包括那些看似自动的证明生成系统，也涵盖一些更细腻但极具价值的“协助型”智能工具。你将看到，在这个人机共证的新纪元，AI 既不是数学家的对手，也不是接替者，而是一个充满潜力的“助手”——在正确引导和使用下，它有可能为数学研究开辟全新的思维路径。

（一）初衷与基础工具：从手工推理到机器验证的演进之路

数学界的“自动证明”并不是 AI 热潮下的新鲜玩意儿，它的历史可以追溯到上世纪五六十年代。那时，研究者们就开始尝试用计算机来模拟推理过程，希望机器不仅能运算，还能“讲理”。到1970年代，一些实用的数学证明辅助工具陆续问世，开启了“人机共证”的探索之旅。

为什么我们需要机器来参与证明？原因其实很朴素：有些数学问题的证明太长、太复杂，甚至需要逐个穷举所有可能的情况，比如著名的四色定理，其原始证明就涉及了对600多个子情形的穷尽验证——人类数学家靠纸和笔很难完整处理这么繁琐的工作。而计算机恰好擅长这种机械性强、规则清晰的任务，它们不怕重复、不怕枯燥，甚至可以“穷举到天明”。

但这里要划清一条线：最初这些机器并不是用来“创造”证明的，而是用来验证或辅助已经存在的推理。它们像是数学家的助手，负责检查逻辑是否严谨、推理链条是否闭环，或者负责那些重复而冗长的穷举部分。

不过，随着计算逻辑的进步，出现了一类更加自动化的工具，比如 SAT 求解器（解决布尔可满足性问题的工具）和一阶逻辑推理系统，这些被称为 自动定理证明器（ATPs），其中包括像 E（Schulz, 2002）和 Vampire（Riazanov & Voronkov, 2002）这样的著名系统。它们在许多子问题中能够完全自动地给出答案，也经常被集成到更高级的系统中，协助解决特定的推理步骤。

如今，数学证明中的主流工具是所谓的 证明助手（proof assistant），也叫 交互式定理证明系统（Interactive Theorem Provers, ITP）。这些系统就像数学界的“编译器”：你要用一种形式化语言去表达定理和证明过程，然后由后台的“证明引擎”来验证它们是否符合逻辑。

常见的证明助手包括：

Mizar [Trybulec, 1991]
Metamath [Megill, 2006]
Isabelle/HOL [Nipkow et al., 2002]
Coq [The Coq development team, 2004]
Lean [Moura and Ullrich, 2021]

这些工具在理论数学研究中发挥了巨大作用，尤其是在处理高复杂度或需要计算验证的场景中。例如，四色定理 和 开普勒猜想 的机器验证版本就是通过这些工具完成的。甚至像 Terence Tao 和 Peter Scholze 这样的大师级人物，也开始用 Lean 来参与严肃的研究项目。

但这类工具也有它的“门槛”：

它们无法自动生成推理步骤，只负责验证你输入的内容是否成立（虽然像 Sledgehammer 这样的工具尝试在一定范围内生成证明步骤，但现代 AI 工具有了更强的表现）。
它们使用的形式语言学习成本高、输入效率低。Terence Tao 曾坦言，使用 Lean 后，自己的研究效率降低了 25 倍！

来看看下面这个例子就知道为什么了。

左侧是用 Lean 语言写出的形式证明；
右侧是来自证明引擎的反馈。
当前反馈为：“No goals”，说明这个证明已经被验证为完备。

尽管这个命题看起来极为简单，但将它转化为机器可验证的形式逻辑语句，却需要写下许多行难以直观理解的代码结构。这正是目前 Proof Assistant 尚未广泛普及的主要障碍。

（二）自动化形式证明生成：AI 在严谨推理中的新进展

在传统数学中，形式化证明（formal proof）被认为是确保严谨性的终极标准，但一直以来它都被认为是一项极其繁琐、难以自动化的任务。过去的证明辅助工具如 Coq、HOL Light、Lean 等虽然在验证方面极为强大，却很难自动生成高质量的推理步骤——这也正是传统证明助手的局限之一。

近年来，得益于深度学习和大语言模型的突破，这一局限正在被打破。越来越多的研究和系统开始尝试让 AI 自动生成形式化的推理步骤，甚至是完整的形式化证明，这不仅仅是一项工程上的突破，更是对“数学是否可以被机器掌握”这一哲学问题的技术回应。

1. 关键特点：AI 证明系统三要素

目前主流的自动化证明工具，尽管技术细节不尽相同，但大致可以归纳为以下三个核心特征：

形式化输入与输出：这些工具的输入与输出都严格遵循某种形式化语言，如 Metamath、Coq、Lean、Isabelle 等，使其生成的证明步骤可以被现有的证明引擎准确验证。

与现有证明助手集成：自动化工具通常并不是独立运作，而是与传统证明助手进行紧密协作。它们通过调用验证器来确保每一步推理都符合逻辑规则。

融入机器学习技术：大多数工具都引入了深度学习或强化学习方法，用于学习如何预测接下来的证明步骤或如何规划完整证明路径。

1.1 早期探索者：RNN、搜索与强化学习的结合

从 2016 年开始，便有工具尝试使用深度学习自动构造形式证明：

Holophrasm（2016）是第一个尝试将 RNN 与形式语言 Metamath 结合的系统。它通过神经网络预测下一步证明，并结合树搜索策略构造完整证明。
HOList 则基于 HOL Light，采用强化学习范式进行训练，并在测试阶段通过广度优先搜索寻找正确的证明路径。
GamePad 和 ASTactic 接入 Coq 系统，前者尝试预测证明长度和步骤，后者使用 TreeLSTM 网络来进行步骤预测，并用 DFS 搜索完成证明。

这些系统为后来的“AI 数学家”打开了第一道门：证明可以由学习模型生成，验证可以交给证明引擎完成。

1.2 向交互式智能迈进：与人类协同工作的证明助手

像 Tactician 这样的新一代工具开始追求与人类数学家更自然的协作。它直接集成进 Coq 中，不仅能预测下一个可能的步骤，还允许用户进行修改、接受或拒绝。这种“AI 辅助 + 人类主导”的模式受到了很多用户的欢迎。

类似的还有 TacticToe（使用轻量级学习 + MCTS 搜索）和 TacticZero（深度强化学习 + 自动证明），它们分别集成于 HOL4 系统中，代表了“人机共证”的另一个方向：AI 生成，系统验证，人类监督。

2. 大语言模型的介入：从 GPT-f 到 COPRA 的新范式

随着 GPT 系列模型的兴起，语言模型也被引入形式化证明领域。与之前基于结构化神经网络的模型不同，大语言模型更擅长处理序列化的数据，这使得它们在训练过程中可以省去大量人工标注，极大降低了工程门槛。

GPT-f（OpenAI，2020）是首个尝试用 GPT 模型对 Metamath 进行形式证明的工具。它在大量数学文本和现有证明数据上进行训练，通过多步采样构建完整证明。
PACT（2021）进一步将此方法迁移到 Lean 系统中，并通过联合训练机制缓解数据稀缺问题。
Thor（2022）在 Isabelle 系统中引入“hammer”策略，能够在某些步骤调用外部定理证明器（如 Sledgehammer），以增强推理能力。
HyperTree Proof Search (HTPS) 则将 AlphaZero 的思路引入到 LLM 领域，通过 transformer 构建“策略模型 + 评估模型”结构进行搜索控制。
Baldur（2023）和 COPRA（2024）展示了两种截然不同但都依赖于大模型的方法：
- Baldur 将 LLM 一次性 fine-tune 成生成完整证明的能力；
- COPRA 则采用 step-by-step agent 风格，每一步调用 LLM 再送给验证器，并根据错误信息进行修复。

3. 更多范式的探索：递归式、Dojo 式、甚至 Olympiad 水平的 AI 数学家

除了逐步生成与一次性生成外，还有一些系统在探索更具层次性的生成逻辑：

POETRY（2024）提出了“层级递归式生成”思想：先草拟整个证明草图，然后逐层填补缺失细节，以避免贪心搜索带来的局部最优问题。
LeanDojo 是一个为 Lean 定制的全方位工具包，包含了名为 ReProver 的模型和高效的检索机制，既可以训练模型，也可以交互式使用。
最引人注目的或许是 AlphaProof，谷歌于 2024 年发布的 IMO 解题模型之一。它据说采用了类似 AlphaZero 的方法进行训练，能在 Lean 中自动完成奥赛级别的证明任务，虽然细节尚未公开，但它的出现标志着AI 生成的数学证明已达到竞赛级水平。

尽管方法层出不穷，当前自动形式证明依然面临关键挑战：高质量训练数据极度稀缺。形式语言和自然语言之间存在显著鸿沟，很少有数学家会手工写出完整的形式化证明。这就导致模型训练严重依赖合成数据或辅助任务，如自监督学习等。

这正是未来 AI 数学家的发展瓶颈：形式语言如何更易于书写？能否自动将非形式化推理转化为可验证的证明？

（三）自动形式化：让 AI 学懂数学语言

如果说“证明”是数学的灵魂，那“形式语言”就是通往这片灵魂世界的密钥。然而，这把钥匙并不好拿。想象一下，一位数学家写下了一篇详实的自然语言证明，想用 Lean、Isabelle 或 Coq 这样的形式化工具来验证它的正确性，却不得不将整篇证明用极其严谨、规范的形式语言重写一遍。这个过程被称为形式化（formalization），它枯燥、繁重，甚至令人望而却步。

比如，著名的开普勒猜想的形式化验证，就动用了 20 多年的人力时间积累（Hales et al., 2017；Szegedy, 2020）。这正是第二类关键障碍——“形式语言的学习成本”——最现实的体现。于是，研究者们提出了一个激动人心的方向：自动形式化（autoformalization），也就是让 AI 自动把自然语言数学表达翻译成形式化语言。与之相反的过程，叫做自动非形式化（autoinformalization），是把机器难以读懂的形式语言转译成人类习惯的自然语言，相对更容易实现，且在数学教学等场景中也非常有价值。

1. 从规则系统到神经网络：早期的尝试与突破

最初，人们尝试用规则系统（Bancerek et al., 1994）或统计学习（Kaliszyk et al., 2015）来实现自然语言与形式语言的互译。然而直到 Wang et al.（2018, 2020）提出基于神经网络的端到端翻译框架，才算真正跨越了一个门槛。他们用循环神经网络（RNN）将 LATEX 中的数学表达翻译成 Mizar 语言的形式表达，从而第一次以深度学习方法实现了“自动非形式化”任务。

但最大的问题在于数据：高质量的自然语言–形式语言（NL-FL）对齐语料极度稀缺。就像教小孩学中文需要成千上万的范例，AI 想学懂“数学语言”也需要大量精确匹配的 NL-FL 对。

2. 大模型介入：从模仿到理解

直到大型语言模型（LLM）的崛起，这一难题才有了解法。Wu et al.（2022）发现，即便是通用模型如 PaLM（Google, 2022）和 Codex（OpenAI, 2021），只需少量提示（few-shot learning），就可以将自然语言的数学陈述自动翻译成 Isabelle 这样的形式语言。

Agrawal et al.（2022）进一步验证了 Codex 在形式化整个证明过程中的潜力。更巧妙的做法来自 Jiang et al.（2023b）：他们让模型只给出形式化草图（proof sketch），也就是高层结构，由后续的自动定理证明工具来“补全细节”。这种人机协作的策略，有效缓解了 LLM 直接构造完整形式证明时易错的问题。

另一个值得关注的系统是 Llemma（Azerbayev et al., 2024），它是一类专为数学设计的大模型，能接受“非正式定理、正式定理、非正式证明”三元组作为输入，输出 Isabelle 风格的正式证明，显示出极高的可塑性和理解能力。

在 Wu 等人发现，大多数自动形式化错误其实源于自然语言和形式定义之间的不匹配后，Patel et al.（2024）提出了一个两阶段方法：第一阶段先用占位符形式化定理，第二阶段再将这些占位符“映射”回真实定义。

Lu et al.（2024b）进一步引入了一个创新机制：过程监督验证器（process-supervised verifier）。它通过 Lean 4 的反馈为模型输出打标签，从而形成可用于后续微调的“智能监督信号”。

3. 数据集构建：AI 数学语言教育的基础工程

要训练 AI“学懂数学”，不能没有教材。为此，研究者们构建了一批具有代表性的 NL-FL 数据集：

ProofNet（Azerbayev et al., 2023）：收集了 371 个自然语言–Lean 形式三元组，覆盖本科数学定理与证明；
MMA 数据集（Jiang et al., 2023a）：合成了 33 万条多语言数学定理–Lean 对应数据，用于多语种自动形式化研究；
Lean Workbook（Ying et al., 2024）：通过更精细的数据合成流程，生成了 5.7 万条 Lean 形式化定理，内容覆盖高中竞赛级别难度。

这些数据集已被广泛用于大模型的微调和新模型的预训练中，为自动形式化打下了坚实基础。

4. 形式化≠验证：自动评估的新挑战

不同于定理证明可以“算出对错”，自动形式化的输出是否真正表达了原定理的“意思”，并不能靠语法检查完成。Lu et al.（2024a）针对这一问题设计了一套新的自动评估体系：

确定性评分（certainty score）：模型对自己翻译的信心；
语义相似度评分：通过对比输入与输出的隐藏向量表示，评估它们是否在语义上“等价”。

虽然不能完全取代人工判断，但这套机制为未来大规模自动形式化应用奠定了评估基础。

自动形式化看似专为数学而生，但它背后的“自然语言 → 结构化逻辑表示 → 形式验证”的范式，已被认为有潜力推广至更广泛的领域，如科学发现、逻辑推理甚至政策分析（Szegedy, 2020；Zhou et al., 2024）。当 AI 不再只是搜索答案，而是构建逻辑、验证过程，这种“结构化思考”的能力，或许正是下一代智能系统的关键所在。

（四）全流程证明生成：从自然语言到完整证明的自动化路径

我们已经看到，大语言模型（LLMs）在辅助数学领域的能力正逐步渗透到推理的核心。但要真正迈向“全流程自动证明”这一目标，仍需跨越两个关键障碍：一是如何将自然语言的问题精确地转换为形式化语言；二是如何生成结构完备、逻辑严谨的证明，并能为人类所理解。

这一愿景被称为“端到端证明生成（End-to-End Proof Generation）”——从输入一个自然语言陈述，到输出一份完整的证明（形式化或自然语言形式），中间不再需要人工干预。

1. AlphaProof 的曙光与迷雾

2024 年，谷歌团队发布了引发广泛关注的 AlphaProof 系统，据称它已经在 IMO（国际数学奥林匹克）2024 上达到了“银牌水平”的解题能力。这个系统由两个主要模块组成：

Formalizer 网络：将自然语言的问题自动翻译为 Lean 形式语言；
Solver 网络：对形式化问题进行自动求解，生成形式化证明。

如果 AlphaProof 的性能真实可信，这将是 AI 数学证明的一大飞跃。

然而，研究人员对其成果提出了质疑：

实际测试中，很多问题并未经过自动形式化处理，而是手动翻译成形式语言，绕开了最关键的难点之一；
相比人类选手在 9 小时内完成全部题目，AlphaProof 需要耗时最长达三天来求解某些题目，远未达到实用化效率。

这些质疑提示我们，在评价 AI 数学能力时，不能仅看最终结果，更要关注过程是否真实地模拟了人类的解决路径。

2. 人机协同：草稿、结构与证明

相比直接生成完整证明，另一个更具“人类思维风格”的方法是“草稿-结构-证明（DSP）”模型。

这一方法由 Jiang 等人提出，其思路如下：

先由人类或 LLM 生成一个非正式的推理草稿（informal proof）；
然后用语言模型将草稿转化为“形式化证明草图（proof sketch）”，即一种高层次的逻辑框架；
最后调用现有的自动定理证明器（ATP）填补细节，生成完整证明。

这个流程将“人类擅长的大局思维”与“机器擅长的细节演绎”结合，既提高了效率，又保留了可读性。

类似的，还有 TheoremLlama 项目，其创新在于将自然语言推理嵌入到 Lean 代码注释中，在形式化证明中保留非形式的解释，从而让 LLM 更容易理解和扩展已有证明。

3. 自然语言证明生成：回归“人类语言”

相比形式化路径，还有研究者提出了一个更“直接”的方法：干脆用 LLM 直接生成自然语言证明。例如 NaturalProver 就采用了这种策略，它在 NaturalProofs 数据集上表现优于 GPT-3，能预测每一步的自然语言证明过程，并通过搜索生成完整证明链条。

这种方式虽然在可读性和教学应用上极具优势，但也面临一个根本问题：大语言模型是否真的“理解”了推理？

研究表明，当前 LLM 在推理任务上仍存在结构性局限。例如：

GSM-Symbolic 数据集测试发现，当问题语义结构被微调（即便表面意思相同），模型表现急剧下降；
当问题中插入无关信息后，LLM 的表现更差，说明它们很依赖上下文的模式匹配，而不是逻辑抽象；
Glazer 等人提出的数学研究级 benchmark 更进一步表明：截至 2024 年底，除了 OpenAI o3 模型外，所有主流模型在新颖数学问题上正确率不到 2%，暴露出深层次的“缺乏真正推理能力”的瓶颈。

“全流程证明生成”是一项挑战极高的任务，其路径正逐渐明晰：

对自然语言理解的精细化处理（通过 DSP、TheoremLlama 等技术）；

对形式化语言生成与验证的工程性提升；

对 LLM 理解能力的持续刻画与修正（通过挑战性 benchmark）。

或许，未来真正可靠的数学 AI，不是一台一蹴而就的“自动化机器”，而是一个善于“草拟-验证-完善”的数学合作者。

四、从识别模式到理论探索：AI 与数学家的共创旅程

真正的数学发现往往源于敏锐的直觉、跨领域的洞察以及对复杂结构中潜藏模式的感知。今天，随着人工智能尤其是大模型技术的迅猛发展，一种全新的合作模式正在浮现——机器发现模式，人类赋予意义，最终共同迈向理论的高峰。

（一）数据驱动的数学研究范式转变

传统数学研究多由“第一性原理”出发，构建自下而上的逻辑体系。这种方法固然稳健，却在面对复杂离散、高维数据结构时常感力不从心。尤其是在组合数学、数论等子领域中，随着计算技术的发展，海量数学对象的结构性数据被系统化采集和整理，人类研究者在模式识别方面的瓶颈越发显现。

此时，机器学习技术，尤其是监督学习模型，展现出其强大的函数逼近与结构感知能力，恰好补上这一短板。机器的长处在于它能从混乱中捕捉隐藏规律，人类的长处则是理解与升华这些规律。这种互补，为“人机共创”的数学研究打开了新局面。

（二）从数据中生发理论：人机协同框架的实践

研究表明：将数学对象表示为结构性数据、用模型从中提取模式、由人类提炼模型洞察为猜想并尝试证明，这一流程可以在微分几何、数学物理、代数几何、表示论等多个领域落地。

这一协作流程被 [Davies et al., 2021, 2024] 等人系统化后，首次在超曲面结理论（Hyperbolic Knot Theory）与表示论（Representation Theory）中取得突破。他们构建了如下的协同工作流，并在论文中以“欧拉公式”的再发现过程为例作了可视化说明。

我们以平面图类对象为例来解释这套流程：

1）假设阶段：设定一个数学对象集合 ZZZ，如“连通的平面图”，在这个集合上定义多个函数变量，如点数 VVV、边数 EEE、面数 FFF。数学家初步假设：这些变量间可能存在某种函数关系。

2）数据采集：使用程序从 ZZZ 中采样，得到大量样本，例如：

3）模型训练：将采集的数据输入到监督学习模型中，模型学得一个预测函数 $\hat{f}$ ，例如：

4）猜想形成：人类从中提炼出更为简洁的数学关系：

这恰是欧拉著名的公式。

这种协作流程，不仅仅能“复现”已知结果，更重要的是它在某些高阶数学领域中也能挖掘出真正的新猜想。例如 [Dong et al., 2024] 利用类似流程，在 affine Deligne–Lusztig 变体研究中提出了新的公式，极大拓展了该方向的理论边界。

（三）从模式识别走向生成性思维

尽管监督学习在理论探索中已大显身手，但生成式 AI 模型，尤其是大规模 Transformer 网络，目前在数学中的应用仍处于初期阶段。近年来的研究开始逐步探索其潜力：

[Johansson & Smallbone, 2023] 使用 LLMs 在 Isabelle/HOL 形式系统中进行猜想生成；
[Gao et al., 2024] 结合 Transformer 与扩散模型预测复杂动力系统演化；
[Hashemi et al., 2025] 设计 Transformer 网络用于代数几何中的枚举任务，具体预测 ψ-类交点数。

Hashemi 团队提出了一种新型激活函数 DRA（Dynamic Range Activator）并结合共形预测方法，使模型在保持预测准确性的同时也输出了不确定度估计。更为关键的是，他们对模型内部结构进行了剖析，发现网络中隐藏层的“表示”与问题本身的几何结构具有深刻对应。这一发现表明，某些 AI 网络不仅能预测结果，更可能捕捉到某种“数学意义”上的世界结构。

总而言之，从函数拟合到生成性理解，从辅助猜想到概念孕育，AI 正在逐步从“数学的工具”成长为“数学的伙伴”。但正如所有理论探索一样，真正的突破仍需要人类的洞察与勇气。未来，人机将共登数学高峰，一同走进那些尚未书写的定理与公式之中。

五、显式构造数学对象：从强化学习到语言模型的双路径探索

在数学研究中，我们常常需要明确构造出某个对象——这可能是一个函数、一个图、一个操作序列，或一个反例。与上一节讨论的“发现模式”不同，这一任务的目标不再是寻找某种“潜在的猜想”，而是亲手搭建出满足特定条件的结构或程序，就像数学家在黑板上一步步推导一样。这项工作也许更接近“创作”而非“验证”，而 AI 在这方面的探索已经初具规模，主要分为两种主流方法：基于强化学习（Reinforcement Learning, RL）的方法和基于语言模型（Language Model, LM）的构造路径。

（一）强化学习方法：构造的决策旅程

强化学习本质上是一个序列决策框架，AI 代理在其中通过与环境交互一步步累积经验，从而学会做出最优动作。令人兴奋的是，这一思路已被应用到复杂的数学构造中——包括拓扑学中的结论简化、图论中的反例寻找，甚至是优化算法的自动设计。

结论化简的RL演绎
Gukov 等人（2020，2023）将 RL 应用于结理论（Knot Theory）。他们让 AI 学会如何对一个复杂的结图执行一系列合法操作，使其逐步简化为“无结”（unknot）状态。这个过程本质上就是一个“变形步骤的搜索”，正适合用 RL 的策略迭代方法建模。
图论中的AI反例创作家
更进一步，Wagner（2021）设计了一个框架，使 AI 能够一步步构造出反例，用于否定某些图论中的未解猜想。例如，在构造一个满足某种极端条件的图时，AI 每添加一条边就根据“奖励函数”评估当前图是否接近目标。AI 最终合成出的反例其复杂度远超人类传统方法。
算法和控制系统的自动设计
这一思想还被推广到其他领域：如 Fawzi 等人用 RL 设计快速矩阵乘法算法（2022）；Bidi 等人构建用于动态系统的稳定控制器（2023）；Farahmand 等人则在偏微分方程（PDE）控制设计中引入 RL（2017）。

这些探索表明，强化学习不仅能在围棋中击败人类，更能在数学构造问题中成为新型合作者。

（二）语言模型路径：从语义到构造的创造性跳跃

如果说强化学习是一种“脚踏实地”的策略搜索工具，那么基于语言模型的构造方法更像是“灵感飞扬”的创造机器。

1. 🧠 从零训练的语言模型：构造函数与组合结构

李雅普诺夫函数的生成实验
Alfarano 等人（2024）训练了一个专门的 transformer 解码器模型，用于构造李雅普诺夫函数。李雅普诺夫函数是判断动态系统稳定性的重要工具，而传统算法往往只能应对简单系统。该团队利用超过 200 万条合成样本数据训练模型，让其可以在测试时通过“逐词生成”的方式构造函数，最终超越了经典算法和人类表现。
图论中的高评分构造问题
Charton 等人（2024）则瞄准了一类更开放的问题：目标不是构造满足某个固定条件的对象，而是尽可能构造得“更好”。他们定义了某种“打分机制”，以筛选高质量组合对象。构造过程被分为两阶段：先用 transformer 模型大规模生成备选样本（如10万条），再由人或程序进一步筛选和修正，这种“全球-局部”式流程使得系统表现逐步进化。