数学家24小时驳回OpenAI攻破的猜想！“AI证对了每句话，但已跟原猜想无关”
内容提要
OpenAI声称其新模型解决了Connes刚性猜想，但数学家Nielsen审查其37000行Lean 4代码后，指出AI构造的群不满足前提条件，证明无效。她列出两条失败路径，并强调机器验证仅保证形式正确，不保证与原始猜想相符，人类审查仍不可或缺。
延伸解读
机器验证的局限
Lean内核只能保证证明在形式上是正确的，即每一步推理都符合逻辑规则，但它无法判断这个形式陈述是否与原始猜想相符。Nielsen指出，OpenAI的代码可能证明了某个关于群的结论，但那个群并不满足猜想的前提条件，因此证明无效。这提醒我们，机器验证不能替代人类对数学意义的理解。
形式化证明的陷阱
在形式化数学中，一个常见的陷阱是“对错误陈述的成功证明”：系统证明了一个命题，但该命题比预期的弱或与原始问题无关。Nielsen发现，OpenAI的证明中，某些引理处理的是对偶变换后的对象，而非原始群，导致结论没有覆盖关键部分。这警示研究者，在依赖自动化证明时，必须仔细核对每个步骤是否忠实于原始定义。
人类审查的必要性
Nielsen的审查过程展示了人类数学家的重要性：她不仅检查了代码的逻辑，还追溯了每个数学对象的原型，并发现了AI忽略的前提条件。过去已有多个案例表明，机器验证通过的结果可能包含反例或空洞定理。因此，即使AI能生成大规模证明，人类仍需负责解释和验证其数学意义，确保结论与猜想一致。
Q&A
OpenAI声称解决了Connes刚性猜想，但数学家Nielsen为什么说这个证明无效？
Nielsen审查了OpenAI公开的37000行Lean 4代码，指出AI构造的其中一个群不满足Connes刚性猜想的前提条件（ICC和Kazhdan性质(T)），因此证明无效。
Connes刚性猜想是什么？
Connes刚性猜想由数学家Connes在1980年左右提出，大意是：如果一个群满足ICC和Kazhdan性质(T)两个附加条件，那么当两个群配出的代数结构完全一样时，这两个群本身也必须一样。
OpenAI的新模型是如何尝试反驳Connes刚性猜想的？
OpenAI的新模型构造了两个不同构的群，让它们生成同样的代数，并给出了两个群都满足ICC和性质(T)的证明，整套论证写成37000行Lean 4代码，由Lean内核验证通过。
Nielsen指出了哪些可能的失败路径？
Nielsen指出AI构造的其中一个群不满足附加条件，既不是ICC也没有性质(T)。她列出了三种可能：代码中性质(T)没有忠实对应Kazhdan的原始定义；证明只对部分成立却被算到整个群上；或者代码中的群根本不是说明文档里描述的样子。
Lean 4代码验证能保证什么？不能保证什么？
Lean 4代码验证能保证证明在形式上严丝合缝，但不负责证明是否真的能证明原结论。也就是说，它只验证形式陈述本身，不验证陈述与意图是否相符。
Nielsen如何验证她的反驳？
Nielsen把OpenAI的代码从头追到尾，列出对照表标出每个数学对象在代码中的位置，并追查了证明ICC的整条推理链，发现引理处理的是对偶变换后的对象，没有覆盖关键元素。她还把自己的两条反驳写成了Lean代码，在Lean 4.32.2下编译。
Connes刚性猜想目前的状态是什么？
Connes刚性猜想仍然开放，没有被解决。
