「陶哲轩说数学界该学会『消化』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-beat.github.io（Palomar 机制拆解）、pivotnews.ai（Tao 公告原文要点）、arxiv 2608.16753（森多夫形式化）、陶哲轩博客 terrytao.wordpress.com。