AI证对却无关原意？数学家24小时驳回OpenAI数学猜想
在人工智能迅速渗透基础科学研究的当下，一场关于“机器是否真正理解数学”的激烈辩论正在学术界悄然展开。近期，OpenAI高调宣布其下一代大语言模型在数学领域取得突破性进展，声称成功解决了包括推翻Connes刚性猜想在内的十个世界级难题。这一消息瞬间引爆了科技圈与数学界，仿佛宣告着硅基智能即将取代碳基大脑成为真理的最终裁决者。然而，戏剧性的一幕在第二天上演：堪萨斯大学拓扑物理中心的数学家J. L. Nielsen发表了一篇简短却极具杀伤力的论文，直指OpenAI提供的反例根本站不住脚。这并非一次简单的纠错，而是一次对AI科研方法论的深刻拷问。
Connes刚性猜想是算子代数与群论交叉领域的一个核心问题，由著名数学家Alain Connes在20世纪80年代初提出。该猜想的核心直觉在于探讨群的结构与其生成的冯·诺依曼代数之间的刚性关系。简而言之，如果两个群在代数结构上表现出完全相同的特征，那么这两个群本身是否必然同构？Connes猜测，只要群满足两个特定的严苛条件——即无限共轭类性质（ICC）和Kazhdan性质（T），这种“形不同而神同”的情况就不会发生。换句话说，若两个群均满足ICC和性质（T），且它们生成的代数同构，则这两个群必须同构。要反驳这一猜想，研究者需要构造出两个不同构的群，它们同时满足上述两个条件，却能生成同构的代数结构。
OpenAI的团队利用其强大的AI模型，生成了一份长达37000行的Lean 4代码。Lean是一种基于依赖类型理论的交互式定理证明助手，以其严格的逻辑验证能力著称。在这份代码中，AI不仅构造了两个看似不同的群，还给出了它们满足ICC和性质（T）的证明，并最终证明了它们生成的代数同构。Lean内核逐条验证了这些代码，确认其在形式逻辑上是无懈可击的。从计算机科学的视角来看，这是一次完美的执行：输入前提，经过严密的逻辑推导，输出结论，整个过程没有产生任何运行时错误或逻辑漏洞。然而，数学的真理性不仅仅依赖于逻辑形式的正确，更依赖于语义内容的准确映射。
J. L. Nielsen的回应之所以具有颠覆性，在于她没有停留在表面结果的质疑，而是深入到了代码的肌理之中。面对一个整合成单文件、丢失了早期模块命名信息的庞大代码库，Nielsen进行了一项近乎考古学般的工作。她建立了一张详细的对照表，将代码中的每一个数学对象与其在标准数学定义中的原型进行一一映射。例如，她指出零上闭链群位于代码的第13700行，扭曲群位于第14069行，而核心的代数同构证明则隐藏在最后的第36712行。这种逐行对号的细致工作，揭示了AI在形式化过程中可能存在的“偷换概念”风险。
Nielsen发现的核心问题在于，AI所构造的其中一个群，实际上并没有满足Connes猜想所要求的附加条件。具体而言，该群既不具备无限共轭类性质（ICC），也不具备Kazhdan性质（T）。这意味着，虽然AI在代码内部自洽地证明了某些属性，但这些属性所依附的数学对象，并不是Connes猜想中所指的那个对象。这就好比一个人声称自己证明了“所有天鹅都是白色的”，但他实际观察的对象却是企鹅。尽管他的观察记录无误，逻辑推导严密，但结论对于原命题毫无意义。
在技术层面，Nielsen指出了三种可能导致这种偏差的原因。首先，代码中对性质（T）的形式化定义可能未能忠实反映Kazhdan的原始数学定义，存在细微的语义偏移。其次，证明过程可能仅对群的某一部分子结构成立，却被错误地推广到了整个群。最后，也是最令人担忧的一种情况，即代码中实际操作的群对象，与说明文档中描述的群对象在构造接口上存在错位。Nielsen特别追踪了证明ICC的推理链，发现引理处理的往往是经过对偶变换后的对象，而非原始带有中心元素的群。这种接口对接的模糊性，使得形式验证通过了，但数学意义却丢失了。
这一事件并非孤例，它折射出形式化验证领域长期存在的一个深层困境：验证的是形式陈述本身，而非陈述与意图的一致性。著名数学家陶哲轩曾明确指出，证明助手如Lean，其核心功能是确保推导过程的逻辑严密性，但它无法判断用户输入的初始命题是否真正表达了研究者的真实意图。如果初始定义存在偏差，或者前提条件被无意中弱化，系统依然会给出一个“正确”的证明。这种现象在统计学习理论的形式化工作中被称为“对错误陈述的成功证明”，其危险性远大于单纯的证明失败，因为它具有极强的迷惑性。
回顾历史，类似的事故已有先例。此前针对五个常用Lean基准的审计研究中，研究人员发现了4833条问题，包括反例、空洞定理和不可靠公理，而这些内容全都通过了机器的自动验证。最终，是人类数学家通过构造具体的反例，才揭穿了这些被机器“证明”为真的谬误。在张量网络等复杂数学结构的研究中，也多次出现系统给出的证明形式完美，但所证命题比预期弱得多的情况。这说明，当前的AI和形式化验证工具，在处理高度抽象和依赖直觉的数学概念时，仍然存在显著的语义鸿沟。
Nielsen在论文中保持了一种审慎而专业的态度。对于OpenAI构造的另一个扭曲群，她承认自己未能从代码中独立核实其是否满足ICC，但也强调，即便那个群满足条件，由于第一个群已经不满足前提，整个反例依然无效。她将自己的反驳过程也编写成了Lean代码，并在Lean 4.32.2环境下成功编译，以展示其论证的严谨性。这种做法不仅是对AI结果的挑战，更是向学界展示了一种人机协作的新范式：人类负责把握数学直觉和语义准确性，机器负责处理繁琐的逻辑细节，两者互为补充，而非替代。
从更宏观的视角来看，这次事件提醒我们，在拥抱AI赋能科研的同时，必须保持清醒的批判性思维。AI擅长在既定规则下进行大规模搜索和优化，但在定义规则、理解语境和把握数学本质方面，人类的洞察力依然不可或缺。Connes刚性猜想目前仍然处于开放状态，并未被推翻。这一结果或许会让那些期待AI一夜之间解决所有数学难题的人感到失望，但对于科学共同体而言，这恰恰是科学精神体现的时刻：真理不因工具的先进而改变，只因证据的坚实而确立。
未来，随着AI模型能力的进一步提升，形式化验证与语义理解的结合将成为关键研究方向。我们需要开发更加智能的工具，能够辅助研究者检查形式化定义与自然语言描述之间的一致性，减少因误解或编码错误导致的“虚假证明”。同时，数学教育也需要适应这一变化，培养既懂数学直觉又懂形式化逻辑的复合型人才。只有在人类智慧与机器算力的深度协同中，我们才能真正突破认知的边界，而不是在形式的迷宫中迷失方向。
这场发生在24小时内的“反转”，不仅是数学界的一次小插曲，更是人工智能发展史上的一个里程碑。它标志着AI从单纯的效率工具，开始进入需要接受严格学术审查的核心知识生产领域。在这个过程中，错误和纠偏将是常态，而正是通过这些不断的试错与验证，我们才能逐步厘清机器智能的边界，找到人与机器在探索真理道路上的最佳协作模式。Connes猜想依旧悬而未决，但我们对AI认知的清晰度，却因此向前迈进了一大步。