AI与数学发现：机器能否成为数学家？

2024年，DeepMind的AlphaProof在IMO（国际数学奥林匹克）中达到28分——满分42，达到银牌分数线。[1] 这不是一道题得分，而是AI在没有人类证明示例的情况下，通过强化学习自我训练，最终在最高难度的中学生数学竞赛中与人类顶尖选手同台竞技。这条新闻迅速点燃讨论：AI是否正在成为真正的数学家？

答案并不简单。AI在数学领域的能力正在多条战线上突破，但”解题”与”发现”是截然不同的两件事——前者有标准答案可循，后者需要提出人类尚未提出的问题。本文基于25篇学术论文，梳理AI在数学推理与数学发现两条战线上的真实进展与仍未跨越的边界。

自动定理证明：三大突破

AlphaGeometry：无师自通的几何证明

2024年发表于《Nature》的AlphaGeometry是首个完全不需要人类证明示例的IMO级几何证明系统。[2] 它采用神经符号混合架构：用神经网络预测”在何处构造辅助线”，再交由符号系统展开证明搜索。30道IMO几何题解决了26道，接近金牌选手水平。训练数据完全由系统自我合成，无需人类示范——这是一种”无师自通”的架构。[2]

后续研究将吴文俊方法与AlphaGeometry结合，将IMO几何问题解决率提升至金牌水准——符号与学习的混合路径已被证明是通向更强数学推理的有效方向。[3]

AlphaProof：自我训练的强化学习证明器

如果说AlphaGeometry解决了”如何构造辅助线”，AlphaProof则试图回答更根本的问题：能否让AI从零学会证明任何数学陈述？[1]

AlphaProof将大语言模型与形式化证明器Lean相连接：模型生成候选证明，Lean逐行验证正确性，通过验证的证明路径成为强化学习的训练信号。这种”自我训练”机制——从自己生成的正确证明中学习——是AlphaProof的核心魔力所在。[1]

混合系统的规模化

IMO-GRAND采用分层架构——大语言模型负责策略选择，传统ATP负责底层逻辑搜索——在IMO问题上比纯符号系统提升约40%的证明成功率。[4] “锤子”策略（多ATP并行搜索）与大语言模型结合后，在Mizar数学库上将证明率提升约15%。[5]

大语言模型的数学推理能力

在自动定理证明之外，另一条平行战线的进展同样激动人心。2022年Google的Minerva展示了大规模预训练对数学能力的惊人提升——在arXiv数学论文和网页数学文本上训练后，MATH和GSM8K基准性能大幅跃升。[6]

此后三条技术主线并行推进：Chain-of-Thought（思维链）提示让模型显式输出推理步骤，[7] 数学专用的强化学习训练（WizardMath的RLAIF方法、DeepSeekMath的GRPO方法）显著超越基础模型，[8] [9] 开源数据集OpenMathInstruct（180万问题-解答对）驱动开源模型快速追赶GPT-4水平。[10]

一个关键方向是过程级验证。MATH-SHEPHERD为每一步推理提供过程级标注，能识别长推理链中哪一步出错，为改进推理稳定性提供了训练信号。[11] SELF-DISCOVER框架则让模型自主组合推理结构，使GPT-4在数学基准上提升约30%。[12]

然而，数学解题能力的提升并不等同于数学发现能力的提升。前者有标准答案可循，后者需要提出人类尚未提出的问题——这是根本性的跨越。

形式化数学：连接直觉与严格证明

形式化数学（Lean、Isabelle、Mizar等）近年来成为AI数学研究的重要基础设施——形式化证明可被计算机逐一验证，每一步对错有明确判定。

Autoformalization：翻译人类直觉

autoformalization探索让LLM将自然语言数学证明自动翻译为形式化证明。GPT-4在Mizar数据集上达到约40%的自动形式化成功率，[4] 这一数字意味着LLM已捕捉到自然语言证明中相当一部分结构化信息。

Lean Copilot与视觉推理空白

Lean Copilot将大语言模型作为Lean证明助手，提供tactic推荐和前提搜索，显著加速形式化证明过程，降低形式化数学的门槛。[13]

但视觉数学推理仍是空白。MathVista测评显示，GPT-4V在视觉数学问题上的解决率仅约49%。[14] 几何作图、函数图像分析——这些对人类数学家稀松平常的能力，对AI仍是未解决的挑战。

AI真正发现了什么

AlphaTensor：突破人类50年纪录

2022年的AlphaTensor是AI首次在真实数学问题上独立超越人类已知最优解。矩阵乘法是线性代数的基本运算，其效率直接影响从机器学习训练到科学计算的无数应用。1969年，施特拉森（Strassen）发现仅需7次乘法运算即可完成2×2矩阵乘法，这一”Strassen算法”将乘法步骤从传统方案的8次降至7次，保持了五十余年的最优记录。AlphaTensor在此基础上发现了更少的乘法步骤方案——打破了施特拉森及其后继者改良版本的23步记录。[15] 但这是在高度形式化且封闭的搜索空间中完成：问题边界明确，评估函数清晰。

FunSearch：从搜索到生成猜想

FunSearch将LLM与进化算法结合，在最大独立集问题（组合优化中的经典NP难问题）和大cap set问题（组合数论中的重要问题）上生成的方案均超越了人类数学家的已知最优结果。[16] 更值得关注的是：FunSearch直接生成数学猜想的候选对象——AI不只找更好的解，而且在产生对人类而言新颖的数学对象。自动猜想生成的研究进一步显示，多个LLM协作可生成、验证、筛选数论和组合数学中的新候选猜想，部分已获人类数学家初步验证。[17]

边界与未解之谜

最核心的区分在于：数学推理 ≠ 数学发现。数学推理是从已知前提推导结论，有明确对错标准；数学发现需要提出正确的数学问题，依赖对数学结构的深层直觉、对不同领域之间联系的敏感性，以及对”什么问题是真正重要的”的价值判断——这些仍属人类数学家的领地。[7]

封闭空间 vs 开放数学

AlphaTensor在固定大小矩阵乘法中发现新算法，FunSearch在特定组合问题上超越人类最优——这些都是封闭搜索空间。而在真正的数学研究中，问题本身往往需要被界定，AI在开放数学环境中的发现能力，目前证据极为有限。

理解还是模式匹配？

LLM本质上是基于大规模语料训练的概率模型。其”数学推理”究竟是真正的形式理解，还是复杂的模式匹配？支持”真实理解”的学者会指出AlphaProof的自我训练机制——它从零学会生成正确证明，难以用单纯的记忆解释；质疑者则指出，LLM在某些基础数学问题上仍会犯”粗心的”错误，这表明其内部可能并不存在稳定的数学对象表征。[7]

Proof Artifact Cartography技术已能可视化LLM在证明过程中的决策点，[18] 但”观察AI在想什么”距离”判断AI是否真正思考”仍有本质差距。这不仅是技术问题，更是关于”什么是理解”的哲学问题。

数学研究中最有价值的部分——提出正确的问题、建立看似无关领域之间的联系、对一个猜想是否值得关注做出价值判断——这些恰恰是当前AI最难触及的领域。AI或许能证明黎曼猜想的每一个推论，但它能提出黎曼猜想本身吗？至少在目前，尚未有证据表明它能做到。