数学界没学会"消化"AI。这句话陶哲轩说得最狠。
先把锅丢到地上:Lech Mazur 用 AI 填了 Sendov 猜想(多项式零点与临界点的距离,中间范围长期空悬)的缺口,Lean 验证过了,故事本该结束。
陶哲轩说:"这份原始证明还没被整理成适合人类阅读和发表的数学文本。"
于是他花了几天,和 ChatGPT + 纸笔一起做了"消化":追溯文献 → 提炼真正起作用的恒等式 → 删掉绕路 → 改写成能看出主线的版本。
结果不仅证明了 Sendov 猜想,还顺手覆盖了更强的 Phelps–Rodriguez 猜想。核心工具比原始形式化呈现的更初等。Lean 代码从 9 万行压到 1.5 万行。
我读到这儿停了一下。这不是工程优化,这是"通过整理来发现新东西"。陶哲轩说这就是他要泼的那盆冷水——AI 能写证明,但"谁先宣布谁获优先权"这套旧规则吃不消了。
他提出的成果生命周期五阶段:生成 → 核验 → 讲给同行 → 发表检验 → 沉淀为标准知识。AI 擅长前两步,后三步(阐释、发表、沉淀)得人深度参与。他主张学界不要再捧"第一个给出证明的人",消化整理证明的人也算功劳。
如果论文作者自己都没法做一场内行水平报告把结果讲明白,AI 验证得再正确,这篇成果也不应该发表。
等等,这听起来像新闻稿。让我换个说法——这等于说数学界把"讲明白"这道工序正式升格成"和证明同等重要"的一道工序。我想到费曼本人——他一辈子最烦的就是把对的东西讲给六年级学生听都讲不明白的人。
陶哲轩没停在演讲里。Palomar 8 月 18 日开放提交了,Lean FRO + ICARM 联合孵化,他本人和 Jeremy Avigad、Matthew Ballard、Jaume de Dios、Nestor Guillen、Bryna Kra、Kim Morrison、Ravi Vakil、Akshay Venkatesh 同在科学顾问委员会。
两道检查:Comparator 工具跑纯机械类型校验(代码是不是真的证明了 challenge file 宣称的定理,有没有偷加公理),LLM 跑语义比对(非确定性的,存在误判可能)。
陶哲轩原话:"Palomar 的检查远远不及人工同行评审对新颖性、重要性和准确性的把关——Palomar 不是 peer-reviewed journal。"
但 Palomar 登记库有个反讽背景——2026 年 7 月,形式化验证专家 Ramana Kumar 利用 Lean 内核漏洞(嵌套归纳类型中幽灵参数逃逸类型检查)构造了考拉兹猜想伪反证,通过了 Comparator 机械校验,2.5 天后被揭穿。漏洞由 Kiran Gopinathan 7 月 28 日报告,Lean 团队一小时修复发 4.32.2 版本。
机械验证工具自身可被攻击。所以双层校验不是冗余,是必须。
他的 Sendov 形式化是首批档案提交。challenge 文件硬上限 1000 行/100KB。
下一根钉子:陶哲轩把"消化"升格成与证明同等重要的工序——AI 时代,数学家的价值不在写出第一个证明,而在把证明读成数学。
#AI数学 #形式化验证