在放出数百份 Lean 证明的同时，OpenAI 还分享了一项与千禧年难题相邻的成果：有研究者整理的追踪记录显示，其内部模型对无粘三维欧拉方程给出了一个形式化的有限时间爆破论证，并构造了光滑、紧支、无散度的初始速度场，外部独立评审尚未完成。这类问题之所以重要，是因为它与 Navier-Stokes 千禧年大奖难题同属流体方程的核心地带。需要强调，这仍是待外部核验的形式化主张，不等于问题已被最终解决。
「算出来」和「想明白」从来不是一回事
数学家长期扮演两个角色：证明者与阐释者。证明者负责给出严格推导，阐释者负责告诉世人这个结果为什么重要、它改变了什么图景、它和别的领域怎么勾连。过去这两个角色由同一个人担任，因为通常只有证出它的人最懂它。
当机器能暴力枚举路径、跑出证明，甚至在人类还没看懂之前就堆出几百份结果，「证明者」这部分工作开始被大规模外包。数学家面对的不是失业，而是角色被迫迁移：从亲自证明，转向判断哪些证明值得关注、它意味着什么、它通向哪里。
意义的译者
这有点像翻译。原著是机器写的那份证明，但它写得极快、极密、极不像人话。人类数学家的工作变成把这份证明「译」回人类的数学审美里——哪一步是关键突破，哪一步是技巧堆砌，哪个猜想因此被点亮，哪个方向从此死路一条。
这个角色并不卑微。事实上它可能更接近「哲学」：
- 机器负责结论的对错，人负责结论的份量。
- 机器负责路径的存在，人负责路径的意义。
- 机器负责广度，人负责纵深。
保留意见
必须说清楚：形式化证明通过类型检查，只代表这一份推导自洽，不代表它对应了真实的数学洞察；OpenAI 自己当天就撤回 3 份、修订 14 份，说明机器产出也会犯低级错误。人类数学家的判断力，在这个时代不是被削弱了，而是被更清晰地推向了「意义」这一端。