两个月三起反例,数学家开始学着当AI的代码审查员

5月20日到7月19日,两个月里,三个盘踞数学界几十年到上百年的猜想先后被人机接力找出反例。最扎眼的不是反例本身,是速度:OpenAI新模型Sol三周内为其中一例生成了约120万行Lean代码,逼近Lean社区维护九年的数学库mathlib(约230万行)体量的一半。

这些进展目前都来自当事人在Zulip、X和个人博客上的自述,还没经过更大范围的学界复核。要看懂这件事,得先把"AI提出反例""AI形式化反例""Lean编译通过"这三件事分开——它们递进,但互不等价。

两个月,三起反例

这里要提醒一句:第三例里"Jacobian猜想"的精确表述,目前公开材料没有给出完整陈述,具体对应哪个版本的定理还待确认,读者不要直接当成已经盖章的百年难题被攻克。

三起里含金量最扎实的是第一起。ChatGPT先给出证明思路,人类专家看过认可;一周后Logical Intelligence把"这个数论定理能推出反例"翻成Lean;又过一个月,OpenAI的Boris Alexeev引导Sol,把整条论证在不依赖额外假设的前提下完整形式化,编译通过。

反例为什么先被AI攻破

反例只需要一个例子成立,不用建一套放之四海皆准的理论。这天然比证明一个正定理容易,AI先攻破反例而不是攻破大猜想,不奇怪。

形式化验证又把"我信不信这个证明"变成了"编译器过不过"。只要形式命题忠实对应原始猜想,编译通过就是硬指标,人不用逐行核对证明细节——群概形反例那1076行代码,Buzzard不到5分钟就核验完语句和证明。

但120万行和230万行不是一回事,不能直接比大小。前者是三周内为单个反例生成的一次性证明代码,后者是九年攒下来、覆盖多个数学分支、能被反复调用的公共基础库。代码量能说明生成速度,说明不了正确性,更说明不了数学难度。

编译通过之后,谁的活儿变了

编译通过不等于猜想被证伪已成学界共识,更不等于AI独立发现了反例。每一步背后都有人在选题、定义命题、审计代码——Akhil把问题丢给AI,DeepMind的Formal Conjectures仓库提前把猜想的Lean语句定好,这才让后面的验证"看起来平凡"。

风险也是真实的:Lean是一门能执行任意命令的编程语言,AI生成的代码可能夹带恶意指令,Buzzard自己是先在本地沙箱跑过一遍才敢编译。Erdős反例依赖的类域论证明有100多页,至今没人压缩过,也没人把它全部形式化——链条最上游,仍是一段被默认为真的人类证明。

对关注AI和数学研究的技术读者,这轮事件说明的不是AI证明能力反超人类,而是反例搜索和形式化验证的成本在断崖式下降。接下来该盯的不是又冒出一个反例,而是有没有权威数学家公开确认某个反例真的站得住,有没有被写进正式论文或综述——目前三起里,只有第一起拿到了同行认可这一步。

对数学研究者和形式化证明从业者,更现实的变化落在工作方式上。写猜想时最好同步给出可形式化的精确陈述,不然AI批量生成的反例根本对不上号;审计AI生成的Lean代码要先过沙箱,不要直接编译进主环境;博士生选题如果撞上"找反例"这类问题,现在得先查一遍是不是已经有模型在扫了,免得白费功夫。

数学家真正稀缺的角色,正从"算得快、证得对"挪到"问得准、审得严、讲得清"。庄子说"吾生也有涯,而知也无涯",这轮反例潮外包出去的只是"无涯"那部分,"有涯"的人还得负责判断这些反例到底说明了什么。

编译通过不是真理抵达,读懂才是。