当AI遇见数学——智能证明助手是颠覆者还是好帮手?

分享一篇来自经济学人2026年4月刊出的文章。

导语：

从困扰数学家数百年的“球体堆积”难题，到前沿的高维空间证明，人工智能正以前所未有的方式介入最纯粹的数学领域。它究竟是来抢饭碗的，还是来当助手的？

一、从“信任瓶颈”到AI介入

数学证明的严谨性要求每一步都经得起最苛刻的检验。1998年，托马斯·黑尔斯对“最密球体堆积”猜想的证明，花了同行十多年时间才被完全验证。这个过程凸显了数学进步的一个核心瓶颈：信任与验证的效率。

正是为了突破这一瓶颈，研究者们开始将目光投向人工智能。美国国防高级研究计划局（DARPA）的科学家帕特里克·沙夫托指出，利用AI（特别是精通数学的大语言模型）来加速证明的形式化验证，有望为数学研究按下“快进键”。

二、AI的“意识流”与人类的“规划式”思维

有趣的是，AI处理数学逻辑的方式与人类截然不同。顶尖数学家陶哲轩比喻道，人类证明像精心编写的剧本，步步为营；而AI的推理则更像“即兴对话”，是一种基于概率预测的“意识流”。这种差异化的思维方式，反而让AI在一些特定问题上表现出色，近期已成功解决多个长期悬而未决的数学难题。

三、核心战场：让AI的推理“看得懂”

要让AI真正成为数学家的帮手，关键挑战在于让其推理过程对人类透明可理解。目前，多家机构和公司正从不同角度攻关：

谷歌DeepMind：开发了如AlphaEvolve等工具，允许用户用自然语言描述优化问题，由AI生成证明。同时，其DeepThink AI致力于让AI的“思考”过程更易于被人类追踪。

初创公司Harmonic：其AI系统“亚里士多德”能将数学家非正式的证明草稿，转化为基于Lean等形式化证明语言的严密代码，并自动补全缺失的步骤，最终输出逻辑无懈可击的完整证明。

初创公司Math, Inc.：其模型“高斯”成功将关于8维和24维球体堆积的复杂证明（由数学家玛丽娜·维亚佐夫斯卡完成）进行了形式化，不仅验证了结果，还帮助数学家更深层地理解了证明中使用的工具。

四、AI的“怪癖”与人类的不可替代性

然而，AI并非万能，其局限性同样明显：

缺乏“数学审美”：剑桥大学的蒂莫西·高尔斯教授指出，AI难以将解决一个问题的经验迁移到另一个问题上，更缺乏人类数学家那种寻找更优雅、更本质证明的“审美”驱动和创造力。在需要颠覆性创新的领域，人类仍占优势。

难以预料的故障：AI有时会以奇怪的方式“卡壳”。例如，斯坦福大学的高德纳教授在尝试用AI解决一个旅行商问题（一个经典的组合优化问题）时发现，AI能完美处理“奇数”路径的情况，却在面对“偶数”路径时完全“死机”，连基本的推理代码都无法正确生成。这提醒我们，AI的推理稳定性仍需提升。

五、未来：协作而非替代

DARPA的愿景是构建一个统一的“数学知识体”，将散落在论文、教科书和人脑中的知识结构化，降低年轻学者入门门槛。但这并不意味着数学家会被取代。

当前，数学专业知识对于有效使用和纠错AI仍然至关重要。正如沙夫托博士所说：“AI会犯错，你必须有能力找出错误所在。”未来的模式更可能是“人类直觉引导方向，AI负责繁重验证与细节填充”的深度协作。

结语：

AI不会让数学家失业，但善用AI的数学家可能会让不用AI的数学家感到压力。这场人机协作的试验，最终目标不是替代人类智慧，而是解放它，让数学家们能更专注于提出那些真正伟大而深刻的问题。