AI证对却无关原意？数学家24小时驳回OpenAI数学猜想
在人工智能迅速渗透基础科学研究的当下，一场关于“机器是否真正理解数学”的激烈辩论正在学术界悄然展开。近期，OpenAI发布了一项引人注目的成果，宣称其下一代AI模型成功解决了包括推翻Connes刚性猜想在内的十个世界级数学难题。这一消息瞬间引发了全球数学界的震动，毕竟Connes刚性猜想自1980年提出以来，一直是算子代数与群论交叉领域的一座高峰。然而，戏剧性的一幕在第二天上演：堪萨斯大学拓扑物理中心的数学家J. L. Nielsen发表了一篇简短而有力的论文，明确指出AI提出的反例并不成立。这并非简单的意见分歧，而是一次基于代码底层逻辑的精准狙击。
Nielsen的工作并非停留在口头质疑，而是深入到了OpenAI公开的37000行Lean 4代码深处。她将代码中的每一个抽象对象逐一映射回其对应的数学原型，最终构建了两条相互独立的失败路径，证明了AI所构造的反例在数学定义上存在根本性缺陷。这一事件不仅是对单一猜想真伪的澄清，更是对当前AI辅助数学证明范式的一次深刻拷问。它揭示了一个被技术光环掩盖的事实：形式验证系统的完美运行，并不等同于数学真理的发现。
要理解这次争议的核心，首先必须厘清Connes刚性猜想的本质。在数学结构中，群与代数之间存在着深刻的联系。通常情况下，两个不同构的群可能会生成同构的冯·诺依曼代数结构。Connes在1980年左右提出的猜想认为，如果限制在满足特定条件的群上，这种“多对一”的现象将不再发生。具体而言，这两个关键条件是ICC（无限共轭类）性质和Kazhdan性质(T)。简而言之，猜想断言：若两个群均满足ICC和性质(T)，且它们生成的代数结构相同，则这两个群必然同构。因此，要推翻这一猜想，必须构造出两个不同构的群，它们同时满足上述两个条件，却生成相同的代数结构。
OpenAI的AI模型正是沿着这一思路进行的尝试。它声称构造了两个不同构的群，并提供了详细的Lean 4代码证明这两个群均满足ICC和性质(T)，且生成的代数同构。整套论证过程被封装在37000行代码中，并由Lean内核逐条验证通过。从形式逻辑的角度看，这是一份无懈可击的证明文档。然而，Nielsen指出，问题的症结不在于逻辑推导的错误，而在于前提条件的缺失。她发现，AI构造的其中一个群，实际上既不具备ICC性质，也不具备Kazhdan性质(T)。
这一发现指向了三种可能的技术失误：一是代码中对性质(T)的定义未能忠实反映Kazhdan的原始数学定义；二是证明过程仅对群的某一部分成立，却被错误地推广到了整个群；三是代码中实际操作的群对象与说明文档中描述的群对象存在偏差。无论哪种情况，都意味着AI虽然完成了一次完美的形式化演绎，但其出发点已经偏离了原猜想的约束范围。
为了验证这一结论，Nielsen进行了一项极为繁琐且需要深厚数学功底的工作。由于OpenAI发布的代码是一个整合后的单文件版本，早期开发过程中使用的模块化命名和注释大多已丢失，这给逆向工程带来了巨大困难。Nielsen不得不手动建立一张详细的对照表，将代码中的每一行与具体的数学对象对应起来。例如，她标识出零上闭链群位于第13700行，扭曲群位于第14069行，而两套代数同构的关键证明则出现在第36712行，主定理陈述在第36954行。
更为关键的是，Nielsen追踪了代码中证明ICC性质的完整推理链。这条链条从第31430行开始，经过层层引理传递，最终在第31610行合成结论。她敏锐地发现，这些引理所处理的对象是经过对偶变换后的变体，而非原始猜想中带有中心元素的那个群。因此，这些证明并没有直接覆盖到关键的核心元素。至于这些性质是否适用于最终进入定理的那个具体群，完全取决于两块构造模块之间的接口对接方式。这表明，问题出在“要证明什么”的定义阶段，而非“如何证明”的执行阶段。Lean系统只负责验证后者，即给定前提下的逻辑有效性，而无法判断前提本身是否符合原始数学意图。
对于另一个被AI声称满足条件的扭曲群，Nielsen采取了更为保守的态度。她承认自己未能在代码中独立核实该群是否满足ICC，也认可代码中的引理可能在形式上证明了这一点。但这并不影响最终结论，因为只要有一个群不满足前提条件，整个反例就不攻自破。为了增强说服力，Nielsen将自己的反驳过程也编写成了Lean代码，并在Lean 4.32.2环境下成功编译。这意味着，她的反驳同样通过了机器验证，形成了“用魔法打败魔法”的局面。
这一事件将我们带入了一个更深层的哲学与技术讨论：机器检查的是形式，而非意义。Lean内核能够保证的，仅仅是一段证明在形式逻辑上的严丝合缝，它无法理解数学符号背后的语义内涵。正如著名数学家陶哲轩所言，验证证明的是形式陈述本身，而不是这个陈述与研究者的初始意图相符。因此，人类的审查环节在AI时代不仅没有被取代，反而变得愈发关键。
历史上，类似的事故已有先例。一份针对五个常用Lean基准测试的审计研究曾发现4833个问题，包括反例、空洞定理和不可靠公理，这些内容全都通过了机器验证。最终，是人类数学家构造出反例，才揭示出被“证明”的命题本身是错误的。在统计学习理论的形式化工作中，这种现象被描述为“不是一个失败的证明，而是一个对错误陈述的成功证明”。在张量网络研究中，也曾记录过系统给出的证明形式完全正确，但其证明的命题比预期要弱得多的情况。
Nielsen在论文最后强调，OpenAI的形式化工作可能确实将其声称的每一条结论都建立对了，但它没有建立、且Lean内核也无法检查的，是这些结论与Connes刚性猜想原话之间的关联。人类阅读猜想时，会自然地将前提条件纳入考量；而证明助手拿到一个不满足前提的结论时，会照样验证关于它的任何断言，只要逻辑自洽即可。这种“语义鸿沟”是当前AI辅助证明系统面临的最大挑战。
从更广泛的视角来看，这一事件反映了AI在科研中的应用正处于一个微妙的转折点。AI擅长处理海量的符号操作和逻辑推导，能够在极短时间内生成复杂的证明结构。然而，它缺乏对数学概念本质的直观理解，容易陷入局部最优解或定义偏差的陷阱。在这种情况下，人类数学家的角色从单纯的“证明者”转变为“架构师”和“审查者”。我们需要设计更严谨的形式化框架，确保AI的操作空间被严格限制在正确的语义范围内；同时，我们需要保持对AI输出结果的高度警惕，通过深入的代码审计和数学直觉检验，防止形式正确但实质错误的结论误导研究方向。
此外，这也提示了形式化验证工具本身的局限性。目前的证明助手如Lean、Coq等，主要关注逻辑的一致性，而对于数学对象的语义一致性缺乏内置的检查机制。未来的发展方向可能包括开发能够自动检测语义偏差的工具，或者引入自然语言处理技术，让AI能够更好地理解数学文本中的隐含前提和上下文约束。只有当AI不仅能“算对”，还能“懂意”时，它才能真正成为数学研究的得力伙伴。
目前，Connes刚性猜想仍然处于开放状态，未被推翻。Nielsen的驳斥不仅维护了数学的严谨性，也为AI在基础科学中的应用划定了清晰的边界。这场24小时内的快速回应，展示了人类智慧在面对机器智能时的韧性与敏锐。它提醒我们，无论技术如何进步，数学的核心依然在于人对真理的追求和理解，而不仅仅是符号的游戏。在未来的科研范式中，人机协作将更加紧密，但人类的主导地位和审查责任将始终不可或缺。我们需要建立的，不是对AI的盲目信任，而是一种基于深刻理解的批判性合作模式。