OpenAI宣称下一代AI模型解决了10个世界级难题，其中包括推翻了Connes刚性猜想。
第二天，就有一篇人类论文回应：AI提出的反例不成立。
作者是堪萨斯大学拓扑物理中心的J. L. Nielsen，他把OpenAI公开的37000行Lean 4代码从头追到尾，把每一个对象对回它的数学原型，最后给出两条互相独立的失败路径。
具体的证明过程咱一般人也看不太懂，让AI和数学家神仙打架去吧。
但通过这件事，说明人类对AI科研结果的审查仍然很关键。
什么是Connes刚性猜想
Connes刚性猜想说的是这样一件事。
数学上可以给一个群配一套代数结构。有时候两个长得不一样的群，配出来的结构却完全一样。
Connes在1980年左右提出猜测：只要这个群满足两个附加条件，这种情况就不会发生，结构一样，群就必须一样。
这两个附加条件，一个叫ICC，一个叫Kazhdan性质(T)。
换句话说，想反驳这个猜想，需要举出满足两个条件，但构造不一样的群。
OpenAI新模型的做法是构造两个不同构的群，让它们生成同样的代数，并给出两个群都满足ICC和性质(T)的证明。
整套论证写成37000行Lean 4代码，由Lean内核逐条验证通过，另外附了一份说明文档，解释这两个群是怎么搭出来的。
Nielsen指出：AI构造的其中一个群，其实没有满足附加条件，既不是ICC，也没有性质(T)。
这其中有三种可能：
代码里性质(T)没有忠实对应Kazhdan的原始定义；或者证明只对部分成立，却被算到了整个群上；又或者代码里那个群根本不是说明文档里描述的样子。
37000行，逐行对号
为了验证这个结论，Nielsen还做了一件更费力的事。
公开发布的代码是一个整合成单文件的版本，早期分模块源码里的那些名字全都不见了。
他于是列了一张对照表，把每个数学对象在新代码里的名字和行号一一标出：
零上闭链群在第13700行，扭曲群在第14069行，两套代数同构的证明在第36712行，主定理在第36954行。
他还把代码证明ICC的整条推理链追了一遍。这条链从第31430行起步，一层层往上传递，最后在第31610行合成结论。
Nielsen指出的问题是，这些引理处理的是经过对偶变换之后的对象，不是原来那个带中心元素的群，因此并没有直接覆盖到关键的那部分元素。
至于它们是否对最终进入定理的那个具体的群里每一个元素都成立，取决于两块构造之间的接口怎么对接。
这说明“要证什么”就出了问题，不是“证得对不对”的问题。Lean只负责验证后者。
对于另一个扭曲的群，Nielsen的态度是保守的。他说自己没有从代码里独立核实它到底满不满足ICC，也承认代码里的引理有可能确实证明了它满足，但那不改变结论，已经有一个条件不满足。
他把自己的两条反驳也写成了Lean代码，在Lean 4.32.2下编译。
机器检查的是形式，不是意思
论文最后一节把这件事放进了一个更大的背景。
Lean内核能保证的事情，只是一段证明在形式上严丝合缝，但不负责是否真的能证明原结论。
这里可以直接引用陶哲轩的说法：验证证明的是形式陈述本身，而不是这个陈述和意图相符，所以人类的审查不能直接被取代。
过去这类事故已经有记录。
一份针对五个常用Lean基准的审计给出了4833条发现，包括反例、空洞定理和不可靠公理，全都通过了机器验证。最后是人类构造出反例，才发现被证明的那句话本身是错的。
在统计学习理论的形式化工作中，最危险情形被描述为“不是一个失败的证明，而是一个对错误陈述的成功证明”。
张量网络方面的研究也记录过同类现象：系统给出的证明形式上完全正确，只是它证的那个命题比预期的要弱。
Nielsen写道，OpenAI那份形式化可能把它声称的每一条结论都建立对了。但它没有建立、Lean内核也检查不了的，是这些结论和猜想的原话有没有关系。
人读猜想会看到前提，证明助手拿到一个不满足前提的结论，会照样验证关于它的任何断言。
Connes刚性猜想仍然开放。
论文地址：
https://philarchive.org/archive/NIEWTCv17
参考链接：
[1]https://openai.com/index/ten-advances-in-mathematics/
[2]https://github.com/openai/ten-proofs/blob/main/ConnesRigidity.lean
本文来自微信公众号“量子位”，作者：梦晨，36氪经授权发布。
