AI批量生产数学证明引发信任危机：Lean被曝健全性漏洞，陶哲轩转向警惕

美国当地时间10月9日，菲尔兹奖得主、加州大学洛杉矶分校教授陶哲轩在其博客转发了数学家托马斯·黑尔斯的专栏文章《数学家应该了解的Lean定理证明器：可靠性与人工智能问题》。文章抛出的核心问题是：当AI开始以前所未有的速度批量生产数学证明，人类凭什么确信这些证明是可靠的？

解题不再是稀缺品。黑尔斯在文中回顾，开普勒猜想的形式化曾耗费约20个人工年、产出约50万行证明脚本；而过去一年，AI自动形式化接连突破——今年3月Math Inc.宣布完成24维球体堆积的自动形式化，生成约50万行代码；5月Meta研究团队以ATLAS项目形式化了26本数学教材的大部分内容；9月4日Anthropic宣布完成费马大定理的形式化，11天生成约1300万行Lean代码。OpenAI则于10月6日在GitHub一次性放出722篇由内部模型生成的数学手稿，涵盖372个结果系列与约4000个测试问题。

速度的另一面是可靠性裂缝。黑尔斯指出，2026年夏季Lean接连曝出多个健全性漏洞，被圈内称为“健全性漏洞之夏”。其中最受关注的一次发生在7月：有人在AI协助下发布了一份声称“证伪考拉兹猜想”的Lean形式化证明，该证明被Lean内核与独立检查器同时接受，几天后人们才发现，它利用了内核在处理嵌套归纳类型时的实现缺陷，让系统错误接受了矛盾命题。把证明交给计算机，并不等于万无一失。OpenAI那批手稿在公布一天后也被撤回了3篇，其形式化代码与自然语言推导之间经常出现假设和步骤脱节。

陶哲轩的态度因此从力挺AI数学转向警惕。他在Mathstodon上提出“Math 1.0”与“Math 2.0”之分：传统数学看重“谁先解决某个公开问题”，而当解题被AI批量完成，数学界需要转向重视解释说明、社区建设与开辟新的研究方向。据腾讯科技报道，一份联署25位菲尔兹奖得主的宣言《人工智能在数学中的严重错位》已经发出，陶哲轩牵头的“人类数学协会”还发表声明呼吁停止与OpenAI合作。黑尔斯则提出了一个更尖锐的问题：既然AI已参与过对Lean内核的漏洞扫描与修复，人们又如何证明它没有在这个过程中留下隐秘缺陷甚至后门？

颇具意味的是，同样在近日，谷歌DeepMind数学AI攻克厄多斯难题的成果选择走同行评审、登上《科学》杂志，与OpenAI直接公开手稿的做法形成鲜明对比。受访研究者普遍认为AI浪潮无法阻挡，SevenX管理合伙人冯瑶也在访谈手记中写道：“更强的模型，不会自动变成更好的交付。”共识在于：数学不仅需要更快地产出结果，还必须有人能解释、理解并为这些结果负责——人类在享受速度的同时，仍要保有独立判断证明是否可信的能力。