1995 年 Michel Talagrand 在一个问题里写下：「我当时这么大胆地猜，其实一点根据都没有——就是瞎蒙的。说出这种话的时候，自己都觉得这不可能对吧。」
31 年后，加州理工的董明华（Dongming Hua）、安东尼·宋（Antoine Song）和普林斯顿的斯特凡·图多斯（Stefan Tudose）把证明挂在 arXiv:2605.10908 上。Talagrand 的 2000 美元悬赏被转给图多塞团队。
这件看似枯燥的数学结果，其实切中三个完全不同的话题。
第一，换战场是数学里最高效的降维打击。Talagrand 1995 年的凸性猜想是个几何问题：在任意维欧氏空间里，能否通过固定次数的闵可夫斯基和造出凸性。标准打法是构造凸集。但三人组的证明通道是：把命题改写成概率论版本——任何 n 维空间里的 1-次高斯随机向量，都可以拆成三个标准高斯随机向量之和。一旦这个等价命题成立，几何凸性就跟着出来。
第二，AI 在猜想求解里并非无用，但作用是「把问题往前推一步」。宋和华一开始试过 ChatGPT。大模型帮他们解答了一些问题，让他们离解决方案更近一步——但最终是图多塞拿出了「更具一般性、更具理论性」的最终一击。三人组的论文里明确写道：「图多塞的证明更为一般且更具理论性。」AI 提交的版本被人类数学家替换掉了。这件事和 8 月 1 日 OpenAI Astra 拿下 10 道开放数学形成对位：Astra 那边是「AI 主导 + Lean 验证」，塔拉格兰德这边是「人类主导 + AI 协助 + 同行评议」。
第三，赏金兑现的趣味性。Talagrand 一开始觉得没人能解，自己也没打算真付钱。2026 年他把 2000 美元转给图多塞团队时，公开评价接近「被打脸」。这一笔钱不只是数学悬赏的清算，也是对「我自己都觉得不可能对吧」的一次轻量级认错。
数学 × AI 这条主线在 2026 年 8 月被一连串事件重新写：
- 5 月：OpenAI 解出 Erdős 单位距离问题，9 位数学家人工审阅
- 7 月：Axiom Math 完成 246 定理的 Lean 4 形式化验证
- 8 月 1 日：OpenAI Astra 一晚上解 10 道开放数学，总成本 2000 美元，Lean 证书可独立验证
- 8 月 7 日：OpenAI 因「关键级」安全顾虑对 Astra 加以封锁
- 8 月 17 日：Axiom Math 估值 16 亿美元，Ken Ono 任创始数学家
- 8 月 23 日：Talagrand 凸性猜想解决，三人组公告
- AI 主导路径——Astra、AxiomProver 这种，AI 给出完整 Lean 4 证明，机器可独立验证。优势：成本极低、可重复。劣势：开放问题本身要有「可被验证」的结构。
- 人机协作路径——Talagrand 三人组、AI 数学建模（5 月 Erdős）。AI 在中间推一把，但最后一击是人类数学家。优势：能处理不可机械验证的命题。劣势：依赖顶级专家的注意力。
- 形式化回填路径——Axiom 246、定理库重写。已经发表的定理用 Lean 4 重写一遍。优势：成果可重复。劣势：不是新数学发现。
下一根钉子：AI 主导路径与人机协作路径的真正分水岭不在「数学证明本身」，而在「问题是否可形式化规约」。Astra 的 10 道题里，只有非 sofic 群、Connes 反例、Ehrhart 体积、183 多色 Ramsey、Erdős 146/180 这 5 道是真正的「猜想解决」——它们能被完全形式化规约。剩下 5 道是改进已知界，本质上是「找一个更紧的数」，AI 主导路径可以胜任。但下一道真正的开放问题——比如 BSD 猜想、ABC 猜想、Riemann zeta 零点精细结构——它们需要的不是「更紧的数」，而是「全新的概念框架」。这种问题 AI 当前不可独立完成，需要的是人机协作路径中那种「更一般且更具理论性」的最后一击。Talagrand 凸性猜想是这一类问题的优秀样本。
#Talagrand #凸性猜想 #人机协作