AI 在数学领域的应用：迫使人们思考根本性问题

背景

回顾 2000 年代中期，应用数学的研究往往侧重于模拟和近似，例如利用简单方程来理解液晶中特殊光波的相互作用。如今看来，这类工作若借助 AI 辅助，可能仅需数天甚至数小时即可完成。然而，与之形成鲜明对比的是当时在爱丁堡大学共事过的纯数学博士生的处境。他们长期沉浸在抽象的数学问题中，看似毫无进展，甚至多年未发表任何论文。

作者曾误以为这是出于傲慢或某种形式的受虐倾向，但事后才意识到，这些数学家从漫长的探索和理解过程中获得了巨大的喜悦、满足感和意义。这种对“理解之美”的追求是数学家的核心驱动力。然而，随着大型语言模型（LLMs）等 AI 系统的发展，这种需要长时间深思熟虑的传统数学研究范式正受到挑战。AI 正在介入并加速这一过程，引发了关于数学家角色、动机以及数学领域未来的深刻辩论。

核心内容

数学家的核心驱动力：理解之美

卡内基梅隆大学的数学家 Jeremy Avigad 描述了数学家特有的体验：“有时，理解本身就会让你觉得非常美丽。这不仅仅是一种完成马拉松般的成就感，而是在长时间思考复杂、困难的问题后，一切突然豁然开朗的那种美妙感觉。”

这种驱动力促使数学家通过观察数字、形状或逻辑结构中的联系、模式或属性，提出猜想（未证明的推测）。随后，通过创造性的逻辑推理和数学工具来证明或反驳这些猜想，最后由其他数学家进行验证。这一过程充满了“思考时间”，正如佛蒙特大学即将获得博士学位的数学家兼计算机科学家 Krystal Maughan 所述，在纯数学夏令营中，学生们常需静坐半小时面对难题，独自沉思，然后再协作梳理问题。这是数学古老的乐趣所在，但如今 AI 开始试图绕过这一缓慢的 deliberative（深思熟虑）过程。

AI 在数学中的角色演变

尽管计算技术在过去 50 年中加速了数学进步（例如 50 年前计算机通过检查 1,936 个案例证明了四色定理），但人类数学家在提出猜想、制定策略和验证证明方面始终占据核心地位。然而，AI 正在改变这一现状：

1. 从“随机鹦鹉”到高级推理机器：LLMs 已从仅能复述互联网上基础数学内容的工具，进化为具备高级数学推理能力的系统。
2. 奥林匹克竞赛级别的成就：去年夏天，Google DeepMind 和 OpenAI 的系统在国际数学奥林匹克竞赛（IMO）中达到金牌水平，相当于世界上最富数学天赋的高中生水平。
3. 博士级研究成果的自主生成：今年早些时候，Google DeepMind 的实验性 AI 系统 Aletheia 自主生成了可发表的博士级研究成果。虽然其计算的算术几何结构常数在数学上较为晦涩，但其解决未解数学问题所展现的复杂推理能力具有重要意义。
4. 推翻重要猜想：OpenAI 最新推出的通用 AI 系统推翻了组合几何学中的一个重要猜想。这一成果若由人类完成，足以发表在顶级数学期刊上，被顶尖数学家誉为 AI 在数学领域独立、原创且 sophisticated（精密/复杂）思维的里程碑。

形式化证明与 LLMs 的结合

另一个重大转变是将 LLMs 与证明助手（Proof Assistants）相结合。Isabelle、Lean 和 Rocq 等系统已存在十余年，它们是专门的编程语言，用于逐步检查数学证明的逻辑正确性。传统上，数学家必须手工将定理和证明转化为机器可读的格式（即形式化），这是一个繁琐的过程。现在，LLMs 开始消除这一瓶颈，自动化地将非形式化证明翻译为证明助手可以验证的形式代码。

以欧几里得关于素数无限多的著名证明为例，人类证明通常省略步骤并依赖共享的理解；而在 Lean 中的形式化证明则使每一个假设和推理都变得明确，以便计算机验证。AI 公司 Math, Inc. 使用的推理代理 Gauss 在 2022 年帮助瑞士洛桑联邦理工学院（EPFL）的玛丽娜·维亚佐夫斯卡（Maryna Viazovska，2022 年菲尔兹奖得主）完成了其解决 8 维球体堆积问题证明的形式化工作，仅用数天便完成了原本耗时的工作，并随后自主完成了形式化。

关键要点

• 数学研究的本质转变：传统数学研究依赖于人类漫长的思考、直觉和创造性推理，其核心价值在于“理解”带来的美学体验和智力满足。AI 的介入使得这一缓慢过程变得可能不再必要。
• AI 能力的快速跃升：
  • LLMs 已具备解决国际数学奥林匹克竞赛级别问题的能力。
  • AI 系统（如 Aletheia）已能自主生成具有博士研究水平的数学成果。
  • AI 已能独立推翻重要的数学猜想，展现出独立且原创的思维。
• 形式化验证的自动化：LLMs 正在解决数学形式化过程中的瓶颈，自动将人类直觉性的证明转化为机器可验证的形式代码，极大地提高了证明验证的效率和准确性。
• 人类角色的重新定位：虽然计算和 AI 在证明和验证中的作用增强，但人类在提出猜想、引导直觉和赋予数学意义方面的角色依然关键。然而，AI 是否会让数学家完全边缘化，仍是学界争论的焦点。

意义与影响

AI 在数学领域的突破不仅是一个技术里程碑，更引发了关于学科本质的哲学反思。

首先，它挑战了“数学家”的定义。如果 AI 能够自主发现模式、提出猜想甚至完成证明，那么数学家的工作重心将从“计算”和“推导”转向“引导”和“诠释”。数学家可能需要更多地关注如何选择值得解决的问题，以及如何解释 AI 生成的复杂证明背后的数学直觉。

其次，它加速了数学知识的积累和验证。形式化证明的自动化使得数学真理的验证更加严谨和高效，减少了人为错误的可能性，并可能揭示出人类难以察觉的逻辑联系。

最后，这一趋势迫使学术界重新审视数学教育的目标。未来的数学教育可能不再仅仅强调解题技巧，而应更注重培养批判性思维、对 AI 生成结果的评估能力，以及对数学美学和深层结构的理解。AI 并未消除数学的魅力，而是将其提升到了一个新的维度，让人类数学家能够从繁琐的推导中解放出来，更专注于探索数学的深层结构和意义。