Daily Tech Briefing
AI 科技速览
每天 5 分钟内学习 AI。获取最新的人工智能新闻，理解其重要性，并学习如何将其应用于您的工作。
量子位 · 2026/8/4 09:22:46
数学家24小时驳回OpenAI攻破的猜想！“AI证对了每句话，但已跟原猜想无关”
AI 中文解读
OpenAI刚宣称AI模型推翻了一个世界级数学猜想，第二天就被人类数学家打脸了。这位数学家花了24小时把AI的37000行证明代码从头追到尾，发现AI每一步推理都对，但证明的根本不是原猜想——就像AI答了一道超难的题，可惜题目被它自己悄悄换掉了。通俗地说，数学猜想就像一道“证明某类物体都满足某条件”的题，AI构造了两个特殊物体想当反例，结果其中一个压根不属于题目要求的范围，等于答非所问。这事最值得关注的，是它暴露了AI科研的一个致命盲区：机器只验证证明过程是否形式正确，却不负责证明的题目是否对路。对普通人来说，这提醒我们AI工具再强大，在数学、法律、医学等严肃领域也不能直接盲信结论，关键时刻还得靠人类专家把关。目前这个数学猜想依然悬而未决，但这件事本身已经成了AI科研审查必要性的经典案例。
首页
资讯
智能车
智库
活动
MEET大会
AIGC
扫码关注量子位
// $('.biaojiwei').click(function(){
$('.biaojiwei').click(function(event){
event.stopPropagation();
$('#pophead').show();
})
$('.weixin_pop').click(function(){
$('.weixin_pop').hide();
})
// })
< img id="wx_img" src="https://www.qbitai.com/wp-content/uploads/imgs/qbitai-logo-1.png" width="400" height="400">
数学家24小时驳回OpenAI攻破的猜想！“AI证对了每句话，但已跟原猜想无关”
梦晨
2026-08-04
17:22:46
来源：量子位
第二天，就有一篇人类论文回应：AI提出的反例不成立
梦晨 发自 凹非寺量子位 | 公众号 QbitAI
OpenAI宣称下一代AI模型解决了10个世界级难题，其中包括推翻了Connes刚性猜想。
第二天，就有一篇人类论文回应：AI提出的反例不成立。
作者是堪萨斯大学拓扑物理中心的J. L. Nielsen，她把OpenAI公开的37000行Lean 4代码从头追到尾，把每一个对象对回它的数学原型，最后给出两条互相独立的失败路径。
具体的证明过程咱一般人也看不太懂，让AI和数学家神仙打架去吧。
但通过这件事，说明人类对AI科研结果的审查仍然很关键。
什么是Connes刚性猜想
Connes刚性猜想说的是这样一件事。
数学上可以给一个群配一套代数结构。有时候两个长得不一样的群，配出来的结构却完全一样。
Connes在1980年左右提出猜测：只要这个群满足两个附加条件，这种情况就不会发生，结构一样，群就必须一样。
这两个附加条件，一个叫ICC，一个叫Kazhdan性质(T)。
换句话说，想反驳这个猜想，需要举出满足两个条件，但构造不一样的群。
OpenAI新模型的做法是构造两个不同构的群，让它们生成同样的代数，并给出两个群都满足ICC和性质(T)的证明。
整套论证写成37000行Lean 4代码，由Lean内核逐条验证通过，另外附了一份说明文档，解释这两个群是怎么搭出来的。
Nielsen指出：AI构造的其中一个群，其实没有满足附加条件，既不是ICC，也没有性质(T)。
这其中有三种可能：
代码里性质(T)没有忠实对应Kazhdan的原始定义；或者证明只对部分成立，却被算到了整个群上；又或者代码里那个群根本不是说明文档里描述的样子。
37000行，逐行对号
为了验证这个结论，Nielsen还做了一件更费力的事。
公开发布的代码是一个整合成单文件的版本，早期分模块源码里的那些名字全都不见了。
她于是列了一张对照表，把每个数学对象在新代码里的名字和行号一一标出：
零上闭链群在第13700行，扭曲群在第14069行，两套代数同构的证明在第36712行，主定理在第36954行。
她还把代码证明ICC的整条推理链追了一遍。这条链从第31430行起步，一层层往上传递，最后在第31610行合成结论。
Nielsen指出的问题是，这些引理处理的是经过对偶变换之后的对象，不是原来那个带中心元素的群，因此并没有直接覆盖到关键的那部分元素。
至于它们是否对最终进入定理的那个具体的群里每一个元素都成立，取决于两块构造之间的接口怎么对接。
这说明“要证什么”就出了问题，不是“证得对不对”的问题。Lean只负责验证后者。
对于另一个扭曲的群，Nielsen的态度是保守的。她说自己没有从代码里独立核实它到底满不满足ICC，也承认代码里的引理有可能确实证明了它满足，但那不改变结论，已经有一z个群不满足。
她把自己的两条反驳也写成了Lean代码，在Lean 4.32.2下编译。
机器检查的是形式，不是意思
论文最后一节把这件事放进了一个更大的背景。
Lean内核能保证的事情，只是一段证明在形式上严丝合缝，但不负责是否真的能证明原结论。
这里可以直接引用陶哲轩的说法：验证证明的是形式陈述本身，而不是这个陈述和意图相符，所以人类的审查不能直接被取代。
过去这类事故已经有记录。
一份针对五个常用Lean基准的审计给出了4833条发现，包括反例、空洞定理和不可靠公理，全都通过了机器验证。最后是人类构造出反例，才发现被证明的那句话本身是错的。
在统计学习理论的形式化工作中，最危险情形被描述为“不是一个失败的证明，而是一个对错误陈述的成功证明”。
张量网络方面的研究也记录过同类现象：系统给出的证明形式上完全正确，只是它证的那个命题比预期的要弱。
Nielsen写道，OpenAI那份形式化可能把它声称的每一条结论都建立对了。但它没有建立、Lean内核也检查不了的，是这些结论和猜想的原话有没有关系。
人读猜想会看到前提，证明助手拿到一个不满足前提的结论，会照样验证关于它的任何断言。
Connes刚性猜想仍然开放。
论文地址：https://philarchive.org/archive/NIEWTCv17
参考链接：[1]
https://openai.com/index/ten-advances-in-mathematics/[2]
https://github.com/openai/ten-proofs/blob/main/ConnesRigidity.lean
版权所有，未经授权不得以任何形式转载及使用，违者必究。
数学
梦晨
年薪百万抢电工，Meta急到自己办技校2026-08-03
AI不再用完即忘：华为诺亚开源MindMemOS，记忆和Skill一起进化2026-08-03
亚太唯一！阿里云跻身Gartner可观测魔力象限“挑战者”象限2026-07-24
业内首款超算+智算的大规模计算底座，在WAIC上我们找到了2026-07-22
扫码分享至朋友圈
// 设置参数方式
var qrcode = new QRCode('qrcode', {
text: 'https://www.qbitai.com/2026/08/465792.html',
width: 256,
height: 256,
colorDark : '#000000',
colorLight : '#ffffff',
分享
阅读原文 ↗