模型Astra一口气攻克10项数学难题根本不存在

寂静回声

8月1日，OpenAI宣布，内部模型Astra一口气攻克10项数学难题，非Sofic群、高维球体堆积上界、量子并行重复定理等，每个证明都过了机器验证，代码开放在GitHub。
但欢呼声还没停，反转就来了。有数学家发现，这10项成果里有几项，经不起推敲。
先说个背景，这些证明用的验证工具叫Lean，最早由微软研究院孵化、现在由独立机构Lean FRO维护的开源软件，相当于数学证明的编译器。数学家把证明写成代码，一个内核程序逐行检查每一步推导，全对才放行。OpenAI也是用它给成果背书，机器验证通过，一直被当成可靠保险。
哥伦比亚大学副教授Henry Yuen研究量子并行重复定理多年，是这个方向绕不开的人物。
他看完Astra那份证明后，说自己失望。
Lean的证明铺垫绕了半天，关键的一步被一笔带过，没有解释为什么这么走是对的。
他看得懂每一步的逻辑，却说不出这一招背后的直觉是什么。
连深耕这个方向的人都吃不准它到底在说什么，这事儿就不能简单算翻篇了。

更实锤的还在Astra发布前几天，7月25日，有人用不到300行Lean证伪了科拉兹猜想，3天后就被发现是钻了Lean内核的一个底层漏洞的空子，跟猜想本身毫无关系，发布者其实心里清楚这是在演示漏洞，不是真宣称破了题。
巧的是，OpenAI的研究员Daniel Selsam后来带着一个专攻网络安全的AI帮Lean团队做审计，又揪出了几个类似的编程漏洞，全部修复。
这说明一件事：Lean能不能被信任，本身也是个动态过程，光看“编译通过”这四个字，不够。
真戳中要害的问题，是数学界这几天反复在提的一点：Lean只管代码编译，逻辑对不对，管不了你写的定义是不是你想证的那个定理。
定理证对了，目错了，Lean照样绿灯放行。
形式化的表述和数学家脑子里真正关心的那个问题，中间还隔着一层人工判断，机器越不过去。
OpenAI自己在公告里也承认，10项成果里只有非Sofic群和Connes刚性猜想两章，找了外部数学家通读过手稿，其余的目前更多是“内部审阅”。
看来以后不能急着相信哪些AI攻克了数学难题的说法，AI能生成证明，但理解和把关，还得靠人。