陶哲轩博客发了一篇客座文章：AI 解出纳维-斯托克斯问题，不代表数学被终结了

After Math

9月8日 OpenAI 宣布用 AI 生成了纳维-斯托克斯存在性与光滑性问题的解答，还附上了 Lean 形式化验证和一份手稿。客座作者 Silvia De Toffoli 和 Eamon Duede 直接泼了盆冷水：逻辑上有效的证明不等于数学家要的证明。数学家需要的是能读懂、能消化、能接着往下推进的“可理解的证明”，而 AI 给出的东西目前还漂在形式逻...

推荐理由：陶哲轩的平台、两位署名学者、直接回应 OpenAI 9 月 8 日的声明，这三样加在一起让这篇文章分量很重。它不止是表态，而是提出了“可理解的证明”这个具体框架，把形式验证和数学研究之间的鸿沟说清楚了。对 AI 从业者来说，这比一百篇“AI 又赢了”的标题都有用，所以我会给 featured 并打 78 分——信息密度高，但正文没给出更多技术细节，分数先不打满。