数学之问②｜AI 如何重塑数学研究？从辅助工具到共创伙伴的演进

AI 对数学研究的影响并非一蹴而就，而是历经数十年演进，从早期的计算辅助逐步发展为具备协同能力的研究伙伴，每一步突破都与具体技术工具和学术实践紧密相关，深刻改变着数学研究的范式与边界。

（一）机械验证与形式化萌芽（1970s-2000s）

这一阶段的核心是将数学证明从 "纸面推理" 转化为 "机器可验证代码"，计算机开始承担起 "超级校对员" 的角色，其核心价值在于通过严格的形式化逻辑消除人类证明中可能存在的模糊性与疏漏。

1976 年，Appel 与 Haken 对四色定理的证明堪称里程碑 —— 这个困扰数学界百年的难题，要求证明 "任何平面地图只需四种颜色即可区分相邻区域"，其关键在于验证 1834 个 "可约构形" 的逻辑自洽性。由于人工计算难以完成如此庞大的工作量（仅单个构形的验证就需数页推导），研究者首次引入计算机进行批量验证：他们将每个构形转化为可计算的逻辑命题，机器则逐一检验其 "可约性" 与 "不可避免性"。但此时的机器仅能执行预设的计算步骤，核心的构形选择仍完全依赖人类直觉，Haken 的女儿 Dorothea Blostein 甚至需要手工核对数百页微缩胶片的计算结果，期间还发现了多处可修复的错误。这一突破引发学界激烈争议：哈佛大学数学家 Mackenzie 批评 "这更像工程验收而非数学证明"，而支持者则认为它开辟了新路径。

2005 年，Gonthier 使用 Coq 证明助手完成四色定理的形式化验证，标志着形式化方法的成熟。形式化的核心是将每一个数学概念（如 "自然数"" 平方 ""等式"）都转化为严格的逻辑定义，每一步推理都必须符合预设的规则。这种近乎苛刻的严谨性，让数学证明首次摆脱了 "人类直觉可能出错" 的隐患。正如研究指出的，形式化证明 "为争议性成果提供了极高的正确性保障，尤其适合那些因过于冗长而难以找到评审的复杂证明"。

这一时期的另一标志性项目是 "Flyspeck 计划"。1998 年，Hales 通过复杂计算证明了开普勒猜想（三维空间中最密的球体堆积方式为面心立方堆积，堆积密度约为 74%），但由于证明过程涉及数百万个几何构型的分析与优化，传统人工评审难以完全验证其正确性 —— 评审团在经过数年审查后仅能表示 "99% 确定证明正确"。为此，Hales 于 2003 年启动形式化验证项目，原计划需 20 年，最终在 21 位研究者协作下用 11 年完成。过程中，计算机不仅确认了原证明的正确性，还纠正了几处微小疏漏（如一个几何不等式的边界条件设定偏差）。Hales 感慨："这就像用显微镜检查艺术品，虽繁琐却能发现肉眼遗漏的细节。" 这种 "人类提出框架 + 机器验证细节" 的模式，为后续更复杂的定理证明提供了可复用的范本。

（二）算法驱动的逻辑推理（2010-2020）

随着算法理论与算力的提升，机器开始处理超大规模逻辑推理，SAT（布尔可满足性问题）与 SMT（可满足性模理论）求解器成为核心工具，其能力远超人类手动计算极限，开始触及一些传统方法难以解决的数学问题。

2016 年，Marijn Heule 团队用 SAT 求解器解决 "布尔毕达哥拉斯三元组问题" 的成果登上《自然》杂志，引发学界广泛关注。团队通过计算机证明得出结论：N=7824 是满足条件的最大数，而 {1,...,7825} 则无法实现这样的划分。

这个证明堪称 "暴力推理" 的典范：计算机耗费 4 CPU 年（单台电脑约 1460 天）运算，生成 200TB 原始数据，压缩后仍达 68GB。其创新之处在于采用 "分而治之" 的启发式策略 —— 将问题拆解为数千个子命题，用剪枝算法优先处理最可能成立的路径，最终找到满足条件的划分方式。普林斯顿大学教授 Conway 曾质疑："人类永远读不完这样的证明，它还能算数学吗？" 但学界最终承认，这种方法拓展了数学证明的边界 —— 有些真理，或许只能通过机器才能触及。

同期，形式化证明工具的应用范围持续扩大，开始深入更抽象的数学领域。2019 年，数学家 Scholze 启动 "液体张量实验"，旨在形式化验证他与 Clausen 关于 "液体向量空间" 的重要定理。这个仅 10 页的人类证明，因涉及大量凝聚态数学的前置知识（如完美畴、固体向量空间等抽象概念），形式化过程异常复杂：研究者需要先将这些概念转化为 Lean 证明助手可理解的定义，再逐步验证定理的每一步推导。整个过程耗时 18 个月，集结了全球数学家协作完成，最终 Lean 确认了定理的正确性，同时也让这个抽象领域的逻辑框架更加清晰。参与项目的学者发现，形式化过程迫使他们重新定义每一个模糊的概念（如 "液体性" 的严格数学描述），这种 "慢思考" 反而让理论体系更坚固。

这一阶段的机器辅助证明已展现出明显的 "协作性" 特征：人类负责提出核心猜想与证明框架，机器则处理规模化的逻辑验证，二者形成互补。例如在开普勒猜想的形式化中，研究者发现原证明中一个被认为 "显然成立" 的引理（关于某类多面体体积的不等式）其实需要更严格的推导，而机器的严格性恰好弥补了人类直觉的疏漏。

（三）深度学习与大模型时代（2020 至今）

2020 年以来，深度学习与大语言模型的发展使 AI 从 "验证工具" 升级为 "发现助手"，开始主动参与数学规律的挖掘与猜想的生成，这一转变彻底重塑了数学研究的范式，让机器从 "证明的执行者" 变为 "规律的探索者"。

在形式化证明领域，Lean 等工具与 AI 的融合催生了新工作模式，人机协同的深度进一步提升。陶哲轩团队 2023 年的实践颇具代表性：他们利用 Lean 对加法组合学中的一个定理进行形式化证明，33 页的人类证明经 20 位研究者三周协作完成转化。过程中，机器不仅发现原证明中一处引理的冗余性（该引理看似必要，实则可由其他条件推导得出），还通过对证明结构的分析，提炼出更通用的证明框架，可适用于更广泛的组合问题。陶哲轩在分享中提到，使用 Lean 初期让他的工作效率暂时下降了 25 倍（这一比例被称为 "de Bruijn 因子"），但这种 "被迫放慢的思考" 反而带来新洞察 —— 形式化迫使研究者拆解每一个模糊的步骤，重新审视证明的逻辑链条。他还观察到，随着 AI 辅助工具的完善（如自动引理推荐、证明路径预测），de Bruijn 因子正快速下降，未来有望降至 1 以下，这将彻底改变数学研究的效率。

AI 在规律发现与猜想生成上的能力也日益凸显，开始在数据中挖掘人类难以察觉的数学关联。Davies 团队在纽结理论中的研究堪称典范：纽结的 "signature 值"（一个刻画拓扑性质的整数）与双曲不变量（描述纽结补空间几何特征的参数，如双曲体积、陈省身不变量等）看似毫无关联，而他们用神经网络分析近 200 万个纽结数据后发现，仅三个参数（纵向平移、meridional 平移的实部与虚部）就决定了 signature 值的变化。通过显著性分析（一种衡量输入特征对输出影响的方法），研究者排除了其他 21 个无关参数，最终引导数学家证明：signature 值与这三个参数存在明确的解析关系（可表示为某个二次型）。这种 "机器发现规律 — 人类证明规律" 的模式，已在微分几何、表示论等领域广泛应用，其核心价值在于突破人类直觉的局限 —— 机器能从海量数据中识别出被噪声掩盖的深层关联。

大语言模型的加入进一步拓展了 AI 在数学研究中的应用场景，开始模拟人类的逐步推理过程。GPT-4 等模型在美国数学邀请赛（AIME）中的表现接近优秀高中生水平，能独立解决部分国际数学奥林匹克（IMO）试题。但同时，这些模型也暴露出 "幻觉" 缺陷 —— 例如在计算 "7×4+8×8" 时，曾先给出错误答案 120，随后又用正确步骤推导出 92，这种矛盾源于其 "模式匹配" 而非 "逻辑演绎" 的工作机制：模型更擅长模仿人类推理的表面形式，却难以掌握数学的深层逻辑。

不过，针对这些缺陷的改进方法正在涌现。2024 年，DeepMind 提出的 FunSearch 框架让大语言模型生成 Python 程序解决组合问题，在 Cap set 问题上超越人类构造的最好结果。其核心是 "生成 — 验证" 循环：LLM 提出候选程序，外部数学工具检验其正确性，优质结果反馈给模型优化下次生成，这种闭环有效抑制了 "幻觉"。同期，AlphaGeometry 结合符号推理与神经网络，在 IMO 试题中超越人类平均水平，其对 2004 年第 4 题的证明引入虚数坐标系，将几何问题转化为代数运算，这种跨界思路连资深几何学家都感到惊讶。

此外，AI 在构造数学对象上展现出独特优势。Wagner 用强化学习构造出极值图论的复杂反例，其结构复杂度远超人类手动构造水平；Fawzi 团队通过强化学习发现更快的矩阵乘法算法，打破了 decades-old 的纪录；AlphaEvolve 不仅解开 300 年悬而未决的 "接吻数问题"（三维空间中最多有 12 个等径球同时与一个中心球相切），还在 14 个数学任务上实现技术突破。这些案例印证了 AI 在 "构造性问题" 上的潜力 —— 通过海量试错与策略优化，机器能找到人类难以想到的特殊结构。

值得注意的是，当前 AI 的创新仍有明显局限。剑桥大学数学家 Kevin Buzzard 指出："AI 能生成漂亮的证明步骤，却提不出 ' 朗兰兹纲领 ' 这样的宏大理论。" 机器的突破多源于对海量数据的统计归纳，而人类数学家能从看似无关的领域中提炼出统一框架（如朗兰兹纲领将数论、代数几何与表示论联系起来），这种 "从 0 到 1" 的原创性，仍是 AI 尚未跨越的鸿沟。