数学家逐行审查OpenAI证明：形式正确但未覆盖原猜想前提
OpenAI的AI证明被数学家发现形式无误却未忠实对应原猜想，提醒我们机器验证不能替代人类对含义的审查。
OpenAI称AI模型解决了包括推翻Connes刚性猜想在内的10个难题。数学家Nielsen审查其37000行Lean 4代码后指出，AI构造的群其实未满足原猜想的前提条件（ICC和性质T），代码中的证明与说明文档可能不一致，或只部分成立。Lean内核只验证形式正确，不保证陈述与意图相符，人类审查仍不可替代。
正文摘录
OpenAI宣称下一代AI模型解决了10个世界级难题，其中包括推翻了 Connes刚性猜想 。 作者是堪萨斯大学拓扑物理中心的 J. L. Nielsen ，她把OpenAI公开的37000行Lean 4代码从头追到尾，把每一个对象对回它的数学原型，最后给出两条互相独立的失败路径。 数学上可以给一个群配一套代数结构。有时候两个长得不一样的群，配出来的结构却完全一样。 Connes在1980年左右提出猜测： 只要这个群满足两个附加条件，这种情况就不会发生，结构一样，群就必须一样。 OpenAI新模型的做法是构造两个不同构的群，让它们生成同样的代数，并给出两个群都满足ICC和性质(T)的证明。 整套论证写成37000行Lean 4代码，由Lean内核逐条验证通过，另外附了一份说明文档，解释这两个群是怎么搭出来的。 Nielsen指出： AI构造的其中一个群，其实没有满足附加条件，既不是ICC，也没有性质(T) 。 代码里性质(T)没有忠实对应Kazhdan的原始定义；或者证明只对部分成立，却被算到了整个群上；又或者代码里那个群根本不是说明文档里描述的样子。 零上闭链群在第13700行，扭曲群在第14069行，两套代数同构的证明在第36712行，主定理在第36954行。 她还把代码证明ICC的整条推理链追了一遍。这条链从第31430行起步，一层层往上传递，最后在第31610行合成结论。 Nielsen指出的问题是，这些引理处理的是经过对偶变换之后的对象，不是原来那个带中心元素的群，因此并没有直接覆盖到关键的那部分元素。 至于它们是否对最终进入定理的那个具体的群里每一个元素都成立，取决于两块构造之间的接口怎么对接。 对于另一个扭曲的群，Nielsen的态度是保守的。