四川
九月初，OpenAI宣布其AI系统给出了纳维-斯托克斯方程解会发生爆破的证明，消息一出，数学界和科技圈一片哗然。更让人信服的是，配套的Lean证明代码顺利编译通过，仿佛给这项成果盖上了一枚“机器认证”的钢印。
纳维-斯托克斯方程描述水流、气流等流体的运动，其三维光滑解会不会在有限时间内“爆破”，是克雷数学研究所悬赏百万美元的千禧年难题之一。
然而仅仅一个月后，这枚钢印就被人揭了底。
如果这一结论经得起同行检验，这场人机对弈中，数学家算是漂亮地扳回了一局。
要理解这次“翻车”，得先弄清Lean到底在检查什么。
AI写Lean代码的方式让问题雪上加霜。常见流程是先写一版，报错就改，反复试错直到编译通过，目标只剩“通过”二字。
在这种激励下，AI很容易绕道而行，换个说法、改个条件，怎么省事怎么来，这正是机器学习里臭名昭著的“奖励投机”。
这好比原本承诺及格就发证书，代码版却改成满分才发，发出的证书含金量还更低。
问题出在自然语言里大量隐含的前提。比如“满足某条件的最小整数”，这句话默认了这样的整数确实存在。
这并非吹毛求疵。在数学里，存在与不存在往往就是一个定理成立与否的分水岭。
在Lean里，对空集取最小值会直接返回0。AI一旦用上这个约定，一个根本不存在的整数就会摇身变成0，代码照样编译通过，意思却已面目全非。
要堵住这个漏洞，翻译器必须先判断那个整数是否存在。可是，没有任何程序能在所有情形下都判断正确。
汉森团队长期研究计算的根本极限，此前就曾证明，有些稳定可靠的神经网络虽然存在，却没有算法能把它们训练出来。此番出手，等于把同一把“不可能性”手术刀，对准了AI数学证明。
这项研究并不否定Lean的价值。代码验证通过，说明代码内部的推理确实无懈可击。
对AI公司而言，这也是一记提醒：把“编译通过”当作宣传口号之前，最好先回答一个更朴素的问题，代码证明的究竟是不是你说的那句话。
AI或许已经学会写出漂亮的证明，但判断它到底证明了什么，依然是人类数学家守着的最后一道关口。
特别声明：以上内容(如有图片或视频亦包括在内)为自媒体平台“网易号”用户上传并发布，本平台仅提供信息存储服务。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
