数学家们集体签名搞「莱顿宣言」，AI 做数学真不是刷榜那么简单

上周莱顿洛伦兹中心聚了一堆菲尔兹奖得主和大模型负责人，没讨论 SOTA，专门签了份「莱顿宣言」。核心就一句：别把定理证明当榜单刷，数学研究的核心是洞察和验证，不是生成一堆 LaTeX 代码扔给 Coq 过型检。

宣言里几条硬杠杠的共识，我看着挺解气：

• 基准测试污染严重：MiniF2F、Lean Workbook 那些题，训练集里早背烂了，模型「会做」大概率是背答案，真推理能力打个问号。
• 验证链条缺失：现在流程是 LLM 出证书 → 自动化工具查语法 → 人类信了。中间少了最关键的「数学直觉审查」，万一证明思路本质上是错的，工具只查格式查不出逻辑硬伤。
• 开放性被忽视：真数学是问问题、定概念、找反例，哪有那么多现成的「证明目标」等着你去 QED？现在的 Agent 全在解封闭问题，离开放研究差十万八千里。

其实陶哲轩早就说过，AI 目前顶多是个「极其博学的研究助理」，别指望它自动搞出新数学。宣言呼吁建立「人机协作验证标准」，搞清楚哪步靠模型、哪步必须人把关，这才是正经事。

要是下个版本 o1-preview 还在吹「数学能力超越人类」，建议先把 Lean 库里那些被污染的 benchmark 全洗了，再来跑分不迟。