OpenAI把一个未发布的模型扔向数学深海，88小时内捞出Navier-Stokes存在性与光滑性问题的候选解——这是七大千禧年难题之一。随后GPT-6 Astra花了17小时，用Lean完成形式化验证。期间系统发送490万条消息，消耗约3000亿输出token，数字大到让人来不及兴奋就先眩晕。
数字很浪漫，争议却很现实。Simon Willison在博客中对比双方陈述后提出一个尖锐问题：这个未发表数学解是否会被后续模型当成训练语料抢先用掉？当解题速度超过审稿速度，所有权比正确性更早变得模糊。Anthropic研究员和OpenAI高管显然各执一词，但真正该被追问的是数据使用边界——OpenAI有没有权利把一场实验性证明直接写进下一代模型的记忆？
其实对数学界而言，88小时更像是一场压力测试而非最终证明。没有完整推导公开，没有同行评议，Lean验证只能说明机器认为推理链条没问题，并不保证人类理解了那个反直觉的构造。让这件事真正令人后背发凉的，是AI与形式化工具咬合后形成的新节奏：它正把数学从“发现”变成“可执行程序”。当模型在token流里比人类更早看到真理，我们或许该重新回答一个老问题——证明的终点到底在人，还是在机器？
