OpenAI 公布 AI 生成的 Navier–Stokes 千禧年问题解法及 Lean 形式化

OpenAI 公布一份由内部 AI 系统生成的 Navier–Stokes 证明与 Lean 形式化，并表示该构造给出了平滑外力下有限时间奇性，对应 Clay 问题表述中的 breakdown alternatives C/D。OpenAI 还披露相关搜索由大规模协同 agents 完成。Radar 将其记录为 OpenAI 已公开的研究主张与形式化产物，而不是替代数学共同体的最终独立认证。