OpenAI 模型破解 80 年悬案：AI 重塑数学研究范式

2026 年 5 月底，一个 OpenAI 模型成功推翻了 Erdős 的单位距离问题——这一组合几何难题已悬而未决 80 年，成为机器辅助数学又一标志性节点。该事件并非孤例：2020 年 Quanta Magazine 报道了用 Lean 训练 AI 参加国际数学奥林匹克竞赛的 IMO 大挑战，此后数年间，机器辅助数学迎来真正的大爆发。

AI 时代数学界的集体回应：《莱顿宣言》

在 OpenAI 模型公布上述成果两周后，《莱顿宣言》（Leiden Declaration）正式发布，并迅速获得超过 2000 位数学家签署。这一文件被形容为数学界的「国情咨文」，系统汇总了数学家群体对 AI 浪潮的现状判断与未来态度。宣言的迅速扩散表明，AI 已不再只是数学家的辅助工具，而是正在重塑数学研究、审稿乃至人才培养的范式。

Lean 与强化学习：AI 数学能力跃升的核心机制

作家 Kevin Hartnett 在 Simons Foundation 与出版人 Thomas Lin 的公开对谈中，解释了数学为何会成为大模型训练生态的核心场景：

「模型能力的快速提升，很大程度上得益于强化学习。而要做好强化学习，你需要一种能给出精确反馈信号的环境。Lean 恰好满足这一点——模型可以在 Lean 中完成数学题、输出证明代码，并即时获得反馈……这是大实验室如此重视数学的根本原因。」

也就是说，Lean 这类交互式定理证明语言为模型提供了稀缺的、可机器验证的奖励信号，使数学成为强化学习的高价值训练场。

人机协作的数学未来

Hartnett 对人机协作持乐观态度，但同时告诫学生：

「你需要真正理解数学——用过去千百年来人类学习数学的方式去理解它、与之搏斗。如果你想成为像陶哲轩（Terence Tao）那样能够『指挥』AI 的人，你必须先具备那种深度的数学理解。」

他强调，AI 不会取代数学家，但会重新定义「数学家」的工作方式：解题的体力活更多交给机器，而提出问题、构建框架、验证价值的判断力将愈发珍贵。

背景：相关活动预告

文中另预告了 2026 年 7 月底在美国费城举行的国际数学家大会（ICM）相关活动，包括 Hartnett 新著《THE PROOF IN THE CODE》的发布与签售，以及陶哲轩即将出版的《SIX MATH ESSENTIALS》的预购信息。这些活动作为事件背景，进一步印证了 AI 与数学交叉领域当前的关注热度。