从“做题机器”到“研究伙伴”：AI如何重塑数学探索的边界？

当我们抛给人工智能一道数学题，它常常能很快给出答案，甚至写出一段看起来颇为完整的证明。但更有意思的问题是：如果面对一个没有标准答案、数学家自己也不知道答案的研究课题，AI还能做什么？它能成为数学家的研究伙伴吗？

这个问题正在成为“AI for Mathematics（AI4Math）”研究的重要方向。

数学研究远不只是“做题”。一个真正的研究问题，往往要经历提出猜想、查阅文献、尝试证明、寻找反例、计算验证、修改结论，再到形成严格证明等一系列过程。

应用数学还需要进一步经历建模、算法设计、数值实验和结果验证。换句话说，数学研究不是一次问答，而是一条漫长的探索链条。

今天的人工智能正在逐渐进入这条链条。

大语言模型的一项突出能力，是能够快速探索大量可能性。面对一个研究问题，它可以提出不同的证明思路、尝试不同的参数、比较已有方法，甚至根据计算实验不断修改猜想。

一种很有代表性的模式可以概括为：

提出候选—实验检验—严格证明。

北京大学团队在研究Grover量子搜索相关的数学优化问题时，就尝试让AI参与这样的过程。AI首先提出可能的分析路线和关键参数，再通过数值实验进行“压力测试”；研究人员则进一步检查其中隐藏的数学结构，AI最终帮助完成严格证明。

在这一过程中，AI负责扩大探索范围，数学家负责判断哪些方向真正有价值，并对最终结论负责。目前该论文已经被计算数学顶级期刊SIAM Journal on Scientific Computing正式接收。

这与我们通常想象的“让AI替人做一道题”很不一样。更准确地说，AI更像是一位能够高速阅读、不断尝试、不会疲倦的研究助手。它可能在短时间内探索几十条路线，其中多数最终失败，但某一条路线可能为数学家提供新的启发。

数学家的价值，也因此从“完成大量尝试”，进一步转向“提出好问题、识别好结构、判断什么值得证明”。

人机协同数学研究流程示意图

图片来源：文再文 提供

这也是AI进入数学研究后最关键的问题。

数学家写证明时，经常使用“显然”“类似可得”“不难证明”等表述。这些省略对于专业研究者来说往往可以理解，但对于计算机而言，每一步推理都必须明确。因此，人们发展出了一类特殊的工具——形式化证明系统。

所谓形式化证明，就是把数学中的定义、假设、定理和推理步骤写成严格的机器可读语言，再由计算机逐步检查。在Lean等交互式定理证明器中，只要证明中存在不符合逻辑规则的一步，系统就不会让它通过。

可以把Lean想象成一位极其严格的“数学审稿人”。

它不会因为一段证明写得流畅就点头，也不会接受“看起来应该成立”。它只检查一件事：

这一步，真的能够从前面的假设和已经证明的定理推出吗？

于是，一种很有意思的新型人机协同方式出现了：

大模型负责提出具体证明步骤，形式化系统负责检查；如果检查不通过，AI根据错误信息继续修改。

在北京大学ReasLab形式化系统中，这一过程包括识别数学定义和目标、构造形式化命题、检索相关定理、生成证明，再交给Lean编译验证，并根据反馈不断修正。

可以把这种机制概括成一句话：

AI负责大胆探索，形式化系统负责严格验证。

如果AI能够形式化一个定理，下一个问题自然是：它能不能处理一整本数学教材？

这要困难得多。

一本数学书中的知识彼此高度依赖。后面的一个定理，可能依赖几十页之前的定义、符号和引理。要让机器真正理解一本书，不能只把每个定理孤立地翻译出来，还要同时处理其中复杂的依赖关系。

为此，北京大学团队开发了文档级自动形式化系统Quokka。它的目标是将长篇数学文献自动转化为可以编译检查的Lean4项目：大语言模型提出形式化方案，Lean进行严格裁决，同时保留数学原文与形式化代码之间的对应关系。

Quokka文档级形式化示意图

图片来源：文再文 提供

目前，Quokka已将陶哲轩的《Analysis II》和Rockafellar的《Convex Analysis》等经典教材完整转化为机器可验证的Lean形式化资源，累计生成约300万行Lean代码。

这意味着，未来一篇数学论文或者一本数学教材可能同时拥有两个版本：

一个是写给人看的版本，方便阅读、理解和学习；甚至可以生成交互式定理依赖图，以可视化方式清晰呈现所有定义、定理及其关联关系，支持点击任意节点，一键溯源。

交互式定理依赖图案例

（https://optpku.github.io/ReasBook/theorem-maps/papers/tr_lalm_theory）

另一个是写给机器看的版本，其中每个定义、定理和证明都可以被检索、调用和验证。

如果越来越多的教材、论文和定理都变成机器可读的知识，AI还可以进一步建立数学知识之间的关联：一个结论依赖哪些假设？一个定理可以用哪些引理证明？不同领域之间是否存在相似的结构？

这就像为机器建立一部可以计算、检索和验证的“数学百科全书”，把分散在教材和论文中的定义、定理、算法与依赖关系组织成可检索、可复用的数学知识基础设施。

因此，AI4Math真正令人期待的，并不是让机器取代数学家。

未来更可能出现一种新的分工：AI负责大规模搜索与尝试，数学家负责提出重要问题、发现关键结构和作出学术判断，形式化系统则提供机器可检查的逻辑验证。

当数学家的直觉、人工智能的探索能力与形式化系统的严格验证结合起来，AI就有可能从一个“会做数学题的工具”，成长为数学家的研究伙伴。

参考文献：

1.Li Chenyi, Lai Zhijian, An Dong, Hu Jiang, Wen Zaiwen, Advancing Mathematical Research via Human-AI Interactive Theorem Proving, arXiv:2512.09443

2.Lai Zhijian, An Dong, Hu Jiang, Wen Zaiwen, A Grover-compatible manifold optimization algorithm for quantum search, SIAM Journal on Scientific Computing, 2026, accepted, arXiv:2512.08432

3.Wang Zichen, Ma Wanli, Ming Zhenyu, Zhang Gong, Yuan Kun, Wen Zaiwen, M2F: Automated Formalization of Mathematical Literature at Scale, arXiv:2602.17016

4.数学论文、形式化代码、定理依赖图案例： https://github.com/bqliu815/NR-LALM

5.Quokka: https://quokka.reaslab.io

6.智能数学推理引擎：https://reaslab.io/

7.数学百科全书demo：https://atlas.reaslab.io/

作者：文再文  北京大学北京国际数学研究中心 教授

审核：刘颖 李培元 张超 杨柳