#OpenAI宣布攻克千禧年难题#OpenAI公布的是AI对纳维—斯托克斯存在性与光滑性问题提出的一套解答，并给出了Lean形式化证明。这道题研究的是三维流体运动过程中，会不会在有限时间内突然出现数学上的奇点。

Lean验证很重要，说明推理链条在设定的形式系统里能够成立，但它仍不能替代数学界对前提、模型对应关系和证明价值的审查。按照克雷数学研究所的规则，成果还要正式发表、经过至少两年检验并获得学界普遍认可，才能算真正解决。

谁能想到AI开始从整理资料、辅助计算，走向提出原创证明。以后数学家的竞争对手可能还真不是AI，而是更会使用AI的数学家，各行各业都会受到冲击，这句话的含金量还在增加[并不简单]