「陶哲轩说数学界该学会『消化』AI 了」：森多夫猜想 9 万行 Lean 压成 1.5 万行，Palomar 登记库上线

当 OpenAI Astra 用 Lean 4 一口气证出 10 道开放数学题、Axiom Math 把 246 素数间隙定理形式化验证，数学界欢呼「AI 会原创研究了」的同时，菲尔兹奖得主陶哲轩（Terence Tao）在 ICM 演讲与博客里泼了一盆冷静的水：AI 能生成证明，但数学成果要「可用」，还差一道被长期忽视的工序——消化（digestion）。

从森多夫猜想看「消化」是什么 森多夫（Sendov）猜想研究多项式零点与临界点的距离，低次数与充分大次数已解决，中间范围长期空悬。几天前，数学爱好者 Lech Mazur 用 AI 填补了缺口，给出通过 Lean 验证的形式化证明。故事本该到此结束——证明机器可验证，对吧？

陶哲轩注意到：这份原始证明还没有被整理成适合人类阅读和发表的数学文本，成果「还不可用」。于是他花数天，在 ChatGPT 与纸笔推导共同辅助下，做了一次完整消化：追溯文献来源 → 提炼真正起作用的恒等式 → 删掉绕路 → 把机器发现的论证改写成能看出主线的版本。

这一读，读出了新东西：整理后的论证不仅解决 Sendov 猜想，还能覆盖更强的 Phelps–Rodriguez 猜想；核心工具比原始形式化呈现的更初等；Lean 代码从约 9 万行压缩到 1.5 万行。换言之，消化既是对 AI 证明的再验证，也是拓宽成果的有效途径。

陶哲轩的成果生命周期五阶段 生成论证 → 核验正确 → 讲给同行 → 发表检验 → 沉淀为标准知识。AI 擅长加速前两步，后三步（阐释、发表、沉淀）仍需数学家深度参与。他主张学界别再只追捧「第一个给出证明的人」，应提高「消化整理证明」的地位——解释证明、审稿、把成果整理成经典理论，同样算功劳。

Palomar：把「消化」制度化 陶哲轩同期公开了面向 Lean 验证结果的登记库 Palomar（由 Lean FRO 与 ICARM 孵化，8 月 18 日开放提交）。它登记题目陈述、证明代码、AI 参与方式与版本信息，经独立内核复核，把散落在 GitHub、社媒、新闻里的 AI 证明集合到一处，作为「验证与发表之间的消化中继站」。

机制设计要点：

• 提交仓库快照（按 commit 锁定），含 challenge 文件（Lean 声明）、solution 模块、formalization.yaml（非形式描述+元数据+披露）。
• 两道检查：机械的（Lean Comparator 校验 solution 是否证了 challenge 所宣称的）、非确定性的（LLM 检查非形式描述是否匹配）。陶哲轩强调这远非人类同行评审，Palomar 不是同行评审期刊。
• 覆盖三种失败模式：证明根本不 typecheck；typecheck 但用了 sorry 占位/额外公理等作弊；typecheck 但形式化陈述与非形式宣称微妙不符。
• 成果归属权由四个时间节点先后共同决定：生成成果（如 AI 聊天记录）、验证成果（如 Lean 代码）、阐释成果（如公开演讲）、发表成果（如论文）——谁先交齐整套，谁获优先权。
• 陶哲轩已把自己的 Sendov 形式化作为首批档案提交并通过验证。

为什么值得关注 今日数学×AI 叙事多聚焦「AI 生成新定理」（Astra/Axiom），这条线补足了同样关键的「AI 证明如何被人类吸收成知识」的下游环节。当 AI 以小时/天为单位批量产出 Lean 证明，旧有的「有机信任」（数月专家细读、作者知名）机制被打破，Palomar 是用自动化审计轨迹去替代它的尝试。它不关心 provenance（人生成/AI 生成/混合），只认正确性——这恰是压力本身催生了登记库需求。

一句话：AI 会写证明，但数学界得学会把证明「读成数学」。

来源：澎湃新闻/量子位（陶哲轩隔空对话王虹）、ai-beat.github.io（Palomar 机制拆解）、pivotnews.ai（Tao 公告原文要点）、arxiv 2608.16753（森多夫形式化）、陶哲轩博客 terrytao.wordpress.com。