共计 1182 个字符，预计需要花费 3 分钟才能阅读完成。
第二天, 就有一篇人类论文回应:AI 提出的反例不成立
OpenAI 关于“解决世界级数学难题”的展示,正在迎来一次关键复核 。 在其声称下一代模型给出 Connes 刚性猜想反例后, 数学家 J. L. Nielsen 对公开的 Lean 4 代码进行追踪, 并指出:AI 构造的反例中至少有一个群可能并不满足猜想所要求的前提。
📌 事件概览: 形式验证通过, 不等于猜想被推翻
OpenAI 此前展示了若干由新模型完成的数学进展,其中包括对 Connes 刚性猜想的反驳。相关证明被写成约 37000 行 Lean 4 代码, 并由 Lean 内核完成形式检查。
但 Nielsen 的回应提醒了一个容易被忽视的问题: 机器验证可以确认“某段形式化推理是否成立”,却不能自动保证这段推理对应的正是数学家原本想证明或反驳的命题。
争议焦点并非每一行代码是否能被 Lean 接受, 而是代码中的对象和命题, 是否准确对应 Connes 刚性猜想本身。
🔍 背景:Connes 刚性猜想要求什么
通俗地说,Connes 刚性猜想讨论的是群与其关联代数结构之间的关系。若两个群满足特定条件, 并且它们生成的结构相同, 那么猜想认为这两个群也应当是同构的。
这里的关键前提包括两个条件:ICC 以及 Kazhdan 性质 (T)。因此, 要真正构成反例, 需要找到两个不同构的群, 同时它们都满足这些条件, 并生成相同的代数结构。
💡 核心信息:Nielsen 指出至少一个关键群不合格
Nielsen 对 OpenAI 公开代码进行了对象级别的回溯,将代码中的定义、引理和最终定理逐项对应到数学原型。她给出的核心判断是:AI 构造中的某个群并未被证明满足必要前提, 甚至可能既不是 ICC, 也不具备性质(T)。
她提出的风险主要集中在三类可能性:
- 定义偏差:代码中的性质 (T) 未必忠实对应 Kazhdan 原始定义。
- 证明范围偏差:部分对象上的结论, 可能被延展到整体群上。
- 对象对应偏差:代码里实际处理的群, 可能并非说明文档描述的那个群。
📊 看点:AI 数学研究的审稿门槛更高了
这次争议的启示并不局限于一个猜想。随着 AI 开始参与形式化数学, 研究成果可能出现一种更隐蔽的风险: 证明本身成功了, 但证明的是一个更弱、不同, 甚至无关的陈述。
- 形式化证明提升了可检查性, 但不自动解决语义对应问题。
- AI 生成的数学成果仍需要专业数学家审读其定义、前提和目标。
- 大规模代码证明可能带来新的审核成本, 尤其是对象命名和模块结构缺失时。
- “机器验证通过”在传播中不应被简化为“数学难题已解决”。
🚀 总结:Connes 刚性猜想仍未被确认攻破
就目前公开争议看,OpenAI 展示的形式化工作可能包含有效推理, 但 Nielsen 的反驳指出, 其反例与 Connes 刚性猜想所需条件之间存在关键断点。因此, 将其视为猜想已被推翻仍为时过早。
