问题背景：数学证明是「最难验证的正确性」
大模型写文章错了可以改，写代码错了可以跑测试，唯独数学证明处于一个尴尬位置：一句话的错误就能让整个论证作废，而发现这句话可能需要顶级专家数天。奥数（IMO）恰好把这个难题标准化了——每届 6 道题、每题 7 分、满分 42，人类选手在两个 4.5 小时的时段内作答。它因此成了 AI 推理能力的公共标尺，也成了检验「AI 说的到底对不对」的最佳实验场。
现状：两年三级跳
2024 年 1 月：几何突破。 DeepMind 在 Nature 发表 AlphaGeometry（Trinh et al.）：神经–符号混合架构，语言模型负责建议辅助线（直觉），符号引擎负责演绎推导（严谨），训练数据是自动生成的 1 亿条几何证明，绕开了人类示范数据稀缺的问题。在 2000–2022 年 30 道 IMO 几何题上解出 25 道，接近金牌选手平均的 25.9 道，此前最佳 AI 方法只解出 10 道。
2024 年 7 月：银牌。 AlphaProof 与 AlphaGeometry 2 联手拿下当年 IMO 28/42 分——离金牌线（29 分）只差 1 分。分解开看：AlphaProof 用 AlphaZero 式强化学习在形式化语言 Lean 中做证明搜索，解出两道代数题和一道数论题（包括全场仅 5 人解出的最难的第 6 题）；AlphaGeometry 2 用快了两个数量级的符号引擎在 19 秒内解出几何题；两道组合题未解。评分人是菲尔兹奖得主 Timothy Gowers 与两届 IMO 金牌得主 Joseph Myers——Gowers 的评价是这种非常规构造「远超我对当时技术水平的预期」。两个必须交代的细节：部分题目耗时长达 3 天，远超人类的 4.5 小时；题目是先人工翻译成 Lean 形式化语句再求解的。
2025 年 7 月：金牌。 一周之内两家先后宣布达标：DeepMind 的 Gemini Deep Think 以 35/42 完美解出 5 题且全程在官方时限内，解答由 IMO 官方评委按人类选手标准评分（IMO 主席 Gregor Dolinar 确认）；OpenAI 的实验性推理模型同样拿下 35/42，由三位前 IMO 奖牌得主按官方评分标准以自然语言评分——但它是非官方场景下的闭网测试，比 Google 早一天公布，时机选择当时引发过争议。值得注意的是，这两次金牌都放弃了 Lean：纯自然语言证明在人类评委眼里「看起来对」就够拿奖了。
关键问题：形式化验证为什么是关键
回头看，DeepMind 先走 Lean 这条路并非技术怀旧，而是被一个结构性矛盾逼的：语言模型会幻觉，而数学不接受「看起来对」。 形式化证明的每一步都被证明助手机器校验，错误在语法层就被拒绝——AlphaProof 的闭环之所以能跑通强化学习，前提是奖励信号来自 Lean 的机器判定而不是另一个模型的主观打分。DeepMind 的工程路线也绕着这个矛盾展开：先微调 Gemini 把自然语言题目自动翻译成 Lean 形式化语句（autoformalization），再让 RL 循环在「提出候选—Lean 验证—用已验证证明反哺模型」中迭代，赛前数周内证明或证伪了数百万道题。
反过来看，2025 年的金牌路线等于把验证责任重新交回人类评委，这在研究级数学里是不可持续的——IMO 只有小孔径的已知答案，真正的数学前沿既没有评委也没有标准答案。陶哲轩对此的观察流传很广：LLM 在研究前沿「表现得像过度自信的本科生」（Quanta Magazine, 2026 年 6 月报道）——因为训练数据在那里最稀薄。形式化验证恰好在模型最不可靠的地方提供了地面真值。
陶哲轩自己的实践是最有说服力的注脚。他在 2014 年就预言未来论文会写成可被机器检查的形式；2023 年 10 月经 Kevin Buzzard 劝说上手 Lean 4（形式化麦克劳林不等式，原计划一周、实际用了近一个月，难点反而不是数学本身而是翻找 Mathlib 里的引理）；2023 年 11 月牵头把 PFR 猜想（多项式 Freiman–Ruzsa）的证明众包形式化，约三周完成——远快于旧 Polymath 模式的人工互查；2024 年 9 月启动 Equational Theories 项目，用 Python 脚本加自动定理证明器在数天内解决了约 4694 条代数恒等式之间 2200 万条逻辑蕴含中的 99% 以上，甚至捞出了「magma 上同调」这样的新概念。按中科院 2026 年 6 月的综述说法，AI 已「深度融入数学研究核心环节」，而形式化推理被 Meta、斯坦福等机构的研究者列为 AI for Math 的下一个前沿。
案例小结与展望
把两条路线放在一起看，逻辑就清晰了：奥数金牌可以靠人类评分达成，但「AI 数学」要变成「AI 时代的基础数学」，绕不开机器可验证这一关——它既是防幻觉的护栏，也是强化学习能持续运转的奖励来源。截至 2026-10-07，值得跟踪的方向有三个：一是 autoformalization 的规模化（2024 年 AlphaProof 还要人工翻译题目，2025 年的金牌模型已能直接读自然语言）；二是 Lean 生态本身的扩张（Mathlib 与陶哲轩主导的解析数论形式化项目）；三是「实验数学」范式的形成——陶哲轩的判断是数学将像物理学一样长出实验分支，AI 负责把大问题拆成上千个小子问题，人类守住最难的部分。
相关阅读
- RLHF 全景：从人类偏好到 PPO、DPO 与可验证奖励——AlphaProof 的 RL 闭环是「可验证奖励」在科学领域的极端案例
- 丘成桐新论文致谢了 GPT 和 Claude——一线数学家使用 LLM 的另一面
参考资料
- AI solves IMO problems at silver-medal level — Google DeepMind（2024-07-25）
- AlphaGeometry: An Olympiad-level AI system for geometry — Google DeepMind（2024-01）
- Advanced version of Gemini with Deep Think officially achieves gold-medal standard — Google DeepMind（2025-07-21）
- How Terry Tao Became an Evangelist for AI in Math — Quanta Magazine（2026-06-08）
- Formalizing the proof of PFR in Lean4 — Terence Tao's blog（2023-11-18）
- AI 正深度融入数学研究核心环节 — 中国科学院（2026-06）
读者留言
COMMENTS 暂无还没有留言，来说第一句？